The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-03-10, Daniel Schepler wrote:
> Let me add my own question on typeclasses:
> 
> Suppose I define
> 
> Generalizable All Variables.
> 
> Class ExtEqual {X Y} (f g:X->Y) : Prop :=
>   extensional_equality : forall x:X, f x = g x.
> 
> Class injective `(f:X->Y) : Prop :=
>   injectivity: forall x1 x2:X, f x1 = f x2 -> x1 = x2.
> 
> Instance injective_properness
>   `{ExtEqual X Y f g} `{injective _ _ f} :
>   injective g.
> 
> Here why do I have to fill in the implicit arguments for ExtEqual and 
> injective?  Is that the intended behavior?

You can get the usual handling of implicit arguments by inserting ! at
the begining of an generalizing binder, which also turns off the
implicit generalization of unspecified arguments. I don't know what the
rational for this behaviour is.

> Also, it seems if I add too many instances along these lines (fg injective 
> -> 
> g injective, id injective and surjective, etc.) I tend to end up with the 
> resolver failing in simple situations, and "typeclasses eauto" looping.

I think that this is a known issue. I don't know of any general
workarounds. One suggestion that I have seen for some cases, is to add a
hint conditioned with a more specific pattern to the typeclass_instances
database. (An instance is, as far as I can tell, essentially a hint in
this databse)

  Tom