#14863 closed bug (fixed)
QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | quantified-constraints/T14863 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
#14833 fixes #14835: we can witness curryC :: ((a, b) |- c) :- (a |- b |- c)
.
Now for the entirely predictable, how about uncurryC
{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs, LiberalTypeSynonyms, TypeOperators, MultiParamTypeClasses, FlexibleInstances #-} data Dict c where Dict :: c => Dict c infixr |- class (a => b) => (a |- b) instance (a => b) => (a |- b) type a :- b = Dict (a |- b) uncurryC :: forall a b c. (a |- b |- c) :- ((a, b) |- c) uncurryC = Dict
$ ghci -ignore-dot-ghci Z.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Z.hs, interpreted ) Z.hs:13:12: error: • Could not deduce: c arising from a use of ‘Dict’ from the context: a |- (b |- c) bound by a quantified context at Z.hs:1:1 or from: (a, b) bound by a quantified context at Z.hs:1:1 • In the expression: Dict In an equation for ‘uncurryC’: uncurryC = Dict • Relevant bindings include uncurryC :: (a |- (b |- c)) :- ((a, b) |- c) (bound at Z.hs:13:1) | 13 | uncurryC = Dict | ^^^^ Failed, no modules loaded. Prelude>
Change History (8)
comment:1 Changed 19 months ago by
comment:2 Changed 19 months ago by
In uncurryC2
we have a given
[G] Implies a (Implies b c)
by taking its superclass we also have
[G] forall. a => Implies b c
But now we are stuck because I have not yet implemented the superclass story for quantified constraints.
comment:4 Changed 19 months ago by
Yes; and I've added a test case
commit 32e8499889d314e9efd0747b4053290a2dc237d5 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Fri Mar 2 22:53:27 2018 +0000 Test Trac #14863
comment:5 Changed 19 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
comment:6 Changed 19 months ago by
This is great work thanks!
For those interested these examples came from Edward Kmett's encoding of sums of Constraints. This may be a milestone, since curryC
/ uncurryC
mean that the "category of entailment" (:-)
is a Cartesian closed (Constraint
) category (which means we could get HOAS syntax for constraints?).
comment:7 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
comment:8 Changed 16 months ago by
Milestone: | → 8.6.1 |
---|---|
Test Case: | → quantified-constraints/T14863 |
Once again, I think this
:-
thing is a red herring. Here's what I believe to be the essence of the bug:All of these
uncurryC
-functions typecheck except foruncurryC2
. (Note that the first two requireImpredicativeTypes
, so I'm not sure if this is intended to be supported or not.)