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

 Replying to [comment:86 jstolarek]:
 > 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 don't know how to do this either. Luckily, we can reject `E2` on a first
 pass. It's possible that the only examples like this are silly in the same
 way that `E2` is silly, in that the last equation is utterly unreachable.

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

 Simon may be able to answer better than I, but I believe these refer to
 the actions taken in section 7 of the !OutsideIn paper.

 >
 > 3. What does `EvTerm` data type represent?

 These are values of constraint types, including class dictionaries, type
 equalities, and implicit parameters. `EvTerm`s are desugared in !DsBinds.
 Write back if that's not enough of an explanation.

 >
 > 4. What are branches in axioms?

 A closed type family with multiple equations leads to a so-called branched
 axiom. The way overlap works in a closed type family means that we can't
 have separate axioms for each equation. So, a branched axiom contains
 potentially many branches; each branch asserts an equality, but later
 branches can be used only when no previous branch supersedes. Does that
 help? It's all in the closed type families paper.

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

 I think this is also in !OutsideIn.

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