QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'
#14833 (closed) fixes #14835 (closed): we can witness curryC :: ((a, b) |- c) :- (a |- b |- c)
.
Now for the entirely predictable, how about **un**curryC
{-# 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>
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |