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

31 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
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints, wipT2893
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:5 sjoerd_visscher]:
...
How about adding the workaround internally? I.e. add
{{{
class c => SomeInteralClass c
instance c => SomeInternalClass c
}}}
and translate `(forall xx. f xx)` to `(forall xx. SomeInternalClass  (f
 xx))`
That's one idea. But does that idea even work if you write it out by hand?
 I tried:

 {{{#!hs
 {-# Language QuantifiedConstraints #-}
 {-# Language GADTs #-}
 {-# Language ConstraintKinds #-}
 {-# Language FlexibleInstances #-}
 {-# Language UndecidableInstances #-}
 {-# Language UndecidableSuperClasses #-}

 class c => SomeInternalClass c
 instance c => SomeInternalClass c

 data D c where
   D :: c => D c

 proof :: (forall xx. SomeInternalClass (f xx)) => D (f a)
 proof = D
 }}}

 But that fails with:

 {{{
 Bug.hs:15:9: error:
     • Could not deduce: f a arising from a use of ‘D’
       from the context: forall xx. SomeInternalClass (f xx)
         bound by the type signature for:
                    proof :: forall (f :: * -> Constraint) a.
                             (forall xx. SomeInternalClass (f xx)) =>
                             D (f a)
         at Bug.hs:14:1-57
     • In the expression: D
       In an equation for ‘proof’: proof = D
     • Relevant bindings include proof :: D (f a) (bound at Bug.hs:15:1)
    |
 15 | proof = D
    |         ^
 }}}

 Granted, it does work if you change the `proof` to:

 {{{#!hs
 proof :: (forall xx. SomeInternalClass (f xx)) => D (SomeInternalClass (f
 a))
 proof = D
 }}}

 But that would require pervasively inserting `SomeInternalClass`
 everywhere in your program, and not just on the quantified constraints
 which lack an explicit type class constructor.

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