[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------------+-------------------------------------
              Reporter:  lunaris     |            Owner:  jstolarek
                  Type:  feature     |           Status:  new
  request                            |        Milestone:  7.10.1
              Priority:  normal      |          Version:  7.4.1
             Component:  Compiler    |         Keywords:  TypeFamilies,
            Resolution:              |  Injective
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:  #4259
             Test Case:              |
              Blocking:              |
Differential Revisions:  Phab:D202   |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Re comment:89 and comment:90 I'm struggling with limited personal
 bandwidth, and daunted by the challenge of giving a tutorial about the
 type inference engine, which is one of the most complex parts of GHC.

 Let me make this offer. If you do the rest, I'll do the bit in the type
 inference engine that exploits injectivity.  It won't take long, and then
 you can see.

 Decomposition in brief.  If you want `Maybe a ~ Maybe b` then it's enough
 to prove `a ~ b`. From a proof of the latter we can get a proof of the
 former. No more than that.

 Simon

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