在定义递归依赖性字段时，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实例时，我最初想将其定义为：

（在这里需要一些文本，以便将下一个代码块格式化：（...）

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不会让我。在我看来，它试图解决这些呼吁将其表示为其他实例，但实际上它们本来是对被定义的实例的递归调用。

有什么令人信服的会让我在没有明确的fix？

的情况下编写此实例

谢谢！

Answer 1

很难知道为什么fix在不了解您的上下文的情况下困扰您。但是，获得接近您想要的东西的一种方法是打开您的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的足够信息。