采用 [定义] 类型与类型判断 的七条规则， [例] 不完整的规格 中的三个类型检查问题可以得到明确回答：

1. T-If 的三个前提都必须成立，所以 else 分支即使永远不执行也要检查。
2. 两个分支的类型用的是同一个元变量 $𝑇$，所以“类型相同”就是字面相同，没有自动转换。
3. 检查器拒绝 $𝑡$，意思是不存在 $𝑡:𝑇$ 的推导。具体是哪条规则的哪个前提搭不上，可以从搭建推导的过程中读出来，方法见 [附注] 从失败的推导里读出错误位置 。