鉴于 ((forall b.[b]) -> Bool) 比 ((forall a.a) -> Bool) 更具多态性，为什么这段代码在 Haskell 中不进行类型检查？

Question

我正在 Haskell 中使用更高级别的类型，并基于 Peyton Jones 的任意级别类型的实用类型推断），我希望以下函数能够进行类型检查，因为 ((forall b.[b]) - > Bool) 似乎比 ((forall a. a) -> Bool) 更具多态性。

这是我的代码：

fun :: ((forall b. [b]) -> Bool) -> ((forall a. a) -> Bool)
fun arg = arg

但是，GHC 因类型错误而拒绝它。

我也尝试过

fun2 :: (forall a.a -> Bool) -> (forall b.[b] -> Bool)
fun2 arg = arg

编译成功，这与(forall a.a -> Bool)比(forall b.[b] -> Bool)更具多态性这一事实是一致的。但我不明白为什么我之前定义的 fun 函数没有类型检查。

Answer 1

正如Naïm Favier在他们的评论中所说：“打开

DeepSubsumption

。”，这将改变GHC使用的包含规则，从而引入深度skolemization：

GHC 将自动重写表达式，例如

f x

类型的

ty1 -> ty2

成为

(\ (y :: ty1) -> f x y)

;这称为 eta 扩展。请参阅任意排序类型的实用类型推断第 4.6 节，其中此过程称为“深度 skolemization”。

这确实是第 21 页论文“任意排序类型的实用类型推断”所讨论的内容：

因此，也许我们可以通过丰富包容的定义来解决问题，使图5和图6的类型系统接纳相同的程序。这就是图 7 中定义的新包含判断 ⊢

dsk ^{的原因。这种关系 包含 ⊢}ol^{；它严格关联更多类型。}