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@b x = x@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