为什么Coq对可强制转换项应用参数时无法推断强制转换？

问题根因 #

你的强制转换定义不存在错误，该问题是Coq强制转换的固有触发限制导致的：

• Coq的自动强制转换仅会在上下文存在明确的期望类型，且当前项的类型与期望类型不匹配时才会被触发。
• 当你编写foo 1 2这类参数应用语句时，Coq会首先检查待应用项foo的头部类型是否为箭头（函数）类型：你定义的serial nat是带约束的依赖和类型（属于sig归纳类型），本身不是函数类型，Coq会直接判定它不支持参数应用，不会启动强制转换搜索流程。
• 而Check (bar foo)可以正常执行，是因为bar的参数明确要求传入relation nat类型，上下文有明确的类型期待，Coq会自动搜索并插入你定义的serial_to_relation强制转换。

解决方案 #

方案1：显式标注类型触发强制转换 #

通过显式标注目标类型，让Coq主动触发强制转换，修改后代码可正常运行：

Check (foo : relation nat) 1 2.

方案2：为serial类型注册函数应用实例 #

如果你希望完全省略类型标注，直接支持foo 1 2的写法，可以为serial类型注册Funclass实例，让Coq识别该类型支持参数应用：

Instance serial_app A : Funclass (serial A) A (fun _ => A -> Prop) := proj1_sig.

(* 现在该语句可正常执行 *)
Check (foo 1 2).

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