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

 > Does that clarify?

 Yes.

 I don't yet see how to deal with your `E2` example. It looks like we would
 need to have pattern-exhaustiveness checking for type families. And this
 would only be possible for closed kinds I think. Well, for open kinds type
 family would simply be non-injective.

 I have a few more questions about implementation. These most likely go to
 Simon. I've been trying to wrap my head around implementation of
 `doTopReactFunEq` and I have these questions:

 1. What does the term "react" mean? As in the name `doTopReact` and the
 comment below its type signature: "The work item does not react with the
 inert set..." (TcInteract, L1412).

 2. What is "interaction"? As in the module name `TcInteract` or the
 comment mentioned above: "... so try interaction with top-level
 instances".

 3. What does `EvTerm` data type represent?

 4. What are branches in axioms?

 5. I don't understand how canonicalization works. Is there an overview
 somewhere? Other than `Note [Canonicalization]`, which unfortunately is
 too vague for me :-(

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