[GHC] #14840: QuantifiedConstraints: Can't define class alias

[GHC]

#14840: QuantifiedConstraints: Can't define class alias
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:  fixed             |             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 Iceland_jack):

 I'm thinking of these as Church encoding, I wanted to see how close I
 could get to something like a sum or existential constraints

 {{{#!hs
 type Sum a b = forall sum. (a -> sum) -> (b -> sum) -> sum
 }}}

 and actually, both of these definitions work-for-some-definition-of! (with
 judicious aliasing.)

 Here is an example that works today, I can Church encode `(a, b)`

 {{{#!hs
 {-# Language TypeOperators, GADTs, FlexibleInstances,
 MultiParamTypeClasses, UndecidableInstances, ConstraintKinds, RankNTypes,
 QuantifiedConstraints #-}

 data Dict c where
   Dict :: c => Dict c

 class    (a => b) => (a |- b)
 instance (a => b) => (a |- b)
 }}}

 We define a type class constraint of church encoded products (`forall
 pair. (a -> b -> pair) -> pair`)

 {{{#!hs
 class    (forall pair. (a |- b |- pair) |- pair) => ChurchPair a b
 instance (forall pair. (a |- b |- pair) |- pair) => ChurchPair a b
 }}}

 And amazingly GHC can conclude `ChurchPair a b` from `(a, b)`!

 {{{#!hs
 type a :- b = Dict (a |- b)

 wit :: (a, b) :- ChurchPair a b
 wit = Dict
 }}}

 the other half of the isomorphism is too much for GHC

 {{{#!hs
 reductionStackOverflow :: ChurchPair a b :- (a, b)
 reductionStackOverflow = Dict
 }}}

 which is as expected, from your response to one of the other tickets

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14840#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler