#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