[Haskell-cafe] Type families and polymorphism
Dan Doel
dan.doel at gmail.com
Sat Jul 11 18:48:20 EDT 2009
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
More information about the Haskell-Cafe
mailing list