CODEWITHSUNDEEP
recursiontypeclasscoq
Ptival
Ptival

Reputation: 9437

Trouble with Coq type classes when defining recursive dependent fields

I am trying to define a set of descriptions and their interpretation into Coq Types, and this is what I came up with so far:

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
   }.

When declaring the Desc_TypeD instance, I initially wanted to define it as:

(need some text here so that SO will format the next code block :(...)

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
   }.

But Coq would not let me. It seems to me that, it tries to resolve those calls to denote as some other instance that it can't find, while really they were meant to be a recursive call to the instance being defined.

Is there any convincing that will let me write this instance without the explicit fix?

Thanks!

Upvotes: 2

Views: 125

Answers (1)

ejgallego
ejgallego

Reputation: 6852

It is hard to know why the fix bothers you without knowing more about you context. One way to get something close to what you want is to open up your TypeD, however, this will surely have other downsides:

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
  }.

Note that we also need to make denote's type more general as we cannot get enough information about the parameter D.

Upvotes: 2

Related Questions