Unison 语言普遍量化类型字段模式匹配修复解读：fix6018 转录测试与子类型检查原理
Unison 语言普遍量化类型字段模式匹配修复解读：fix6018 转录测试与子类型检查原理
导读
本文围绕 Unison 开源仓库中编号为 6018 的问题修复转录测试（fix6018.md），深入讲解「在数据类型构造器内部存放普遍量化（universal/rank-n）类型字段，并在模式匹配中解构该字段」这一能力是如何被验证的，以及它曾被模式检查器（pattern checker）中的反向子类型检查（backwards subtyping checks）所阻碍的原因。读完本文，你将理解 Unison 中 rank-n 类型字段的书写方式、子类型检查在类型检查器中的实现位置，以及如何通过转录测试体系回归验证此类修复。
一、问题背景：从 issue 6018 到回归测试
Unison 采用「转录测试」（transcript tests）作为语言行为回归验证的主要手段：每个 .md 文件包含一组 Unison 代码块与对应的 UCM（Unison Codebase Manager）命令，运行时会加载代码、执行命令，并把实际输出与文件中预置的输出进行比对。这类测试文件统一存放在 unison-src/transcripts/idempotent/ 目录下，其中以 fixNNNN.md 命名的一系列文件专门用于锁定历史上各 issue 的修复行为，避免将来重构时再次引入同样的缺陷。
fix6018.md 正是这样一个回归测试。它开篇就点明了主题：
Checks that pattern matching against a universal type inside a data type works. This was intended, but was stymied by backwards subtyping checks in the pattern checker.
翻译过来即：本测试用于确认「对数据类型内部存放的普遍类型进行模式匹配」可以正常工作；这一行为本来是设计预期的，但一度被模式检查器中的反向子类型检查所阻碍。整个修复围绕这一处缺陷展开。
二、转录测试内容：最小复现与期望行为
2.1 被测代码
fix6018 的测试主体只有两段代码：
type T r = T (forall x. (x -> r, x))
runT = cases
T (f, x) -> f x
第一行定义了一个数据类型 T r，其唯一构造器 T 携带一个字段，字段类型是普遍量化的 forall x. (x -> r, x)——即一个二元组，第一个元素是从任意类型 x 到 r 的函数，第二个元素是 x 类型的值。注意这里的 forall 出现在构造器字段内部，也就是说字段本身是一个 rank-n 类型：T 的字段并不局限于某个具体 x，而是「对任意 x 都成立」的类型。
第二行 runT 通过 cases 对 T 进行模式匹配解构：T (f, x) -> f x 把字段元组绑定为 f 与 x，然后直接应用 f x。由于 f : forall x. x -> r，把它应用到任意 x 上都是合法的，因此 runT 的类型应当被推导为：
runT : T r -> r
这正是 UCM 加载该代码后的输出：
+ type T r
+ runT : T r -> r
Run `update` to apply these changes to your codebase.
也就是说，修复之后，这种「在数据类型里存普遍量化类型、再通过模式匹配把多态函数绑定出来使用」的写法被接受，并且类型被正确推断为 T r -> r。
2.2 测试的要害之处
这个测试虽然短小，但它的关键点在于：模式匹配解构时，被普遍量化的字段变量在绑定过程中必须保持其多态性（rank-n 语义），不能被错误地实例化或被子类型检查按普通量词的方向处理。测试文件明确指出，阻碍这一行为的正是模式检查器中的「反向子类型检查」。
也就是说，在修复之前，模式检查器在处理 T (f, x) 这类解构时，会对绑定变量 f、x 的类型与被匹配字段的普遍量化类型做子类型方向判断；若方向判断有误（"backwards"），合法的多态字段绑定就会被误判为类型不兼容而拒绝，导致 runT 无法通过类型检查。
三、源码佐证：子类型检查在 Unison 类型检查器中的实现
为了理解「反向子类型检查」具体落在何处，需要回到 Unison 类型检查器的源码。
3.1 subtype 与 isSubtype
Unison 的类型检查器位于 parser-typechecker/src/Unison/Typechecker/Context.hs。该文件中核心的子类型关系检查函数定义如下：
-- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.
subtype :: forall v loc. (Var v, Ord loc) => Type v loc -> Type v loc -> M v loc ()
subtype tx ty = scope (InSubtype tx ty) $ do
（见 Context.hs）subtype 在 t1 是 t2 的子类型时成功返回，否则报错；它在执行时会把检查记录为一条约束 InSubtype (Type v loc) (Type v loc)（该约束构造子在 Context.hs 定义），便于后续错误报告定位具体的子类型失败位置。
对普遍量化类型而言，subtype 的实现需要正确处理量词与方向：当两个类型中某一侧被普遍量化时，量词对应的「实例化方向」必须符合 rank-n 类型的语义——这正是文档中所说容易出错的地方。与之配套的还有纯检查版本：
-- Check if `t1` is a subtype of `t2`. Doesn't update the typechecking context.
isSubtype' :: (Var v, Ord loc) => Type v loc -> Type v loc -> TotalM v loc Bool
以及对外暴露的 isSubtype 公共接口（Context.hs）。
3.2 模式匹配覆盖检查模块
「模式检查器」在 Unison 中对应独立的模块目录 parser-typechecker/src/Unison/PatternMatchCoverage/，其中包括：
Constraint.hs：定义模式覆盖检查使用的约束系统，如PosCon/NegCon（数据构造器的正/负约束）、PosLit/NegLit（字面量约束）、PosListHead/PosListTail/NegListInterval（列表结构与长度区间约束）等；Solve.hs：对约束集求解，判断模式是否穷尽、是否存在冗余分支；GrdTree.hs、PmGrd.hs：模式守卫的树形表示；Desugar.hs：把 Unison 源码中的模式翻译成语义明确的模式守卫；EffectHandler.hs：针对能力处理器（ability handler）的模式匹配。
模式匹配覆盖检查与类型检查是协同工作的：subtype 会被类型检查器用于校验被匹配值（scrutinee）的类型是否与模式中使用的字面量、构造器、列表等结构相容（例如 Context.hs 中依次把被匹配类型与 Boolean、Int、Nat、Float、Text、Char、Bytes 做子类型检查）。当被匹配的字段本身是 forall 普遍量化类型时，子类型检查的方向是否正确直接决定了 T (f, x) -> f x 这类代码能否通过。fix6018 修复的正是模式检查路径中子类型方向处理失当的问题。
四、横向参照：更高阶类型（higher-rank types）的既有测试
fix6018 所验证的能力并非孤立存在。同一目录下还有专门的更高阶类型测试 higher-rank.md，其中展示了普遍量化类型字段在模式匹配中保持多态性的更完整场景，可以作为 fix6018 的能力对照：
unique type Functor f = Functor (forall a b . (a -> b) -> f a -> f b)
Functor.map : Functor f -> (forall a b . (a -> b) -> f a -> f b)
Functor.map = cases Functor f -> f
Functor.blah : Functor f -> ()
Functor.blah = cases Functor f ->
g : forall a b . (a -> b) -> f a -> f b
g = f
()
这里 Functor 的构造器同样携带一个普遍量化函数字段，模式匹配 Functor f -> f 把该字段绑定到 f 之后，f 依然保持 forall a b . ... 的多态类型——这与 fix6018 中 T (f, x) -> f x 的原理完全一致。higher-rank.md 还特别指出两种情况的差别：
- 当 lambda 是**被检查（checked against）**一个多态类型时，调用点无需写类型标注，例如
f (x -> x)； - 而当局部定义是**被独立推断（inferred）**时，则需要显式标注才能得到 rank-n 类型，例如
f' : forall t a . ...。
这从侧面印证了 rank-n 类型在 Unison 中的使用惯例：多态性由「检查方向」保证，模式匹配解构出的字段可以延续这种多态性，这正是 fix6018 修复后所确保的行为。
五、验证方式与工程实践意义
5.1 如何查看与运行该测试
- 测试文档本体位于 unison-src/transcripts/idempotent/fix6018.md，代码块使用
unison与ucm :added-by-ucm两种标注，分别表示「待加载的 Unison 源码」和「UCM 自动追加的输出」； - 转录测试的执行入口在 unison-cli/transcripts/Transcripts.hs，它负责加载转录文件、执行 UCM 命令并比对输出；
- 该测试放在
idempotent（幂等）子目录下，意味着重复执行不会改变代码库状态，适合在 CI 中反复回归。
5.2 工程意义
从工程视角看，fix6018 的回归测试价值体现在三点：
- 锁死语义：以最小代码锁定「数据构造器字段可携带普遍量化类型、且模式解构后保持多态」这一语言特性，防止后续对模式检查器或子类型逻辑的重构再次破坏它；
- 指明缺陷根因：测试注释直接指出历史缺陷来自模式检查器中的反向子类型检查，为后续维护者理解该区域代码（PatternMatchCoverage 与 Context.hs 中的
subtype）提供了上下文； - 作为能力文档：
runT = cases T (f, x) -> f x本身就是一个可直接复制到 scratch 文件中体验的最小示例，任何开发者都可以通过 UCM 的run、update命令在本地复现这一行为。
六、小结
fix6018 是一个「小而关键」的语言特性回归测试：它验证了 Unison 支持在数据类型内部存放普遍量化类型字段，并能在模式匹配解构后继续以多态方式使用这些字段。该能力曾被模式检查器中的反向子类型检查所阻碍，而修复后的行为由 fix6018.md 以转录测试的形式固化下来。结合 Context.hs 中 subtype 的实现与 PatternMatchCoverage 模块的约束求解机制，可以清楚地看到：rank-n 类型在 Unison 中不是仅仅停留在函数签名层面的语法糖，而是贯穿构造器字段、模式匹配与子类型检查的完整一等公民能力。