如何为超出其范围的刚性类型变量重现 GHC 的类型错误？答案

【问题标题】：How to reproduce GHC's type error for a rigid type variable escaping its scope?如何为超出其范围的刚性类型变量重现 GHC 的类型错误？
【发布时间】：2021-06-05 00:04:45
【问题描述】：

以下是刚性类型变量超出其范围的典型示例：

{-# LANGUAGE RankNTypes #-}
runST :: forall a. (forall s. ST s a) -> a
runST _ = undefined

newRef :: forall s a. a -> ST s (Ref s a)
newRef _ = undefined

runST (newRef 'x') -- type error (rigid a would escape its scope)

我试图通过手动进行统一/包含来重现错误：

-- goal: unify the expression `runST (newRef 'x')`
fun :: (forall a. (forall b. Foo b a) -> a)
arg :: (forall c. Foo c (Bar c Char))
(forall b. Foo b a0) -> a0 -- meta-ize all tvs bound by the outermost quantifier
Foo s0 (Bar s0 Char) -- skolemize all tvs bound by the outermost quantifier
-- subsumption judgement: offered `arg` is at least as polymorphic as fun's requested argument:
Foo s0 (Bar s0 Char) <: (forall b. Foo b a0)
Foo s0 (Bar s0 Char) <: Foo s1 a0 -- skolemize on the RHS
Foo ~ Foo -- generativity of Foo
s0 ~ s1 -- injectivity of Foo's arguments
-- REJECTED: cannot instantiate `s0` with `s1`
-- we don't even reach the point where the escape check is taken place:
a0 ~ (Bar s0 Char) -- would fail due to s0 ~ s1

据我所知，刚性类型变量（skolem 常量）只能包含在自身之下或与不允许前者逃脱其范围的元（统一）类型变量统一，即元电视不能是在刚性电视最初被设计的范围内免费。因此，s0 ~ s1 应该被拒绝，因为两个不同的 skolem 不能被实例化，对吧？

但是，当我解释错误消息时，GHC 到达了转义检查。我的统一步骤是错误的还是我误解了错误消息？

【问题讨论】：

到目前为止我唯一的想法：Skolems 一方面在类型推断/泛化过程中表现不同，另一方面在 application.on 事件中表现不同。在后一种情况下，它们不那么严格，即可以专门化。
不确定这到底是什么系统，但似乎在应用程序判断中对论点进行了分析。如果你实例化它，你最终会检查例如Foo a1 (Bar a1 Char) 对 Foo s1 a0，给出了a1 = s1 和a0 = Bar a1 Char，错误是s1 出现在完全替换的Bar s1 Char 中。（没有s0，我只是让你的名字保持不变以避免混淆。）
@Jon 我同意，在包容开始之前的 skolemization 没有意义。奇怪的是，我的算法适用于 20 多种不同的统一，得到的结果与 GHC 相似。非常感谢！

标签： haskell type-systems unification higher-rank-types

【解决方案1】：

写出我的评论作为答案，因为我猜它有帮助。 :)

我相信您的错误在于将应用程序中的论点弄错了；相反，它应该用一个新的元变量来实例化（我将为元变量写一个抑扬符，为 skolem 常量写一个粗体）：

有趣：∀一个。 (∀b.Foo b a) → a

arg : (∀c.Foo c (Bar c Char))

[-₀/a]((∀b.Foo b a em>) → a) = (∀b.Foo b -₀) → -₀

~~Foo c（条形 c 字符）~~

[a₁/c](Foo c (Bar c Char)) = Foo →₁ (Bar →₁ Char)

那么，在子类型判断中：

... ⊢ Foo ∀₁ (Bar ∨₁ 字符) ≤: ∀b。 Foo b Ⅴ₀

您仍然像往常一样对右侧的 ∀ 绑定变量进行 skolemise：

…, b ⊢ Foo →₁ (Bar →₁ 字符) ≤: Foo b ‼₀

这通过生成性给出了 Foo = Foo，但是 解决了 →₁ 到 b 通过注入性，并解决了-₀ 到 Bar -₁ 字符。当退出量词的范围时，这会正确地给出发生检查失败，因为替换类型 [→₁=b](Bar â₁ Char) = Bar b Char 包含 skolem 常数 b。

我说“skolemise”是因为它确实引入了一个类型常量，但它也可以被认为只是进入量词的范围（如“Complete and Easy”中），不一定执行深度 skolemisation。

【讨论】：