将有效的forall类型赋予左绑定变量时发生类型错误

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

让我想到"弱前缀转换"(见本文第23页)可能与此有关。将forall嵌入到一个不能"浮出"的逆变位置，似乎可以使它免受这种奇怪的错误。

Answer 1

我认为这里发生的事情是这样的:在标准的大马士革米尔纳类型推断中，let绑定是唯一发生类型泛化的地方。失败示例使用的类型签名是一个模式类型签名，它"以明显的方式约束模式的类型"。现在，在这个例子中，这个约束应该在泛化之前还是之后发生并不"明显"，但我认为，你失败的例子表明，它在泛化之前被应用。

更具体地说:在绑定let x = id in ...的let中，id的类型forall a. a->a被实例化为单型，例如a0 -> a0，然后将其赋值为x的类型，然后将其泛化为forall a0. a0 -> a0。如果，正如我所认为的，在泛化之前检查模式类型签名，它本质上是要求编译器验证单型a0 -> a0比多型forall a. a -> a更通用，而事实并非如此。

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

我认为，这是不是一个bug，这是一个意见问题。似乎没有一个实际的规范告诉我们什么是正确的行为;只有我们的期望。我建议和GHC的人讨论这件事。

Answer 2

不是一个真正的答案，但是太长了，不能评论:
它很可能是一个bug。稍微摆弄一下表达式，不出所料

let x :: forall a. a -> a; x = id in x 3

如果启用了显式写foralls，

可以工作。不过，这是一个沼泽标准的1级类型。其他一些变化:

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = y -> id y in x 3
3

好的，这是有效的，我不知道为什么lambda的行为不同，但它确实如此。然而:

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = y -> id y in x 3
<interactive>:0:31:
    Couldn't match expected type `t0 -> t1'
                with actual type `forall a. a -> a'
    The lambda expression ` y -> id y' has one argument,
    but its type `forall a. a -> a' has none
    In the expression:  y -> id y
    In a pattern binding: (x :: forall a. a -> a) =  y -> id y

(7.2.2;7.0.4给出相同的错误)。