The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

... and why does removing the vertical bars make it succeed again?  

(What do the vertical bars mean, indeed?  The documentation doesn't seem to 
say.  I'd assumed it was "plain curly braces for record types and braces plus 
bars for record values."  But Instance declarations seem to accept either... 
except when they don't.)

        - B

> On Jun 24, 2017, at 04:07, Gaetan Gilbert 
> <gaetan.gilbert AT ens-lyon.fr>
>  wrote:
> 
> 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]
>