The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

Why is the error


Error:
The term "Bool.eqb_prop" has type
 "forall (a b : bool) (_ : @eq bool (Bool.eqb a b) true), @eq bool a b"
while it is expected to have type
 "forall (x y : bool) (_ : @eq bool (@eqb bool ?e x y) true), @eq bool 
x y".

though? I don't see a nat in there.

Gaëtan Gilbert

On 24/06/2017 01:46, Emilio Jesús Gallego Arias wrote:
> 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]