The Coq mailing list

[Julien Tesson <julien.tesson AT lacl.fr>]

Hello there,
I'm currently experimenting miscellaneous organizations for a set of type 
classes I use in my Coq developments and I was trying a version based on the 
advices of the paper Type Classes for Mathematics in Type theory [1].
But then I ran into trouble when using what they call "operational type 
classes" and here is a minimal example of the kind of trouble I have :

=========
Require Import Coq.Classes.Init.
Require Import Coq.Relations.Relation_Definitions.

(* Here is the definition of an operational class I use to have a common 
notation for the R parameter of many classes.
 *)
Class Equiv A := equiv: relation A.

(* Here is a class that has this parameter. *)
Class test A (R:Equiv A).

(* Here is an instance of the class. *)
Instance T A R : test A R.

(*
then in a context where R is of type Equiv, no problem the instance is found
  *)
Goal forall A (R:Equiv A), test A R.
intros A R.
typeclasses eauto.
Qed.

(*
Now if R is of type relation A, I still can solve the goal using the instance
  *)
Goal forall A (R:relation A), test A R.
intros A R.                    
apply T.
Qed.

(*
but the instance search fails here.
*)
Goal forall A (R:relation A), test A R.
intros A R.                    
typeclasses eauto.(*  this one fail *)
Qed.

=========
Of course, this is a minimal example where I can easily choose to use the 
type Equiv A,  but in the context I use this kind of things, it's not that 
simple and operational type classes are useless if this kind of instance 
cannot be found.

Is there any hope to make "operational type classes" just work ?
I'm I missing something ?
Cheers,
Julien

[1] Type Classes for Mathematics in Type theory, Bas Spitters and Eelis van 
der Weegen. http://arxiv.org/abs/1102.1323