[GHC] #14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints

28 Jan 2018

      #14733: Won't use (forall xx. f xx) with -XQuantifiedConstraints
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!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             ( 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`?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14733
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler