高阶类型子类型疑问：为何σ₁可包含σ₂而σ₃不可？

问题背景 #

我正在学习基于Peyton Jones等人论文《Practical Type Inference for Arbitrary-Rank Types》的高阶类型推导系统，其中4.9.3节重点讨论了子类型关系（ρ₁ ≤ ρ₂）对弱前束范式（Weak Head Normal Form, WNF）的要求。论文给出反例：

• σ₁ = ∀a. a → ∀b. b → ∀c. b → c（弱前束范式）
• σ₂ = Int → ∀c. Int → c
• σ₃ = ∀a b c. a → b → b → c（全前束范式，非弱前束范式）

虽然存在子类型关系⊢dsk σ₁ → σ₂ ≤ σ₃ → σ₂，但仅能推导出⊢⇓ (λx. x 3) : (σ₁ → σ₂)，无法推导出⊢⇓ (λx. x 3) : (σ₃ → σ₂)。

GHC测试验证 #

在GHC中测试以下代码，结果与论文结论一致：

-- GHC接受：test1类型合法
test1 :: (forall a. a -> forall b. b -> forall c. b -> c) -> (Int -> forall c. Int -> c)
test1 = \x -> x 3

-- GHC拒绝：test2类型不合法
test2 :: (forall a. forall b. forall c. a -> b -> b -> c) -> (Int -> forall c. Int  -> c)
test2 = \x -> x 3

核心疑问 #

为何σ₁ ≤ Int → ∀c. Int → c成立，而σ₃ ≤ Int → ∀c. Int → c不成立？这种差异在论文的类型规则中如何体现？

详细解释 #

1. 弱前束范式的定义与作用 #

弱前束范式的核心特点是：顶层全称量词后紧跟非量化类型（如箭头类型），而非将所有量词提前到最外层。论文要求子类型关系的两端必须处于弱前束范式，目的是支持分步实例化量词，而非一次性绑定所有类型变量。

2. σ₁的子类型推导过程 #

σ₁ = ∀a. a → ∀b. b → ∀c. b → c是标准的弱前束范式，推导σ₁ ≤ Int → ∀c. Int → c的步骤如下：

1. 先将右侧类型转换为等价的弱前束范式：Int → ∀c. Int → c ≡ ∀c. (Int → Int → c)（箭头右结合）。
2. 应用子类型规则提取右侧的顶层量词∀c，转化为推导σ₁ ≤ Int → Int → c（c为自由变量）。
3. 实例化σ₁的顶层量词∀a为Int，得到Int → ∀b. b → ∀c'. b → c' ≤ Int → Int → c。
4. 匹配箭头右侧，推导∀b. b → ∀c'. b → c' ≤ Int → c：实例化∀b为Int，得到Int → ∀c'. Int → c' ≤ Int → c。
5. 最后匹配箭头右侧，实例化∀c'为c，得到Int → c ≤ Int → c，子类型关系成立。

3. σ₃的子类型推导失败原因 #

σ₃ = ∀a b c. a → b → b → c是全前束范式，所有量词绑定在最外层，推导σ₃ ≤ Int → ∀c. Int → c时：

1. 同样将右侧转换为∀c. (Int → Int → c)，提取∀c后转化为推导σ₃ ≤ Int → Int → c。
2. σ₃的所有量词∀a b c'（重命名c为c'）必须一次性实例化，无法分步处理。实例化a=Int、b=Int后，得到Int → Int → c' ≤ Int → Int → c。
3. 此时要求c' ≤ c对所有c'成立，但c'是全称量词绑定的任意类型，无法满足对固定自由变量c的子类型约束，推导失败。

4. 论文类型规则中的体现 #

论文的子类型规则（图4的≤规则）明确要求参与子类型比较的类型必须处于弱前束范式：

• 处理箭头类型的子关系时，规则会先递归处理箭头两侧的子类型；
• 处理全称量词时，仅能剥离顶层的单个全称量词，而非批量处理所有外层量词。

全前束范式的类型违反了这一要求，导致无法分步实例化量词来匹配右侧类型的内层约束，最终子类型推导失败。

内容的提问来源于stack exchange，提问作者NisNis