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

 Replying to [comment:76 simonpj]:
 >  * 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
 > }}}
 What is the meaning of `[W]` and `[D]`? "Wanted" and "derived"?

 >  * I don't understand the discussion of `Map`.  Are you perhaps
 discussing how to verify some (not shown here) implementation of a closed
 type family `Map` is in fact injective?

 Yes, I was discussing how to verify whether this definition of `Map` is
 injective:

 {{{#!hs
 type family Map (f :: k -> l) (ks :: [k]) :: [l] where
     Map f '[]       = '[]
     Map f (x ': xs) = f x ': Map f xs
 }}}

 >  * Verifying injectivity for open families: if the RHSs unify then the
 LHSs should be identical under that substitution. Eg
 > {{{
 >   type instance F a Int = a -> Int
 >   type instance F Int a = Int -> a
 > }}}
 >   These are consistent (and hence allowed) and are injective in both
 arguments.

 Ah, I haven't thought about allowing substitution when RHSs unify. Wiki
 updated.

 >  * My brain is too small to think about verifying injectivity for closed
 families. Richard?

 I only remind that I outlined an algorithm on the wiki :-) Richard, it
 would be great if you could take a look and say whether it makes sense.

 In the meantime I have almost implemented checking correctness of
 injectivity condition (point 2 from [comment:73 my earlier comment]).
 Renamer seems to be the right place for doing this.

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