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

 Richard, either I'm not getting the subtleties of your arguments or you're
 misunderstanding what I meant to say on the wiki page. Or both :-)

 I now see the theoretical difference between "overlaps" and "subsumes" but
 I don't yet see how that is important in my algorithm outline. I re-read
 parts of the closed type families paper and now I'm not even sure whether
 I meant "overlaps" or "unifies". Anyway, I believe that my thinking is
 correct and in my algorithm I have addressed problems that you raised. It
 looks that I need help with sorting out the terminology so things are
 clear.

 Now, looking at your examples:

 {{{#!hs
 type family E1 a = r | r -> a where
   E1 Int = Int -- 1
   E1 a   = a   -- 2
 }}}
 When my algorithm reaches (2) it will attempt to unify `a` with RHS of
 equation (1). It will succeed with substitution `[ a -> Int ]`. It will
 apply that substitution to the LHS of (2) and proceed with checking
 whether after substitution this equation is subsumed (?) by any of the
 earlier ones. Clearly, it is by the first equation and since this is the
 last equation we declare `E1` to be injective. In other words I know that
 (2) will never produce an `Int` since this will equation will never be
 reached for `a` equal to `Int`.

 Now `E2`:

 {{{#!hs
 type family E2 (a:: Bool) = r | r -> a where
   E2 False = True
   E2 True  = False
   E2 a     = False
 }}}
 I consider almost identical example on the wiki:
 {{{#!hs
 type family Bak a = r | r -> a where
      Bak Int  = Char
      Bak Char = Int
      Bak a    = a
 }}}
 The difference is the RHS of the last equation: a concrete type in your
 example, a type variable in mine. Yet I believe that both examples are
 intended to demonstrate the same problem - see discussion below that
 example.

 > In `IdNat` and `NatToMaybe`, unification fails before seeing the
 recursive use of the type family.

 Right. I assumed that noticing that allows us to conlcude that equations
 of `IdNat` and `NatToMaybe` produce distinct types and thus these type
 families are injective. Your reasoning in that whole paragraph completely
 agrees with mine.

 > But I'd want a proof first.

 Agreed. As I said, I've been unable to produce a counter-example but that
 doesn't meant that one does not exist.

 I have a question about closed type families paper. Paragraph just after
 Candidate Rule 2 (section 3.2, page 3) says: "As a notational convention,
 apart(ρ, τ) considers the lists ρ and τ as tuples of types; the apartness
 check does ''not'' go element-by-element.", where "not" is emphasized. Why
 is this important? Seems like the choice of representing patterns and
 types as tuples or lists is just an implementation detail.

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