在具有依赖类型的语言中，您可以使用Type-in-Type，它可以简化语言并提供强大的功能。这使语言在逻辑上不一致，但是如果您只对编程感兴趣，而不对定理证明感兴趣，那么这可能不是问题。
在Cayenne论文（一种用于编程的依赖类型语言）中，提到了Type-in-Type：“未分层的类型系统将使得在类型检查过程中无法确定表达式是对应于类型还是实数。值，则无法在运行时删除类型”（第2.4节）。
我对此有两个问题：
Kind扩展层次结构，其中Type : Kind和Kind : Kind。这仍然不一致，但是现在看来您可以知道术语是类型还是值。这是正确的吗？未分层的类型系统将使得在键入过程中不可能检查以确定表达式是对应于类型还是实数值，将无法在运行时删除类型
这是不正确的。键入类型可以防止擦除证明，但是它不能防止擦除类型，前提是我们具有参数多态性，并且没有进行类型区分操作。最近的GHC Haskell是这样一个系统的示例，该系统同时支持键入中类型，类型擦除和类型级别计算，但不支持证明擦除。在依赖类型的设置中，我们总是知道术语是否为类型；我们只是检查它的类型是否为Type。
类型擦除只是擦除类型为Type的所有事物。
证明擦除更加复杂。假设我们有一个像Coq一样的Prop宇宙，该宇宙的意图是与计算无关的证明的宇宙。在这里，我们可以使用一些p : Bool = Int证明将Bool -s强制为Int。如果语言是一致的，则没有Bool = Int的封闭证明，因此封闭程序执行永远不会遇到这种强制性。因此，即使我们删除所有强制，关闭程序的执行也是安全的。
如果语言不一致，并且证明矛盾的方法是无限循环，则存在Bool = Int的封闭证明。现在，封闭程序的执行实际上可以打假。但是通过要求强制必须评估证明参数，我们仍然可以具有类型安全性。然后，只要我们因虚假性而被胁迫，该程序就会循环执行，因此执行永远不会到达程序的不良部分。擦除可以通过几种方式进行概括。例如，我们可能具有带有单个构造函数的归纳数据类型（并且没有其他地方无法提供的存储数据，例如类型索引），并尝试擦除该构造函数上的所有匹配项。如果语言总计，则再次听起来是正确的，否则不是。如果没有Prop Universe，我们仍然可以像这样进行擦除。 IIRC Idris经常这样做。