Agda中Lambda表达式隐式参数的推理问题求解

你遇到的错误根源是类型签名写法有误：{ℕ}在Agda中会被解析为名字为ℕ的隐式参数（而非类型为ℕ的隐式参数），这导致f的类型被推断为「接收一个未知类型的隐式参数后返回自然数类型ℕ」，但你赋值的λ {n} → n是一个「接收隐式参数并返回该参数」的函数，二者类型不匹配。

在保留Lambda抽象的前提下，有两种规范的解决方式：

方式一：明确隐式参数的类型与名字 #

将类型签名中的隐式参数明确标注为类型是ℕ的参数，再用Lambda绑定该参数：

f : {n : ℕ} → ℕ
f = λ {n} → n

方式二：省略隐式参数的名字（用通配符） #

如果不需要使用参数名字，可用通配符_指定隐式参数的类型，Lambda中绑定任意名字即可：

f : {_ : ℕ} → ℕ
f = λ {x} → x

不推荐的写法（仅作参考） #

若你坚持要保留{ℕ}的写法（会和自然数类型名ℕ混淆，不推荐），可将其指定为类型是ℕ的参数名，Lambda中绑定同名参数：

f : {ℕ : ℕ} → ℕ
f = λ {ℕ} → ℕ

内容的提问来源于stack exchange，提问作者דניאל פ.ח.