id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential,wikipage
14733,Won't use (forall xx. f xx) with XQuantifiedConstraints,Iceland_jack,,"{{{#!hs
{# 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 [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:28 wip/T2893] gives
{{{
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 174quantifiedconstraints.hs, interpreted )
174quantifiedconstraints.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 174quantifiedconstraints.hs:8:137
• In the expression: D
In an equation for ‘proof’: proof = D
• Relevant bindings include
proof :: D (f a) (bound at 174quantifiedconstraints.hs:9:1)

9  proof = D
 ^
}}}
How can I instantiate `xx` to `a`?",bug,closed,normal,,Compiler,8.5,fixed,QuantifiedConstraints,,Unknown/Multiple,Unknown/Multiple,None/Unknown,,,,,,