“模式匹配终点提供树IR、槽父表、23条回溯字节码和逐输入对照。覆盖检查还能在编译前给出遗漏值与被遮蔽行；两者的职责不同，诊断全表穷尽并不能证明生成的绑定位置正确。”
形式陈述
入口先给类型和值的范围
代数数据类型用构造子区分形状，例如Bool有F、T，List有Nil和Cons(Bool,List)。本页处理有限种类、每类有限多个且有限元数的构造子；输入值是已经求值的、有限、不可变且良类型的构造树。List的长度没有统一上限，但每次给出的列表都有限。
每个涉及的类型须在算法入口提供一个经过类型检查的有限默认值。 例如Bool提供F，List提供Nil。它用于把未受约束的字段补成实际反例；不能把空类型的“不存在值”当作默认值。类型方程Loop=Again(Loop)没有有限构造值，不满足这份入口合同。本文不处理GADT索引约束、惰性底值、无限常量签名、视图模式或guard。[1, §2]
模式由通配符_、变量、构造子模式c(p₁,…,pₐ)和or模式p|q组成。每个普通模式分支中的变量只出现一次；or两臂绑定相同名字且类型一致。覆盖检查只问能否匹配，因此把变量视为通配符；动作里的变量绑定则由编译阶段保留。
把多列模式排成矩阵P，每行宽度都是n；值向量v和候选行q也有n项。记p≼v表示每项都结构匹配，P≼v表示至少一行匹配。定义有用性：
算法返回这样的具体v，或返回None表示不存在。第i行被早行遮蔽，恰当且仅当U(P₍₁…i−1₎,pᵢ)为假；全表穷尽，恰当且仅当U(P,(,…,))为假。这两个诊断共享一个接口，却分别使用前缀矩阵和完整矩阵。[1, §3]
两个矩阵操作
先把P中的or按从左到右的替代展开为普通模式行。候选q若含or，也展开成q¹,…,qʳ：依次调用单候选过程W(P,qʲ,T)，任一调用给出见证便返回它，全部返回None才判q无用。候选各替代代表集合并，不是要求同一值同时匹配所有替代。覆盖只看集合，但保留展开顺序便于和首匹配执行核对。展开可能很大，不能把它当作免费的一步。下载器用显式栈遍历连续or节点，并向同一结果列表追加；构造子字段才取笛卡尔积，因此不会逐层复制左嵌套or的结果前缀。
在第一列观察构造子c，元数为a。特化S_c(P)逐行执行：c(r₁,…,rₐ)换成r₁,…,rₐ；通配符换成a个通配符；其它构造子行删除。原来的其余列接在后面。特化把“这一项已知是c”变成对子字段的检查。
默认矩阵D(P)只保留第一项为通配符的行，并删除这一项。它描述第一项取一个尚未出现在该列的构造子时，还可能匹配的行。特化和默认都不改变保留下来的行序。[1, §3.1]
直觉
问的是有没有剩下的一块
一个模式代表一批值。Cons(_,_)代表全部非空列表，Cons(T,_)只代表首项为T的非空列表。新行是否有用，不是看它的文字和旧行是否相同，而是看它是否还覆盖到旧行联合之外的值。
例如前两行分别匹配F和T，第三行_虽然与两行都不相同，却没有剩余值可接收。相反，前两行若只有Nil和Cons(T,_)，还剩首项为F的列表。Cons(F,Nil)是可以直接交给程序执行的证书。
缺一个构造子时，为何只查默认矩阵
设第一列已经出现的根构造子集合为Σ。如果Σ没有覆盖该类型的完整签名，可以选一个未出现的c。它不会匹配任何以已有构造子开头的行，剩下的阻碍只有通配符行；这些行对其余列的要求正是D(P)。
反方向也成立：如果某个完整向量没被P覆盖，那么其余分量不可能被D(P)覆盖，否则原来的通配符行已经匹配它。因此，在候选第一项为通配符时，D(P)有剩余值与原问题有剩余值等价。默认字段见证保证选出的c真的能构成值，而不只是一个空壳符号。
例子与边界
两列匹配的漏例与遮蔽行
令第一列是List，第二列是Bool，按从上到下首匹配执行：
| 行 | 列表模式 | 标记模式 | 动作 |
|---|---|---|---|
| 1 | Nil | _ | empty |
| 2 | Cons(T,xs) | F | take-tail |
| 3 | Cons(,) | T | flagged |
| 4 | Nil | T | shadowed |
第四行永远不会成为第一个匹配行：凡它匹配的输入，第一行已经接收。可是删掉第四行并不能修好穷尽性；输入(Cons(F,Nil),F)仍不匹配前三行。
从全通配符候选开始，第一列出现Nil和Cons，签名完整。Nil特化后第一行已经是全通配符，没有漏例。Cons特化得到三列“头、尾、标记”：第二行是(T,_,F)，第三行是(_,_,T)；Nil行删除。
此时头的已出现构造子只有T，不完整。默认矩阵留下第三行的(_,T)，检查“尾、标记”。尾列全是通配符，继续默认到标记；标记只出现T，于是选缺失的F。回填未受约束的尾Nil、缺失的头F，最后恢复Cons，得到(Cons(F,Nil),F)。
在末尾Nil/T之前补入Cons(F,_),F → false-head，全表就穷尽了。新行见证是刚才的漏例，末尾Nil/T仍被遮蔽。修补遗漏与删除死行是两个独立编辑，不能把警告数量减少当作已经做对两件事。
guard不能直接擦掉
_ when false → a在结构上覆盖所有值，实际没有值能进入动作a。如果分析器擦掉guard，把这一行当作普通_，就会错误地宣称后面的每一行都无用。要分析guard，需要另一个能描述其条件的抽象接口；本页返回的结论只针对无guard矩阵。
依赖模式匹配还会从构造子推出索引等式，例如长度为后继数的Vec不能是nil。这里的普通签名特化没有求解这种等式，也不能把“语法上有这个构造子”直接当作“在当前索引下可构造”。
推论与应用
可以执行的递归规则
记W(P,q,T)为返回见证的过程，T是各列类型。无行时直接按q构造值：构造子递归保留，通配字段用入口默认值。没有列时，空矩阵返回空向量()；存在空行则返回None。空向量是一份合法见证，与None不同。
若q第一项是c(r₁,…,rₐ)，递归检查S_c(P)及候选(r₁,…,rₐ,q₂,…,qₙ)。成功时把返回的前a个值重新装进c，其余值恢复为后续列。
若q第一项为通配符且Σ完整，依固定构造子顺序检查所有S_c(P)，候选的首项换成该构造子的a个通配字段。第一个成功分支重建出见证；全部失败才返回None。若Σ不完整，只递归D(P)与候选尾部；成功时选缺失构造子，用默认值填其字段，再接上尾部见证。
正确性逐步来自特化保持匹配关系，以及前述默认分支等价。重建出的值既匹配候选，又避开全部旧行；返回None时，每个允许构造子情形均已排除。它证明的是所有符合模型的有限值，不是只证明下载器枚举过的列表长度。
递归类型不会让算法无限展开
对展开后的P、q，取二元量：所有模式中显式构造子节点的总数，以及当前列数，按字典序比较。候选构造子特化至少去掉候选的一个构造子；完整签名分支至少去掉P中一个根构造子。由通配符产生的新字段仍是通配符，不增加显式构造子数。
默认步骤若删掉构造子行，第一项严格减小；若第一列全是通配符，则第一项不变而列数减一。因此每次递归都严格下降。类型List在字段中再次出现，不会要求把一个通配尾部无限展开：没有显式构造子要求时，算法使用默认步骤直接移走该列。
成本按展开与实际分支收费
令A为输入行、模式节点和列槽的总编码规模，E为or完全展开后矩阵及候选的总模式规模。E可能对A呈指数增长。下载器的类型/变量良构校验会合并变量字典，保守最坏O((A+1)²)，默认见证的读取与检查另计；它不属于下面的矩阵递归成本。
固定本例Bool/List签名后，记每次实际递归调用的矩阵尺寸为m_j×n_j，令B=Σ_j(m_j+1)(n_j+1)。特化、复制行尾和默认提取的总工作为O(E+B)，连同展开输入读取计O(A+E+B)。返回值的展开打印按实际输出字节另计。完整签名分支会复制通配行，不能据几个快速样例承诺整个分析总是线性或二次。[1, §7.1]
模式匹配终点先提交漏例和逐行见证，再交决策树与回溯字节码。诊断不替代执行正确性：后两项还要保留第一个动作及变量绑定，而不只是保持“总有某行能匹配”。
参考资料
- Luc Maranget，Warnings for pattern matching，Journal of Functional Programming17(3)，2007，pp.387–421；§2非空类型前提与模式，§3有用性及特化/default，§5遗漏见证，§7.1复杂度。本文固定有限签名，并要求显式有限默认值；具体两列表和执行器为自行构造。
- Luc Maranget，Compiling Pattern Matching to Good Decision Trees，ML2008，pp.35–46，作者含附录稿§§2–5：有序模式矩阵、位置与特化的语义对应。覆盖集合与首匹配编译的不同验收目标由这两个接口区分。