#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 goldfire): Replying to [comment:73 jstolarek]:

2. That condition must contain only the result type variable on the LHS of `->` and all other type variables on the RHS of `->`. In other words if I declare `type family P a b = r` then I'm only allowed to write `r -> a b` or `r -> b a` injectivity condition. Questions here: a) can I add a restriction that type variables on the RHS must be given in exactly the same order as they were given in the head declaration? This would make the implementation simpler; b) where should this check be done? In the renamer?

I'm ambivalent on this design decision (that the variables have to be in the same order in the annotation). I suppose it simplifies the implementation. Yes, the renamer seems like a fine-enough place to do the check.

3. Once we check 2) we must verify that the type family is indeed

injective. Not sure where this should happen? My guess is that during typechecking of a type family equations. Algorithm is outlined [wiki:InjectiveTypeFamilies#Implementationoutline here]. Please see updates to the wiki page, labeled '''RAE''' ... '''End RAE'''.

Does the implementation plan outlined so far look sensible? Are there

any misconceptions?

4. Once we pass these checks injectivity becomes a binary property, so

we can discard injectivity conditions written by the user and replace it with a `Bool`. Richard, when we first spoke about injective type families you suggested that all the magic will go into `isDecomposableTyCon` in `types/TyCon.lhs`. I've added a `Bool` field to `SynTyCon` data constructor of `TyCon` data type and made `isDecomposableTyCon` use that field to tell whether a type family is injective or not. (Checks described in 2 and 3 are not implemented. When a user writes injectivity declaration for a type family I just assume it is correct.) Sadly, this does not work. Here's an example test case:

{{{#!hs type family F a = r | r -> a where F Int = Bool F Bool = Int F a = a

foo :: F a -> F a foo = id }}}

This fails with:

{{{ Couldn't match type ‘F a0’ with ‘F a’ NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: F a -> F a Actual type: F a0 -> F a0 In the ambiguity check for: forall a. F a -> F a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘foo’: foo :: F a -> F a }}}

I added traces to verify that `isDecomposableTyCon` is called for `F`

type family and it correctly returns `True`.

Out of curiosity I turned on `AllowAmbiguousTypes` and added a

definition like this:

{{{ bar :: Int -> Int bar = foo }}}

That failed with:

{{{ Couldn't match type ‘F a0’ with ‘Int’ The type variable ‘a0’ is ambiguous Expected type: Int -> Int Actual type: F a0 -> F a0 In the expression: foo In an equation for ‘bar’: bar = foo }}}

I imagine that getting this one to work definitely requires more changes

than just `isDecomposableTyCon`. Yes, Simon's comment above is correct -- I was just wrong about the `isDecomposableTyCon` thing. Actually, injective type families still need to say "no" to `isDecomposableTyCon`, because of the '''left''' and '''right''' coercion formers, which assume generativity.

Then again GHC can already deal with some cases of injectivity:

{{{#!hs type family F a = r | r -> a where F Int = Int F Bool = Bool F a = a

foo :: F a -> F a foo = id

bar :: Int -> Int bar = foo }}}

That works perfectly fine in GHC 7.8.

What works perfectly fine? Not the code you wrote above, because it contains a not-currently-parsed injectivity annotation. I tried it without the injectivity annotation, and it does indeed work. But not because of injectivity, at all: it's because GHC is clever enough to figure out that `F` is just an identity function, and so the `F a`s in `foo`'s type become `a`. If you swap the `Int` and `Bool` RHSs in the definition (which preserves injectivity), the code fails to compile.

I tried to analyse what's going on with `-ddump-tc-trace` but the dumps

are 600-1000 lines long. Of course the source code itself is even longer, so I'd appreciate any directions where should I start looking. Fair warning: 1000 lines of `-ddump-tc-trace` isn't long at all! :)

One final question. Assuming that `SynTyCon` really should have a new

field, I believe this field should be stored in interface files. After all we want injectivity information to propagate from one module to another. Now I wonder how this interacts with open type families. I understand that these are typechecked progressively as we find more equations. I haven't looked at the implementation but my intuition from reading GHC papers is that in a given module we import open type family equations from other modules, collect equations from current module and proceed with type checking of an open type family. Is that intuition correct? If so then I believe that checking of injectivity (point 3 of my outline) should be done during this stage (I believe it would be best to combine it with checking equation overlapping). Agreed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:79 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler