固定一套类型规则和语境 $\mathrm{\Gamma }$，考虑类型判断 $\mathrm{\Gamma }⊢𝑡:𝑇$． $\mathrm{\Gamma }$ 记录变量的类型假设，记号见 类型与类型判断 ． 围绕同一套类型规则，按给定什么与要找什么可以区分三类问题：

把 良类型 的良类型定义写成带语境的形式， 问的就是：固定词项，是否存在类型，即 $\exists 𝑇.\mathrm{\Gamma }⊢𝑡:𝑇$． 居留性问的是：固定类型，是否存在词项，即 $\exists 𝑡.\mathrm{\Gamma }⊢𝑡:𝑇$． 注意两个存在量词的位置： 类型推理给定词项求类型； 居留性判定给定类型问是否存在词项，若还要返回一个居留者，就进一步成了构造词项的问题．

以 类型与类型判断 的七条规则为例： 检查给定的 $\text{pred }0:\text{ Nat}$，答案是成立，而检查 $\text{pred }0:\text{ Bool}$ 则不成立； 推理给定项 $\text{pred }0$ 的类型，可以直接得到 $\text{Nat}$，无需调用者预先提供类型； 判断 $\text{Nat}$ 是否可居留时，$0:\text{ Nat}$ 提供了见证，判断 $\text{Bool}$ 是否可居留时，$\text{true }:\text{ Bool}$ 提供了见证． 虽然这两种类型都可居留，但还是存在没有类型的词项，比如 $\text{succ }\text{ true}$ 就属于不良类型．

Rust 算法 type_of(t) -> Option<Type> type_of(t) -> Option<Type> 按输入与输出划分是推理接口：给它词项，它返回类型． 它也常广义地叫作“类型检查器”，因为它同时判定项是否良类型． 带期望类型的检查接口则是 check(t, expected) -> bool check(t, expected) -> bool ． 在这套规则下，可以用 type_of(t) == Some(expected) type_of(t) == Some(expected) 实现它； 这依赖 类型唯一 ， 以及算法相对规则的 算法可靠性 与 算法完备性 ． 实际的检查器也可以交替使用检查与推理； 接口的区分，不要求实现拆成两套互不相干的算法．

常见误解

不少人以为检查失败就说明这个项没有任何类型． 检查针对的只是某个给定类型： $\text{pred }0:\text{ Bool}$ 不成立，只排除了 $\text{Bool}$，这个项仍有类型 $\text{Nat}$． 要断定一个项不良类型，必须排除所有可能的类型，不能把“不等于期望类型”当成“没有类型”．

也有人认为推理器没有给出类型，就证明规则里不存在类型． 把算法的拒绝解释成“规则无法定型”，需要相对规则的完备性． 在 算术语言形式化的未展开前提 的实现假设下， 这里的 type_of type_of 终止且相对规则完备，所以正常返回 None None 确实表示项不良类型； 但在其他系统中，推理器可能只支持规则的一个子集，或要求额外标注． 缺少标注、超时、资源不足或搜索尚未结束，都不能直接当作无类型的证明．

还有一种看法把类型推理当成运行程序看结果类型，把不写标注当成动态类型． 这套算术语言的推理按项的语法和类型规则分析，不执行 $⟶$ 来观察结果． 静态类型系统也可以推理出省略的类型标注； 检查与推理的分工在于是否给定期望类型， 静态与动态的分野则在于检查何时发生，见 静态类型与动态类型 ．

同时，推理返回某个类型，并不代表所有系统都能只靠比较相等来做类型检查． 类型唯一性依赖具体规则与证明，单凭“类型推理”这个名字并不能保证结果唯一． 例如，若在七条规则外增加“由 $𝑡:\text{ Nat}$ 推出 $𝑡:\text{ Bool}$”的转换规则， $0$ 就同时具有这两个类型． 只返回 $\text{Nat}$ 再与期望的 $\text{Bool}$ 比较，会误拒绝在扩展规则下成立的判断． 带子类型或多态的系统可能需要子类型判定、实例化等步骤； 若还要求推理返回最一般的主类型，也必须另行定义“更一般”，并证明主类型存在．

至于类型居留性，能检查或推理并不意味着能直接判定居留性，几个候选失败也不说明类型不可居留． 检查、推理已经拿到了项，居留性却要问是否存在任何合适的项． 否定单个候选不能否定存在性； 候选可能有无穷多个，只靠逐一枚举、检查，也未必能在没有居留者时停下来回答“没有”． 反过来，这也不说明居留性总是不可判定：这套算术语言的两个类型都有现成见证． 三种问题是否可判定，要针对具体系统分别论证．

在含变量的语言中，还需区分语境中的居留者与闭项． 若 $\mathrm{\Gamma }$ 已有 $𝑥:𝑇$，变量 $𝑥$ 就可在这个语境中居留 $𝑇$； 去掉该假设后，判断未必仍成立． 没有另外指定语境时，说“$𝑇$ 可居留”通常指存在闭项 $𝑡$（没有自由变量），使 $⊢𝑡:𝑇$． 词项的集合 的算术语言没有变量，所有词项都是闭项，因此这里取空语境．

此外，有居留者也不等于存在正常的值或程序一定能算出它． 这里的居留者是具有类型的项，不要求它已经是值． 在允许一般递归或异常的语言中，项有类型也可能永远循环或异常退出， 不能据此断言会正常返回该类型的值． 相应地，“底类型没有正常值”不等于“没有表达式能具有底类型”， 具体例子见 显式错误规则与 Kotlin 的底类型 ．