Gleam 如何判断一个 case 是否穷尽

📋 概述

这是一篇带读者走进 Gleam 编译器内部的长文，主题是 compiler-core/src/exhaustiveness.rs 的工作：在编译期判断 case 表达式的每个模式是否覆盖了主语所有可能取值，反过来也判断某个分支是否永远不会被命中。作者从 1984 至 1985 年 Lennart Augustsson 的《Compiling Pattern Matching》讲起，指出其框架是后续工作的基础——把 case 的子句按首要构造子分组，为子部分引入新变量，然后递归。Gleam 的实现在此之上做了拆解：Augustsson 的跳转同时承担了「继续在嵌套里匹配」和「失败」两件事，而 Gleam 把它们分成 Switch 与 Decision::Fail 两种类型。这样，若树建好后能在编译期发现 Fail，就证明原 case 不穷尽；再借助 missing_patterns.rs 沿树回溯，定位到那个永远无法匹配的具体情形并回报给用户，也就是 Maranget 2007 年论文里称作「witness（反例）」的东西。作者赞叹 Gleam 能直接告诉你「缺失的模式是：False」这类精确提示，是一种出色的用户体验。