处理 GHC 中较高级别类型的特殊情况？

Question

考虑 GHCi 会话中的这个示例：

Prelude> :set -XRankNTypes
Prelude> let bar :: (forall a.[a]->[a]) -> [Int]; bar f = f [1,2,3]

这定义了一个 rank-2 类型的函数bar。因此，类型推断不应该能够推断出正确的类型：

Prelude> let foo f = bar f

确实，

<interactive>:7:17:
Couldn't match type `t' with `[a] -> [a]'
  `t' is a rigid type variable bound by
      the inferred type of foo :: t -> [Int] at <interactive>:7:5
In the first argument of `bar', namely `f'
In the expression: bar f
In an equation for `foo': foo f = bar f

令人惊讶的是，如果我们以无点风格编写相同的内容，它会起作用：

Prelude> let baz = bar
Prelude> :t baz
baz :: (forall a. [a] -> [a]) -> [Int]

类型推断如何在这里推断出更高等级的类型？ 任何人都可以确认这在 GHC 中得到了特殊处理，或者指出我错在哪里。

Answer 1

在存在更高级别类型的情况下，类型推断的主要问题是推断 lambda 绑定变量的多态类型。在您的第一个示例中，键入foo 的唯一正确方法是将多态类型分配给f。在您的第二个示例中，不需要这样的东西。相反，baz 只是bar 的（微不足道的）部分应用。无需任何额外的类型注释，只要应用更高级别的多态函数，而不需要任何 lambda 抽象，就应该总是可行的。

另请参阅GHC User's Guide 中的相应部分以及各种研究论文。