[GHC] #2893: Implement "Quantified constraints" proposal

[GHC]

#2893: Implement "Quantified constraints" proposal
-------------------------------------+-------------------------------------
        Reporter:  porges            |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  ⊥
       Component:  Compiler          |              Version:  6.10.1
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #5927             |  Differential Rev(s):  Phab:D4353
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 > ... superclass stufff ... Give it a whirl!

 Terrific. I'd appreciate if someone could test my hypothesis of a use case
 [1]. Note this using QuantifiedConstraints purely as implications with
 nothing `forall`'d.:

 > Consider modelling the logic for somewhat-injective type functions.
 > Take type-level Boolean `And` [5].
 >
 > `And` is not fully injective but:
 >
 > * If the result is True, the two arguments must be True.
 >
 > * If the result is False and one argument is True, the other must be
 False.

 {{{
 class ( (b3 ~ True) => (b1 ~ True, b2 ~ True),
        (b3 ~ False, b1 ~ True) => b2 ~ False,
        (b3 ~ False, b2 ~ True) => b1 ~ False )
           => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool)  | b1 b2 -> b3
              where {}

 instance And True  b2 b2
 instance And False b2 False

 x3 = undefined :: (And b1 b2 True) => (b1, b2)
 -- should infer x3's type as :: (True, True)
 }}}

 [https://mail.haskell.org/pipermail/glasgow-haskell-
 users/2018-February/026694.html [1]]

 [https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html
 [5]] [https://mail.haskell.org/pipermail/glasgow-haskell-
 users/2017-November/026650.html continued]

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