Имеется такой код:
{-# 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 вызвана аналогичной проблемой.