One more example: This does not type-check: ------------------------------------------------------- {-# LANGUAGE RankNTypes, ImpredicativeTypes #-} f :: [forall a. t a -> t a] -> t b -> t b f = foldr (.) id ------------------------------------------------------- Couldn't match expected type `forall a. f a -> f a' against inferred type `b -> c' In the first argument of `foldr', namely `(.)' But this, very similar, does type-check: ------------------------------------------------------- {-# LANGUAGE RankNTypes, ImpredicativeTypes #-} f :: [forall a. t a -> t a] -> t b -> t b f = foldr (\g -> (.) g) id ------------------------------------------------------- What is the reason for this? Thanks, Vladimir On 6/9/09, Vladimir Reshetnikov wrote:

Hi,

I have the following code: ------------------------------------------------------- {-# LANGUAGE RankNTypes #-}

f :: ((forall a. a -> a) -> b) -> b f x = x id

g :: (forall c. Eq c => [c] -> [c]) -> ([Bool],[Int]) g y = (y [True], y [1])

h :: ([Bool],[Int]) h = f g -------------------------------------------------------

GHC rejects it: Couldn't match expected type `forall a. a -> a' against inferred type `forall c. (Eq c) => [c] -> [c]' Expected type: forall a. a -> a Inferred type: forall c. (Eq c) => [c] -> [c] In the first argument of `f', namely `g' In the expression: f g

But, intuitively, this code is type-safe, and actually I can convince the typechecker in it with the following workaround: ------------------------------------------------------- h :: ([Bool],[Int]) h = let g' = (\(x :: forall a. a -> a) -> g x) in f g' -------------------------------------------------------

So, is the current behavior of GHC correct ot it is a bug? How unification for rank-N types should proceed?

Thanks, Vladimir