为何这段Lean代码能通过类型检查？

先看你的代码：

def A : Type := sorry
def B : Type := sorry

def f (a : A) : B := a

关键在于Lean里的sorry是个万能占位符，它的作用是告诉类型检查器：“我暂时没法给出完整定义/证明，先默认这个是合法的”。具体来说：

• 用sorry定义A和B时，Lean并没有真正确定这两个类型的具体内容，只是假设它们存在。此时类型检查器无法判断A和B是否是不同的类型——毕竟你没给出它们的实际定义，Lean只能暂时信任你说的“这俩都是合法类型”。
• 对于f的返回值，虽然表面上a是A类型，返回要求是B类型，但因为A和B都是sorry占位的，Lean没法验证二者是否真的不兼容，所以直接通过了检查。

要是把sorry换成具体的类型（比如def A := Nat，def B := Bool），这段代码马上就会报错，因为Nat和Bool是明确不同的类型，不能直接把Nat值当成Bool返回。

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