按 [定义] 一步归约 的 E-IfTrue，$\text{if }\text{ true }\text{ then }0\text{ else }\text{ false}$ 运行一步就得到值 $0$，不会受阻；但 [定义] 类型与类型判断 无法给它类型，因为 T-If 要求两个分支类型相同。这不是 bug。类型系统不运行程序，只看形状，它只能做近似。 [推论] 类型安全 只保证一个方向：良类型的程序不受阻；它没有保证“不受阻的程序都良类型”。