[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------+-------------------------------------------
        Reporter:  lunaris     |            Owner:  simonpj
            Type:  feature     |           Status:  new
  request                      |        Milestone:  7.10.1
        Priority:  normal      |          Version:  7.4.1
       Component:  Compiler    |         Keywords:  TypeFamilies, Injective
      Resolution:              |     Architecture:  Unknown/Multiple
Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple             |       Blocked By:
 Type of failure:              |  Related Tickets:  #4259
  None/Unknown                 |
       Test Case:              |
        Blocking:              |
-------------------------------+-------------------------------------------

Comment (by simonpj):

 I don't think anyone is working on injective type families right now, but
 it would make a good project, and not too difficult.

 Lunaris's patch has a lot of irrelevant white-space changes in it.  But
 the biggest problem is that I don't think it implements the all-important
 check that a injective type family really is injective. Consider
 {{{
 injective type family F a

 type instance F Int = Bool
 type instance F Char = Bool
 }}}
 This isn't injective and should jolly well be rejected.  And this should
 be the case even if the two `type instance` declarations are in different
 modules.

 Similar code already exist for rejecting type-family ''overlap''; I think
 it is in `FamInst.checkFamInstConsistency`.  But it'd need to be beefed up
 to deal with the injectiveness check.

 And you need to take care. What about
 {{{
 type instance F Int = Bool        -- (BAD)
 type instance F Char = F Int      -- (BAD)
 }}}
 The two RHSs look different, but actually they are the same.  The
 criterion for injectivity is that
 {{{
 If    (F t1 .. tn) ~ (F s1 .. sn)
 then  t1 ~ s1
       ...
       tn ~ sn
 }}}
 That doesn't hold for the (BAD) instances, so they should be rejected.  In
 the terminology of the "Closed type families" paper, we need the two RHSs
 to be '''apart'''.

 Simon

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