[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 jstolarek):

 Simon, Richard, others,

 I'm making progress on this one but before going too far I want to get a
 green light on my design proposal (points 1-3). I've also bumped into some
 problems and have a couple of questions.

 My design proposal is to implement only injectivity of type A (ie. plain
 injectivity in all arguments). The consequences of this are:

 1. A user is allowed to write at most one injectivity condition.

 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?

 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].

 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`. 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.

 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.

 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).

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