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

问题描述

这是一个刚性类型变量逃离其作用域的规范示例：

{-# 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 常量）只能包含在其自身之下或与不允许前者脱离其范围的元（统一）类型变量统一，即元 tv 不能是在刚性电视最初被 skolemized 的范围内免费。因此，应该拒绝 s0 ~ s1，因为无法实例化两个不同的 skolems，对吗？

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

解决方法

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

我认为您的错误在于对申请中的论点进行了讨论；相反，它应该用一个新的元变量实例化（我将为元变量编写一个抑扬符，为 skolem 常量编写粗体）：

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

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

[â₀/a]((∀b.Foo b a) → a) = (∀b.Foo b â₀) → â₀

Foo c (Bar c Char)

[â₁/c](Foo c (Bar c Char)) = Foo â₁ (Bar â₁ Char)

然后，在子类型判断中：

…⊢ Foo â₁ (Bar â₁ Char) ≤:∀b。 Foo b â₀

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

...,b ⊢ Foo â₁ (Bar â₁ Char ) ≤: Foo b â₀

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

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