为 [定义] 类型与类型判断 中的类型判断寻找推导时，从要证的结论出发，选一条结论形状对得上的规则，再去搭它的每个前提。这七条规则是语法导向的，每种项形状只对应一条规则，见 [引理] 反演 ，所以每一步都只有一条规则可选，整个过程是一条确定的路径。路径断掉的地方，就是错误所在，它由三样东西确定：

• 位置：断在哪个子项上。搭推导时每进入一个前提，就进入了项的一个直接子项，所以断点对应语法树上的一个节点。
• 规则与前提：断点上方最后一次成功选用的规则，以及它的哪一个前提搭不上。
• 期望与实际：那个前提要求的类型，和子项实际能得到的类型。

以 $\text{if }\text{ true }\text{ then }0\text{ else }\left(\text{iszero }0\right)$ 为例。最外层选 T-If；第一个前提 $\text{true }:\text{ Bool}$ 由 T-True 搭上；第二个前提要求 $0:𝑇$，T-Zero 给出 $𝑇=\text{ Nat}$；第三个前提于是要求 $\text{iszero }0:\text{ Nat}$，但 T-IsZero 的结论类型是 $\text{Bool}$。断点因此是：T-If 的第三个前提，子项 $\text{iszero }0$，期望 $\text{Nat}$，实际 $\text{Bool}$。编译器的报错信息“expected Nat Nat , found Bool Bool ”，内容就是这三样东西。

Rust 检查器 type_of type_of 在失败时只返回 None None ，把这些信息丢掉了。要保留它们，只需把返回类型从 Option<Type> Option<Type> 换成 Result<Type, Error> Result<Type, Error> ，在每个 ? ? 和比较失败处记下当时的规则、子项和两个类型。