Lean 4中两段函数组合代码一可编译一报错的原因咨询

可正常编译的代码 #

variable (α : Type)
variable (f : {p : α → Prop} → (x : α) → p x)
variable (g : {a b : Prop} → a → a ∨ b)
#check g ∘ f

无法编译的代码 #

variable (α : Type) (p : α → Prop)
variable (f : (x : α) → p x)
variable (g : {a b : Prop} → a → a ∨ b)
#check g ∘ f

报错信息 #

application type mismatch
g ∘ f
argument
f
has type
∀ (x : α), p x : Prop
but is expected to have type
?m.224 → ?m.227 : Prop

原因解析 #

函数复合运算符∘的核心要求是：前一个函数的输出类型必须与后一个函数的输入类型完全匹配，对应类型规则(β → γ) → (α → β) → α → γ。

• 第一个例子中的f是隐式多态依赖函数，{p : α → Prop}是隐式参数，Lean可以根据上下文自动推断p的具体实例。当与g复合时，Lean会把f的p实例化为某个固定命题类型a，让f的输出类型统一为a，此时f可看作α → a，正好匹配g的输入类型a，因此复合合法。

• 第二个例子中的f是具体依赖函数，它的类型是∀x:α, p x，输出类型是随输入x变化的命题p x，并非固定的单一类型。而g要求输入是一个固定的命题类型a，f无法满足“输出类型固定”的要求，无法匹配g的输入类型约束，因此触发类型不匹配错误。

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