依赖模式匹配

普通模式匹配只回答“值是哪一个构造器”；依赖匹配还回答“既然是这个构造器，先前未知的索引现在必是什么”。构造器像一张带约束的收据：看到 nil，不仅知道没有元素，也知道长度必须是零。分支类型因此会随着匹配结果移动，某些表面组合则因索引矛盾根本没有居民。

coverage 的任务不是枚举语法上所有构造器笛卡尔积，而是枚举可达到的依赖状态。所谓 impossible clause 也不是程序员的一句愿望；检查器必须用构造器可辨识性、无混淆性或索引统一证明该状态为空。这样的证明若失败，省略分支就会把总函数伪装成部分函数。

非空向量的表头函数可写成

唯一实质子句是

head n (cons n a xs) = a

nil 的结果索引为 $0$，但预期索引为 $\mathsf{succ}(n)$；自然数构造器无混淆性排除 $0\equiv \mathsf{succ}(n)$，故该分支不可达。相反，若函数参数只是 $v:\mathsf{Vec}(A,n)$，nil 分支可在 $n=0$ 时出现，不能仍以“看起来想处理非空向量”为由删除。

更能显示联合精化的是

首个向量匹配 nil 后 $n$ 精化为 $0$，第二个向量只能是 nil；首个为 cons 后，第二个也只能是同一后继长度的 cons，递归调用落到共同前驱。诸如 zip nil (cons b bs) 的交叉子句并非遗漏，而是索引冲突。这个例子不能机械改成两个普通列表：失去共享索引后，长度不等的分支重新变得可达，函数必须决定截断或报错。

另一个边界是相等证明匹配。若编译器允许对 $p:x{=}_{A}x$ 做不受限的 refl 匹配，并在 index unification 中删除 $x=x$ 约束，可能获得 K/UIP。保持高阶恒等结构的系统会限制这种 deletion 或要求更精细的 coverage；因此接受某段 pattern syntax 取决于 with-K/without-K 一类理论选择，不能只由表面穷尽性决定。

依赖模式匹配使按长度、语法类型、协议状态索引的数据可用接近普通函数语言的方式编程。它可从构造器形状自动恢复等式约束，减少手写 transport；编译所得 case tree 还能供覆盖警告、不可达代码诊断和后端生成复用。可靠的 elaborator 最终仍提交小核心项，因此复杂匹配算法不必进入可信内核。

这种便利不会消除 motive 设计。返回类型若依赖被匹配值，编译器必须推断或由注解获得 motive；重叠模式还要证明选择顺序不改变声明式含义。加入 view pattern、guard 或一般递归后，coverage、可达性与终止性可能分别失效，应按独立检查报告，而不是用一次“pattern match accepted”概括全部保证。