[GHC] #5927: A type-level "implies" constraint on Constraints

[GHC]

#5927: A type-level "implies" constraint on Constraints
-------------------------------------+-------------------------------------
        Reporter:  illissius         |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.4.1
  checker)                           |
      Resolution:                    |             Keywords:
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):

 http://yav.github.io/publications/improving-smt-types.pdf

 > == 3.1    Implication Constraints ==
 > During type inference,  GHC  uses ''implication  constraints'',  which
 do not appear in Haskell source code directly. An implication constraint
 is, roughly, of the form `G ⇒ W`, where `W` is a collection of constraints
 that need to be discharged, and `G` are assumptions that may be used while
 discarding `W`. In the GHC source code, the constraints in `G` are
 referred to as ''given constraints'', while the ones in `W` are known as
 wanted constraints. The intuition behind an implication constraint is that
 `W` contains the constraints that were collected while checking a program
 fragment, while `G` contains local assumptions that are available only in
 this particular piece of code.

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