将有效的forall类型归为let-bound变量时键入错误

Question

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

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不能"浮出"的逆变位置似乎可以避免这种奇怪的错误.

Answer 1

我认为这里发生的是这样的：在标准 Damas-Milner 类型推断中，let 绑定是唯一发生类型泛化的地方。您的失败示例使用的类型签名是模式类型签名，它“以明显的方式限制模式的类型”。现在，在这个例子中，这种约束是否应该在泛化之前或之后发生并不“明显”，但我认为你的失败示例表明它在泛化之前应用。

更具体地说：在 let 绑定中let x = id in ...，所发生的情况是，id的类型forall a. a->a被实例化为单类型，例如a0 -> a0，然后被分配为x的类型，然后被泛化为forall a0. a0 -> a0。正如我所想，如果在泛化之前检查模式类型签名，那么它本质上是要求编译器验证 monotypea0 -> a0是否比 polytype 更通用forall a. a -> a，但事实并非如此。

如果我们将类型签名移至绑定级别，则let x :: forall a. a-> a; x = id in ...在泛化后检查签名（因为为了启用多态递归而明确允许这样做），并且不会发生类型错误。

我认为这是否是一个错误，这是一个见仁见智的问题。似乎没有一个实际的规范可以告诉我们这里的正确行为是什么；只有我们的期望。我建议与 GHC 人员讨论此事。