“广义代数数据类型GADT还允许构造器只生成 或 。匹配时由结果类型得到分支局部等式，使 按索引返回整数或布尔值；这些等式不允许跨分支累积，检查也需明确的刚性签名。”
形式陈述
广义代数数据类型GADT允许同一类型构造器的不同构造器返回不同参数实例。普通代数数据类型的构造器通常统一返回T a；GADT可以让某个构造器只返回T Int，另一个只返回T Bool。匹配构造器时，这些结果类型提供分支局部的类型等式。
固定带Int、Bool、函数和模式匹配的ML式核心，定义
text
data Expr a where
Lit : Int → Expr Int
Truth : Bool → Expr Bool
Add : Expr Int → Expr Int → Expr Int
Less : Expr Int → Expr Int → Expr Bool
If : ∀a. Expr Bool → Expr a → Expr a → Expr a索引a是类型参数，不是运行时整数。构造Expr值时，按普通函数应用规则检查构造器参数；例如Add的两个子表达式都必须是Expr Int。
消去时，设被匹配对象已知为Expr α。某分支构造器的结果为Expr T，则在该分支假设
本页采用明确注解的检查纪律：匹配对象的索引和目标结果类型来自已知签名，外层全称变量是刚性的；分支等式是模式提供的局部证据。合一可用于分解构造器类型等式，但不等于把所有刚性变量交给普通推断任意求解。实际系统也可用显式等式约束或类型强制表示这些证据。
直觉
一棵普通语法树告诉你节点叫“加法”或“小于”。GADT还让构造器向类型系统保证：加法节点的两个孩子能产生整数，小于节点会产生布尔值。
当求值器看见Lit，便同时知道当前表达式的结果类型是Int，所以返回其中的整数合理；看见Less，就知道结果类型是Bool，所以返回比较结果合理。模式不是在运行时猜测一个未知值的类型，而是在揭开构造时已经受检查的证据。
例子与边界
一个无需通用Value包装的求值器
给出显式签名
text
eval : ∀a. Expr a → a
eval e =
match e with
| Lit n -> n
| Truth b -> b
| Add p q -> eval p + eval q
| Less p q -> eval p < eval q
| If c p q -> if eval c then eval p else eval q检查时先取任意刚性α，输入e:Expr α，目标结果为α。逐分支的账本为：
| 分支 | 局部等式 | 子表达式类型 | 分支结果 |
|---|---|---|---|
| Lit n | α≡Int | n:Int | Int，经等式视作α |
| Truth b | α≡Bool | b:Bool | Bool，经等式视作α |
| Add p q | α≡Int | p,q:Expr Int | 两次递归各得Int，相加得Int |
| Less p q | α≡Bool | p,q:Expr Int | 两次递归各得Int，比较得Bool |
| If c p q | 构造器参数β与α相等 | c:Expr Bool，p,q:Expr α | 条件得Bool，两支各得α |
eval在Less分支中以Int实例递归，而当前输入结果索引是Bool；在If中又以Bool和α分别递归。因此完整全称递归签名也承担多态递归的检查责任。
从构造到结果的一次完整运行
取
text
e = If (Less (Lit 2) (Lit 5))
(Add (Lit 7) (Lit 4))
(Lit 0)Less子树类型是Expr Bool。Add子树和Lit 0都为Expr Int，故If实例化为Int，整个e:Expr Int。运行先比较2<5得到true，再计算7+4得到11，不执行else分支；eval e:Int，结果11。
若把else改成 Truth false，If要求两支同为Expr a，却得到Expr Int和Expr Bool，构造e时就失败。无需等到eval运行后再把一个布尔结果错误地当整数使用。
如果改写求值器，让 Less p q -> 0，匹配会给出α≡Bool，目标因而是Bool，整数0不符合，分支检查失败。GADT不是允许不同分支随意返回不同类型；它要求每个返回值都满足该分支所学到的索引等式。
等式不能跑到分支外
Lit分支知道α≡Int，不代表eval的全称α从此都是Int。检查Truth分支时需要重新从原环境开始，再加入α≡Bool；若把前一分支的替换全局保留，就会错误地产生Int=Bool冲突，或把整个eval不当地专门化。
一个只接收Expr Int的函数若列出Less分支，则构造器结果Expr Bool与输入Expr Int矛盾。对本页互异基础类型，能据此认定该分支不可达。完整GADT语言的覆盖检查可能更复杂；这里的简单矛盾判断不等于宣称所有索引可达性都容易决定。
推论与应用
如果去掉索引，改成单一 RawExpr，一个同时处理整数和布尔结果的普通求值器通常返回 Value = VInt Int | VBool Bool，并在加法处检查孩子是否真为VInt。GADT把这项结构正确性前移到构造和类型检查阶段，让eval的返回类型直接对应输入索引。
注解同样重要。按期待类型检查为匹配提供明确的Expr α和结果α；若检查器还在猜它们，什么时候可利用分支等式会影响推断顺序与可预测性。实际ML/Haskell系统因此采用特定的刚性注解、局部抽象类型或约束求解纪律，不能从这份已标注求值器推断“所有GADT程序都有HM式主类型”。
这里的索引等式与依赖模式匹配有共同思想，但本页没有让类型依赖任意项，也没有引入Vec长度motive或一般依赖消去子。它给出的具体新增能力是：在ML式类型参数上，通过构造器结果类型获得局部等式，并据此检查普通函数体。
本单元终点题解把这份Expr接口与可变缓存、多态参数和Eq字典放到同一小库中，逐项检查它们各自需要的证据，避免把不同扩展的规则混用。
参考资料
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Geoffrey Washburn, “Simple Unification-Based Type Inference for GADTs,” ICFP, 2006, 50–61；作者机构托管草稿，§§2–4：构造器结果类型、刚性注解与局部精化
- Microsoft Research论文记录：正式发表信息及作者稿入口