根据 MLton 文档：
标准 ML 要求在使用之前定义类型。[链接]
并非所有实现都强制执行此要求（例如，SML/NJ 没有），但上面链接的页面很好地说明了为什么可能需要它来保证健全性（取决于实现如何处理值限制），并且它符合定义中的一些评论：
尽管在我们的定义中没有假设，但每个上下文C = T , U , E都具有tynames E ⊆ T的属性。因此，可以松散地认为T包含所有“已生成”的类型名称。[…] 当然，就语义规则而言，关于“已生成”的内容的评论并不精确。但是下面的精确结果很容易证明：
令 S 是一个句子T , U , E ⊢短语⇒ A，使得词名E ⊆ T，并且让 S′ 是一个句子T ′, U ′, E ′ ⊢短语′ ⇒ A ′ 出现在 S 的证明中；然后还有tynames E ′ ⊆ T ′。
[第 21 页]
但我对此感到双重困惑。
首先——上述定理似乎倒退了。如果我正确理解“在 S 的证明中发生”这个短语，那么这似乎意味着（通过反证法）“一旦你的上下文违反了 tynames E ⊆ T的意图，所有后续上下文也将违反该意图”。即使这是真的，似乎断言相反会更有用和有意义，即“如果到目前为止所有上下文都符合 tynames E⊆ T 的意图，那么任何随后可推断的上下文也将符合该意图”。不？
其次 - MLton 的陈述和Definition的陈述实际上似乎都没有得到推理规则（或遵循它们的“进一步限制”）的支持。一些推理规则将“tynames τ ⊆ T of C ”或“tynames VE ⊆ T of C ”作为附带条件，但该程序不需要这些规则（在上面链接的文档中给出）：
val r = ref NONE
datatype t = A | B
val () = r := SOME A
（特别是：规则 (4) 与 相关let，规则 (14) 与 相关=>，规则 (26) 与 相关rec。本程序中均未使用这些。）
而从另一个方向来看，规则 (17) 涵盖了datatype声明，只要求生成的类型名称不在C的T中；因此它不会阻止生成在现有值环境中使用的类型名称（除非 tynames VE ⊆ T of C已经是真的）。
我觉得我可能在这里遗漏了一些非常基本的东西，但我不知道它可能是什么！