#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