On Jul 11, 2009, at 14:31 , 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

The scope of each a is the surrounding parentheses, so the de facto type is TF a -> TF b. Or, put otherwise, you're saying that for *any* type (TF a) you can produce *any* type (TF a) (because of the delimited forall-s), but then the code asserts that they are the same type. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

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

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

The error message is slightly better in GHC head: Couldn't match expected type `TF a1' against inferred type `TF a' NB: `TF' is a type function, and may not be injective In the expression: x In the definition of `identity': identity x = x Dan Doel already explained how the lack of injectivity leads to a type checking error. FWIW, the same code would work with a data family, because data families are injective. regards, Bertram