The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Because of a type unification, when applying the instance, Equiv and relation should be convertible.

Le vendredi 28 février 2014, Frédéric Blanqui <frederic.blanqui AT inria.fr> a écrit :

Hi. To better understand what's going on, could you explain why Equiv needs to be unfolded? Best regards, Frédéric.
 

Le 28/02/2014 02:59, Jason Gross a écrit :

You need to tell Coq that it's allowed to unfold [Equiv].  In this case, your example goes through if you do

Typeclasses Transparent Equiv.

-Jason

On Thu, Feb 27, 2014 at 11:56 AM, Julien Tesson <julien.tesson AT lacl.fr> wrote:

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

--