recursion - 定义递归依赖字段时 Coq 类型类出现问题

Question

我正在尝试将一组描述及其解释定义为 Coq 类型，这是我迄今为止想到的:

Class Desc (D : Type) :=
  { denotesInto : D -> Type
  ; denote : forall (d : D), denotesInto d
  }.

Notation "⟦ d ⟧" := (denote d).

Inductive TypeD : Type :=
| ArrowD : TypeD -> TypeD -> TypeD
| ListD  : TypeD -> TypeD
| NatD   : TypeD
.

Global Instance Desc_TypeD : Desc TypeD :=
  { denotesInto := fun _ => Type
  ; denote := fix go d :=
      match d with
      | ArrowD dL dR => (go dL) -> (go dR)
      | ListD  dT    => list (go dT)
      | NatD         => nat
      end
   }.

在声明 Desc_TypeD 实例时，我最初想将其定义为:

(此处需要一些文本，以便 SO 格式化下一个代码块:(...)

Global Instance Desc_TypeD : Desc TypeD :=
  { denotesInto := fun _ => Type
  ; denote :=
      match d with
      | ArrowD dL dR => ⟦ dL ⟧ -> ⟦ dR ⟧
      | ListD  dT    => list ⟦ dT ⟧
      | NatD         => nat
      end
   }.

但是 Coq 不让我这么做。在我看来，它试图解析这些调用以表示它找不到的其他实例，而实际上它们是对正在定义的实例的递归调用。

是否有任何令人信服的证据可以让我在没有显式修复的情况下编写此实例？

谢谢!

Answer 1

如果不了解更多有关您的上下文的信息，就很难知道为什么修复会困扰您。获得接近您想要的结果的一种方法是打开您的 TypeD，但是，这肯定会有其他缺点:

Class Desc (D : Type) :=
  { denote : forall (d : D), Type }.

Notation "⟦ d ⟧" := (denote d).

Inductive TypeD (D : Type) : Type :=
| ArrowD : D -> D -> TypeD D
| ListD  : D -> TypeD D
| NatD   : TypeD D
.

Global Instance Desc_TypeD D `{DI : Desc D} : Desc (TypeD D) :=
  { denote := fun d =>
      match d with
      | ArrowD _ dL dR => ⟦dL⟧ -> ⟦dR⟧
      | ListD _ dT     => list ⟦dT⟧
      | NatD _         => nat
      end
  }.

请注意，我们还需要使 denote 的类型更加通用，因为我们无法获得有关参数 D 的足够信息。