The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi Benjamin,

what happens is that the pre-typer tries to solve a "coercion problem"
[basically a type equality] from

 forall a b : bool, Bool.eqb a b = true -> a = b

to

 forall x y : ?X12, eqb x y = true -> x = y

[note the fresh type ?X12]

but indeed type class search will pick the first instance it finds, in
this case for Nat:

  Debug: 1: looking for (Eq ?A) with backtracking
  Debug: 1.1: exact eqNat on (Eq ?A), 0 subgoal(s)

which of course makes the coercion problem fail, and backtracking in
that part of the type inference is not powerful enough as to retry with
a different one.

I am not sure what the best solution is in this case, other than the one
you propose, as the logic is subtle [people talk from time to time of
improving the backtracking capabilities of the pretyper but I am not
sure that a brute force approach is what one would want here]

Best,
E.

[Regarding your original question, for most cases we tend to use the
 class hierarchy that mathcomp provides which is implemented using
 canonical structures and mixins. They seem mature and we just don't
 have to worry too much about them]