#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