相关疑难解决方法(0)

我发现我可以说

{-# LANGUAGE RankNTypes #-}
f1 :: (forall b.b -> b) -> (forall c.c -> c)
f1 f = id f

(和HLint告诉我,我可以在这里做"Eta减少"),但是

f2 :: (forall b.b -> b) -> (forall c.c -> c)
f2 = id

无法编译:

Couldn't match expected type `c -> c'
            with actual type `forall b. b -> b'
Expected type: (forall b. b -> b) -> c -> c
  Actual type: (forall b. b -> b) -> forall b. b -> b
In the expression: id …

这是类型检查器中的错误吗？

Prelude> let (x :: forall a. a -> a) = id in x 3

<interactive>:0:31:
    Couldn't match expected type `forall a. a -> a'
                with actual type `a0 -> a0'
    In the expression: id
    In a pattern binding: (x :: forall a. a -> a) = id

以上事实无法进行类型检查,但这种扭曲成功:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id
3

使我认为"弱prenex转换"(见23页文章)可能以某种方式有关.嵌入一​​个forall不能"浮出"的逆变位置似乎可以避免这种奇怪的错误.