高秩多态与局部检查

一个接口说“给我一把能开任意盒子的钥匙”，与“你先选一个盒子，再给我开它的钥匙”不同。前者能在一次调用中用同一个参数处理Int和Bool；后者只保证参数适用于本次已经选定的那个类型。

普通let多态允许在环境中保存一份方案公理库类型方案Type scheme · Polytype通过显式量化类型变量表示一族单态类型的多态对象。，但传统HM的λ参数通常是单态的。把已经多态的id传入一个普通λ参数，不会自动让该参数在函数体中变成多态；需要在接口上保留这个量词。

一个参数，在同一次调用中用两种类型 ​

定义

accept : (∀a. a → a) → Int × Bool
accept = λ(f : ∀a. a → a). (f 5, f true)

检查第一处f时，从方案得到新鲜α→α；实参5要求α=Int，因此第一项是Int。检查第二处f时，重新得到β→β；true要求β=Bool，因此第二项是Bool。α和β不是同一个未知量，最终二元组符合Int×Bool。

给定 id:∀a.a→a，accept id合法并得到 (5,true)。也可把 λx.x按期待的全称参数类型检查：引入刚性b，在x:b下有x:b，因此λx.x:b→b；b没有逃逸，量词检查成功。

若把accept签名换成 $\mathrm{\forall }a.(a\to a)\to \mathrm{Int}\times \mathrm{Bool}$，检查体时a是一个固定的任意类型，f只有a→a。第一处使用要求a=Int，第二处要求a=Bool，无法成立。这个签名本身不是空类型，例如忽略f而返回 (5,true)就可实现它；只是它不足以支持当前函数体的两种调用。

刚性检查拒绝冒充通用函数 ​

λx.x+1可以是Int→Int，却不能作为accept的参数。按 $\mathrm{\forall }a.a\to a$ 检查时，x的类型是新鲜刚性b，加法要求b=Int。由于b代表任意类型而非待选类型，这一步失败。

再看一个更隐蔽的逃逸例：

λg. (g : ∀a. a → a)

本页规则给无注解的λ参数g一个单态未知β。检查内部注解时引入刚性b，要求g:b→b。如果普通合一直接写下β=b→b，就把一个只在内部量词检查期间存在的b塞进了外层g的类型。离开该检查范围后b失去作用域，所以这个解必须拒绝。

正确的修复是把接口明确写成 λ(g:∀a.a→a).g，使g一开始就携带全称方案，而不是借内部注解把一个单态参数升级成任意多态值。实现常为未知量记录创建层级，或在返回时检查自由刚性变量，以发现这种逃逸。

高秩与impredicative不是同义词 ​

把 $\mathrm{\forall }a.a\to a$ 直接写在accept的参数位置是高秩。另一个操作是拿普通 id:∀t.t→t，把t实例化为 $\mathrm{\forall }a.a\to a$，从而让id接收并返回一个多态值；这属于impredicative实例化，本页选择的规则不允许它。

即使两个程序在显式System F中都能表达，面向推断的语言也可能只支持前一种。遇到拒绝时，应先检查是否真的需要多态实例化，而非仅仅缺一个高秩参数注解。

高秩接口可以让库函数重复使用调用者提供的通用操作，也可以把一个类型变量限制在局部计算内部。无论应用场景是什么，检查机制都要保持同一原则：引入∀时使用任意刚性变量，消去∀时才选择实例。

注解驱动的检查把困难集中在边界。知道参数需要 $\mathrm{\forall }a.a\to a$ 后，就可以分别检查函数体和实参；并不需要猜测每个无注解λ参数是否应当多态。本页没有声称给出了所有高秩语言的完整推断算法，量词下潜、subsumption和类型应用的选择会随具体系统不同。

调试时可为每个类型变量记下三个信息：谁绑定它、它是刚性还是可解、哪个作用域允许使用它。例子中的Int/Bool两次实例化与β=b→b逃逸，分别检验实例独立性和作用域保持；仅看最终类型字符串很容易漏掉后者。