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
#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]: 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