Recursive use of typeclass methods in Coq

Question

Is there a way to use recursion with Coq's typeclasses? Like for e.g., in defining show for lists, if you want to call the show function for lists recursively, then you will have to use a fixpoint like so:

Require Import Strings.String.
Require Import Strings.Ascii.

Local Open Scope string_scope.


Class Show (A : Type) : Type :=
  {
    show : A -> string
  }.


Section showNormal.

Instance showList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ lshow xs
        end
  }.

End showNormal.

Which is all well and good, but what if I want to define some helper function that I'll use for defining Show instances? Like I want to create a more DAZZLING show function called magicShow that prints stars around something...

Definition magicShow {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show a ++ " **".


Instance showMagicList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ magicShow xs
        end
  }.

However, in this case Coq can't find a show instance for the list xs to pass to magicShow:

Error:
Unable to satisfy the following constraints:
In environment:
A : Type
H : Show A
lshow : list A -> string
l : list A
x : A
xs : list A

?H : "Show (list A)"

Is there any way to do this in general? I.e., can you define a method for a typeclass using functions that rely upon the typeclass instance that you're defining?

Answer 1

No, there's no way to do this. This works in Haskell because arbitrary recursive bindings are allowed, and the language doesn't care about the order of bindings. Coq is more restrictive on both fronts. This makes sense if you think about what the desugaring looks like: the recursive call to show would refer to the currently-being-defined instance by name, but that binding isn't in scope yet. And you can't make the instance itself a fixpoint because you're recursing on the structure of a type, not on a value of an algebraic data type.

Your inline fixpoint works for show, but the problem gets thornier if your method implementations refer to each other, such as

newtype MyInteger = MyInteger Integer

instance Num MyInteger where
  MyInteger m + MyInteger n = MyInteger $ m  + n
  negate (MyInteger m) = MyInteger $ negate m
  m - n = m + negate n
  -- other methods

Here, the calls to (+) and negate in the definition of (-) needs to refer to the definitions of (+) and negate above, but this also doesn't work in Coq. The only solution is to define all your methods separately, manually referencing each other, and then define the instance simply by setting each method to the one you defined above. For example,

Inductive MyInteger := Mk_MyInteger : Integer -> MyInteger.

Definition add__MyInteger (m n : MyInteger) : MyInteger :=
  let 'Mk_MyInteger m' := m in
  let 'Mk_MyInteger n' := n in
  Mk_MyInteger (add m' n').

Definition negate__MyInteger (m : MyInteger) : MyInteger :=
  let 'Mk_MyInteger m' := m in
  Mk_MyInteger (negate m').

Definition sub__MyInteger (m n : MyInteger) : MyInteger :=
  add__MyInteger m (negate__MyInteger n).

Instance Num__MyInteger : Num MyInteger := {|
  add    := add__MyInteger;
  negate := negate__MyInteger;
  sub    := sub__MyInteger;
  (* other methods *)
|}.