Имеется такой код:

{-# 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 отвергает его:

    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

Тем не менее, интуиция подсказывает, что этот код является типобезопасным, и на самом деле можно убедить в этом typechecker с помощью такой подсказки:

h :: ([Bool],[Int])
h = let g' = (\(x :: forall a. a -> a) -> g x) in f g'

Вопрос: является ли нынешее поведение GHC правильным или это баг? Как на самом деле должна происходить унификация rank-N типов?