为 类型与类型判断 中的类型判断寻找推导时， 从要证的结论出发，选一条结论形状对得上的规则，再去搭它的每个前提． 这七条规则是语法导向的，每个子项的候选规则由语法形状确定， 见 反演 ． 由于 T-If 有三个前提，推导搜索会分出三个分支，形成一棵树． 按指定的检查顺序，可以定位首先失败的前提；这条诊断包含三样信息： 断在哪个子项上的位置（搭推导时每进入一个前提就进入一个直接子项，断点对应语法树上的一个节点）， 断点上方最后一次成功选用的规则与前提（以及它的哪一个前提搭不上）， 还有那个前提要求的类型与子项实际能得到的类型之间的期望与实际对照．

以 $\text{if }\text{ true }\text{ then }0\text{ else }\left(\text{iszero }0\right)$ 为例， 按条件、$\text{then}$ 分支、$\text{else}$ 分支的顺序检查． 最外层选 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, found Bool expected Nat, found Bool ，内容就是这三样信息． 若先用 $\text{else}$ 分支确定 $𝑇=\text{ Bool}$，也可以报告 $\text{then}$ 分支的 $0$“期望 $\text{Bool}$，实际 $\text{Nat}$”； 首先报告哪一处，取决于检查顺序，不由语法导向性单独决定．

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