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

{-# 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 типов?

Вот еще интересный эффект:

1) Такой код не проходит проверку типов:

{-# LANGUAGE RankNTypes #-}

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 `(.)'

2) А вот такой, практически эквивалентный, проходит:

{-# LANGUAGE RankNTypes #-}

f :: [forall a. t a -> t a] -> t b -> t b
f = foldr (\g -> (.) g) id

Кто это может объяснить?

И еще вопрос:
Согласно Haskell Report, выражение [f | f <- foo] транслируется в (let ok f = [f]; ok _ = [] in concatMap ok foo).
Рассмотрим такие определения:

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

foo :: [forall a. [a] -> [a]]
foo = [reverse]

bar :: [a -> b] -> a -> b
bar fs = head fs

Такое выражение проходит проверку типов:

bar [f | f <- foo]

А такие — не проходят:

bar (let ok f = [f]; ok _ = [] in concatMap ok foo)
bar foo

Почему?

Я не дам точного ответа, но поразвожу в воздухе руками, на уровне своего понимания проблемы. Возможно, поможет.

N>Согласно Haskell Report, ...
Там, где начинаются расширения GHC, Haskell report заканчивается. List comprehensions в GHC рассахариваются по-другому, но при отключенных расширениях разницу невозможно обнаружить.

N>foo :: [forall a. [a] -> [a]]
N>foo = [reverse]
GHC Haskell компилируется в Core, основанный на System F.
Полиморфная функция

id = \x -> x

компилируется (упрощенно) в:

id = \ (@ a) (x :: a) -> x

Чтобы использовать полиморфную функцию id, ей нужно передать тип:

test = id True

компилируется в

test = id @ Bool True

С этой точки зрения, типы [forall a . a] и forall a . [a] унифицировать нельзя — первый является списком функций, второй — функцией, возвращающей список. Невозможность вызвать bar с аргументом foo вызвана аналогичной проблемой.