与类型族匹配时的 Coq 类型错误

Question

我正在尝试根据记忆重新实现 CPDT 中的示例。我写道：

Inductive myType : Set := MyNat | MyBool.

Definition typeDenote (t : myType) : Set :=
  match t with
    | MyNat => nat
    | MyBool => bool
  end.

Inductive unaryOp : myType -> myType -> Set :=
| Twice : unaryOp MyNat MyNat.

Definition twice (n:nat) : nat := n + n.

Definition tunaryDenote (a b : myType) (t : unaryOp a b)
    : typeDenote a -> typeDenote b :=
  match t with
  | Twice => twice
  end.

产生的错误是：

Toplevel input, characters 125-130
>   | Twice => twice
>              ^^^^^
Error: In environment
a : myType
b : myType
t : unaryOp a b
The term "twice" has type "nat -> nat" while it is expected to have type
 "forall H : typeDenote ?141, typeDenote ?142"

我不明白这个错误信息。我认为一旦 Twice : unaryOp MyNat MyNat 上的匹配成功，Coq 推断 a 和 b 是 MyNat，因此 typeDenote a -> typeDenote b ≡ nat -> nat，使 twice 非常适合 return 值。我哪里出错了？

Answer 1

我认为答案是 Coq 的类型推断是有限的，并没有做你想让它做的推理。

Coq的类型推断不做任意计算，而是简单的统一。它查看 twice，理解它是 nat->nat 并得出结论它不是（语法上）形式 typeDenote a -> TypeDenote b.

如果它正在进行计算，它很可能是非终止的，因为它的类型系统非常复杂，因此您可以在那里编码非平凡的计算。

Answer 2

正如@AntonTrunov 所说，它在我的 Coq 8.5pl1 上进行了类型检查，没有任何问题。但是，如果您需要为您的版本添加一些额外的注释以接受该功能，您需要 have a look at this section of the manual 弄清楚该怎么做。

我的猜测是你想有一个match ... in ... return ... with表示return类型应该是refined通过匹配t得到的信息在类型 unaryOp a b（实际上：a 和 b 将在 Twice 分支中采用具体值）。

这是您使用该技术得到的定义：

Definition tunaryDenote (a b : myType) (t : unaryOp a b)
    : typeDenote a -> typeDenote b :=
  match t in unaryOp a b return typeDenote a -> typeDenote b with
  | Twice => twice
  end.

Answer 3

我尝试了较新版本的 Coq，正如其他人所说，它在 Coq 8.5 上的类型检查没有问题。 :)

与类型族匹配时的 Coq 类型错误

Coq type error when matching with type family

coq