Coq报错中?T@{x:=t}形式类型标识含义及报错解析

问题背景 #

尝试编写用于移除列表中零值元素的函数，最初的错误实现代码如下：

Require Import Nat.
Require Import List.
Fixpoint shrink (x : list nat) list nat := (* 错误点：返回类型前漏写冒号，应为: list nat *)
  match x with
  | nil    => nil
  | h :: t => if h =? 0 then shrink t else (h :: shrink t)
  end.

编写上述代码时触发如下报错：

Error:
In environment
shrink : forall (x : Datatypes.list Datatypes.nat) 
           (list0 : ?T) (nat : ?T0@{list:=list0}),
         Datatypes.list ?T1@{x:=x; list:=list0; x1:=x}
x : list nat
list : ?T
nat : ?T0
h : Datatypes.nat
t : Datatypes.list Datatypes.nat
The term "shrink t" has type
 "forall (list0 : ?T@{x:=t}) (nat : ?T0@{x:=t; list:=list0}),
  Datatypes.list ?T1@{x:=t; list:=list0; x1:=t}"
while it is expected to have type "Datatypes.list ?T1@{x1:=h :: t}".

正确的函数实现代码如下：

Fixpoint shrink (x : list nat) : list nat :=
  match x with
  | nil    => nil
  | h :: t => if h =? 0 then shrink t else (h :: shrink t)
  end.

报错中(list0 : ?T@{x:=t})片段较难理解，对应三点核心疑问：

• 为什么此处的标识符是list0而非list？
• 类型标识T前的?符号代表什么含义？
• 类型标识T后的@{ ... }片段代表什么含义？

报错根因 #

错误本质是函数定义时漏写了返回类型前的冒号。正确写法中: list nat是用来标注函数返回类型的，漏写冒号后，Coq不会把后面的list nat识别为返回类型，反而会把list、nat解析为shrink函数需要接收的两个额外入参，最终导致类型完全不匹配。

疑问解答 #

1. 标识符显示为list0而非list的原因 #

Coq解析到错误的函数签名时，已经把shrink识别为需要3个入参的函数：第一个入参是x : list nat，第二个入参名是list，第三个入参名是nat。当解析到递归调用shrink t时，发现只传入了1个参数，还缺2个参数，Coq会为这两个缺失的参数自动生成临时绑定名。由于当前外层作用域已经存在名为list的绑定，为了避免命名冲突，自动生成的临时名会加数字后缀，变成list0。

2. T前的?符号含义 #

带?前缀的标识符是Coq类型推导阶段生成的存在类型元变量，代表这个位置的类型还未被确定，Coq正在尝试根据上下文推导它的具体类型。由于代码存在语法错误，Coq无法推导这些额外生成的入参的实际类型，因此全部标记为待确定的元变量，如?T、?T0、?T1。

3. @{ ... }片段的含义 #

该片段是Coq用来标记元变量所属局部上下文的标识，用来记录这个待推导的元变量是在哪个作用域、哪些变量绑定的环境下生成的。例如?T@{x:=t}表示这个名为?T的元变量，是在递归调用shrink t、此时形参x被绑定为实参t的上下文下生成的，用来区分不同调用点生成的同名元变量，避免类型推导时出现上下文混淆。

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