The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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?

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.
-- 
Daniel Schepler