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

 Simon, I'm trying to understand your [comment:76 earlier comment]:
 >  * We are not (at least for now) changing System FC.  So the only effect
 of injectivity is to add extra "Derived" unification constraints, very
 much like functional dependencies.  If we see
 > {{{
 >  [W] F t ~ F s
 > }}}
 >   then we don't decopose it.  Instead we add
 > {{{
 >  [D] t ~ s
 > }}}
 >   That guides inference, but does not produce proof terms.  So, no,
 nothing to do with `isDecomposableTyCon`.  Much more like the
 `try_improvement` code in `TcInteract.doTopReactFunEq`.

 First of all, do we ever get a chance of actually seeing `F t ~ F s`? I
 think this is not canonical and if such constraint ever appears it would
 be turned into `F t ~ a, F s ~ a`. I'm not sure which of the
 canonicalization rules in Fig. 21 in OutsideIn paper would be responsible
 for that conversion because I don't know the meaning of these stylized D,
 F and T used in the mentioned figure. My guess would be FFLAT[W/G]R rules.
 Anyway, once we have `F t ~ a, F s ~ a` we could apply my suggested
 INJFEQFEQ interaction rule to generate `[D] s ~ t`. If my thinking here is
 right then shouldn't the implementation go into `TcInteract.interactFunEq`
 (guessing from its name)?

 I also wonder whether `[W]` is important in your `[W] F t ~ F s` example?
 I believe this rule is valid for both given and wanted constraints.

 I don't understand what you mean by "we don't decopose it". What is this
 "decomposition" that you mention?

 I believe that the only moment when injectivity interacts with top-level
 axioms is when we're deducing LHS from RHS. I suspect this might require a
 new reaction rule, separate from FINST.

 Are my ideas here correct?

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