[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 jstolarek):

 Can I get some more time before I throw in the towel? Say, until next
 Thursday?

 Simon, if you were to start working on this what parts of my
 implementation need to be finished? Everything up to `SynTyCon` storing a
 list of `Bool`s? In what form would you like my patch? A differential
 revision? A branch on github? Do you want my work rebased against latest
 HEAD?

 > 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.

 Obviously, this is what we currently have for data types and what we want
 for injective type families. But from the OutsideIn paper my understanding
 was that *current* treatment of *type families* is different.

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