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