采用 类型与类型判断 的七条规则， 不完整的规格 中的三个类型检查问题都有明确答案． T-If 的三个前提都必须成立，因此 $\text{else}$ 分支即使永远不执行也要检查； 两个分支的类型使用同一个元变量 $𝑇$，“类型相同”指字面一致，不做自动转换； 检查器拒绝 $𝑡$ 意味着不存在 $𝑡:𝑇$ 的推导，具体是哪条规则的哪个前提搭不上，可以从搭建推导的过程中直接读出来（方法见 从失败的推导里读出错误位置 ）．