Scala能否检查类型级计算终止性？match类型是否会破坏类型安全？

完全依赖类型如果不进行终止检查，会直接破坏类型安全性。比如在Idris中就有这样的示例代码：

anything : a
anything = anything

这段无限递归的定义可以生成任意类型a的值，甚至能推导出2 + 2 = 5或者String = Int这类违背常识的类型等式，引发各类类型安全问题。

那如果Scala取消终止检查的限制，能不能借助它的match类型（一种依赖类型）实现类似的操作？

能实现。我们可以利用无限递归的match类型，配合无终止检查的特性，构造出可以“匹配任意类型”的万能定义，进而生成任意类型的值。

举个例子：

// 递归的match类型，永远匹配自身
type Anything[A] = A match
  case _ => Anything[A]

// 无限递归的函数，返回任意类型A
def anything[A]: A = anything[A]

如果Scala不做终止检查，编译器不会拒绝这个无限递归的定义。此时你可以把anything当作任意类型的值来使用：

// 将"String类型的值"赋值给Int变量
val nonsense: Int = anything[String]
// 构造出2+2等于5的"类型证明"
val fakeEquality: 2 + 2 =:= 5 = anything

这和Idris里的anything效果完全一致——因为编译器无法验证递归是否终止，只能接受这个定义，最终直接突破了类型安全的限制，允许任意类型的转换和荒谬的类型等式成立。

内容的提问来源于stack exchange，提问作者joel