Won't use (forall xx. f xx) with -XQuantifiedConstraints
{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
data D c where
D :: c => D c
proof :: (forall xx. f xx) => D (f a)
proof = D
Running this program with wip/T2893 gives
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 174-quantifiedconstraints.hs, interpreted )
174-quantifiedconstraints.hs:9:9: error:
• Could not deduce: f a arising from a use of ‘D’
from the context: forall xx. f xx
bound by the type signature for:
proof :: forall (f :: * -> Constraint) a.
(forall xx. f xx) =>
D (f a)
at 174-quantifiedconstraints.hs:8:1-37
• In the expression: D
In an equation for ‘proof’: proof = D
• Relevant bindings include
proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1)
|
9 | proof = D
| ^
How can I instantiate xx
to a
?
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 |