[Haskell-cafe] Type families and polymorphism

[Dan Doel]

On Saturday 11 July 2009 2:31:28 pm Jeremy Yallop wrote:
> Why does compiling the following program give an error?
>
> > {-# LANGUAGE TypeFamilies, RankNTypes #-}
> >
> > type family TF a
> >
> > identity :: (forall a. TF a) -> (forall a. TF a)
> > identity x = x
>
> GHC 6.10.3 gives me:
>
>      Couldn't match expected type `TF a1' against inferred type `TF a'
>      In the expression: x
>      In the definition of `identity': identity x = x

It has to do with the way that type families are checked, and the fact that 
they aren't guaranteed to be injective. You can massage the type to look like:

  identity :: forall b. (forall a. TF a) -> TF b

Which means that the caller gives us a 'b' and a 'forall a. TF a', and wants 
us to return a 'TF b'. That sounds fine, but when GHC goes to check things, 
things go awry. It instantiates things something like...

  x :: TF c (for some fresh c)
  TF c ~ TF b (this constraint must be solved for the return type to work)

However, since type families aren't necessarily injective, it can't deduce

  c ~ b

since there might well be distinct 'b' and 'c' such that 'TF b ~ TF c'. So, it 
fails to come to the conclusion that:

  x :: TF b

which is what is actually needed for the function as a whole to type. Thus, 
checking fails. I think that's a reasonably accurate description of the 
process; if not someone will probably correct me.

One could imagine extensions to solve this. For instance, if you could 
(optionally) do something like:

  identity at b x = x at b

to specifically apply the type variables, the compiler might have an easier 
time accepting such things. You can fake it now by having non-family types fix 
the variable:

  data Witness a -- = W -- if you don't like empty types

  identity :: (forall a. Witness a -> TF a) -> (forall a. Witness a -> TF a)
  identity x w = x w

This will be accepted, because inference/checking for Witness provides enough 
information to deduce the 'c ~ b' above. But of course, it's somewhat less 
than ideal.

Hope that helps.

-- Dan