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

 I've read section 7.4 of OutsideIn(X) paper. Code makes more sense now but
 still I have some questions. Most importantly I'm trying to understand
 FINST top-level reaction rule (OutsideIn paper, fig. 24 page 65), which
 according to my understanding is implemented by `doTopReactFunEq`. Since I
 don't have LaTeX in the wiki I'll be using following notation:

 \Q - set of top-level axiom schemes
 \g - little gamma
 \d - little delta
 \th - little theta
 \t - little tau
 \e - little epsilon
 _0 - 0 in a subscript
 \vec{...} - a vector of values, in paper denoted using overline
 \in - set membership realtion

 Now the rule:

 {{{
 forall \vec{a}. F \vec{Xi_0} ~ Xi_0 \in \Q             -- (1)
 \vec{b} = ftv(\vec{Xi_0})                              -- (2)
 \vec{c} = \vec{a} - \vec{b}                            -- (3)
 \g fresh                                               -- (4)
 \th = [\vec{b |-> \t_a},\vec{c |-> \g}]                -- (5)
 \th \vec{Xi_0} = \vec{Xi}                              -- (6)
 if (l = w) then \vec{\d} = \vec{\g} else \vec{\d} = \e -- (7)
 -------------------------------------------------------------
 topreact[l](\Q, F \vec{Xi}~Xi) = {\d, \th Xi_0 ~ Xi}   -- (8)
 }}}

 Here's how I understand (or misunderstand that rule):

 Premise (1) represents a type family equation written by the user (either
 from a closed or open type family). `\vec{Xi_0}` represents the LHS of `F`
 ie. patterns in that equation. So for example if the equation is `F [b]
 Bool c` then `\vec{Xi_0}` is `([b],Bool, c)`. I'm not sure about `[b]` - I
 think that's not canonical? Are axioms canonicalized?

 I'm also not sure about the meaning of `\vec{a}` in (1)'s forall. My
 intuition would be that these are type variables in the LHS (`b` and `c`
 in above example). But then I don't know how to understand premise (2). If
 `\vec{b}` represents free variables if `\vec{Xi_0}` then wouldn't this be
 identical to `\vec{a}`? This does not make sense because in that situation
 `\vec{c}` in premise (3) would always be empty.

 Premise (5) is a substitution used in premise (6) to turn the LHS of the
 original axiom into LHS of a constraint we are trying to solve. But what
 does `\t_a` represent? Instantiation of variables in the original axiom to
 some particular values present in `\vec{Xi}`?

 Premise (7) says that if a constraint is wanted then we introduce new
 variables. I'm not sure why. Maybe this will become clear once I
 understand the rest.

 I'm not sure if I understand the conclusion (8). Reading the rule I see
 that if we have `F \vec{Xi} ~ Xi` constraint we use it to figure out the
 `\th` substitution and then use that substitution to create a new
 constraint that tries to equate the RHS of our current constraint with the
 RHS of original axiom. But why do we want this? I could use an example
 with more comments than in the paper (and the example could be more
 complicated too). Before proceeding with the implementation I'd like to
 understand how injectivity affects FINST rule.

 What is not clear to me is whether the new constraint we are producing is
 wanted or given? My guess is that we produce a given if the original
 constraint was given and wanted if the original was wanted.

 I also wonder whether injectivity gives us a new interaction rule:

 {{{
 INJFEQFEQ   interact[l] (F \vec{Xi_1} ~ Xi, F \vec{Xi_2} ~ Xi) =
                         (F \vec{Xi_1} ~ Xi, \vec{ Xi_1 ~ Xi_2 })
 }}}

 where `\vec{ Xi_1 ~ Xi_2 }` represents vector of pairwise constraints.

 A few more questions unrelated to the paper:

 1. Are axioms for associated types treated differently than for open type
 families?

 2. What does `BuiltInSynFamTyCon` constructor represent?

 3. `Note [Basic Simplifier Plan]` in `TcInteract` mentions "inert
 reactions" and "spontaneous reactions". What's the difference between the
 two?

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