[Haskell-cafe] Unification for rank-N types

[Vladimir Reshetnikov]

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