The Coq mailing list

[Matthieu.Sozeau AT lri.fr]

> (* Hello list
>  *
>  *  Ok, this seems like a really silly problem... Let's take an EqDec
> class
> as defined in the manual:
>  *)
>
> Class EqDec (A : Type) := {
>  eqb : A -> A -> bool;
>  eqb_leibniz : forall x y, eqb x y = true -> x = y
> }.
>
> Section test.
>
>   Variable A : Type.
>
>   (* here, everything works as expected *)
>   Definition test `{w : EqDec A} (a b : A) := eqb a b.
>
>   (* but if we introduce a type abbreviation: *)
>   Definition eqdecA := EqDec A.
>
>   (* then this doesn't work:
>
>> Definition test' `{w : eqdecA} (a b : A) := eqb a b.
>
>      I also tried it with:
>> Typeclasses Transparent eqdecA.
>      and with replacing Definition with Let in [eqdecA]; both to no avail.
>     *)
>
> End test.
>
> (* I'm using 8.2pl1; what am I missing?
>  * Best, Adam
>  *)

Hi Adam,

Typeclass resolution tries to be clever and not use every hypothesis
in your context but only those that represent type class instances.
The test is syntactic, it checks if the head of the hypothesis type
under some products is a class, without any reduction. It should take
a kind of head normal form instead. You can use a Notation to work
around the problem in this case.

Best,
-- Matthieu