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