coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Typeclass confusions
- Date: Sat, 24 Jun 2017 06:27:02 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT hound.seas.upenn.edu
- Ironport-phdr: 9a23:M4GbWhH673k2PxUbccBFeJ1GYnF86YWxBRYc798ds5kLTJ78o86wAkXT6L1XgUPTWs2DsrQf2rWQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOCI2/2/KisJ+i6BUrhyuqRJ8zY7afpqYNOZnfqPYYd8aRXZNU8RXWidcAo28dYwPD+8ZMOtFsYb9oVkOogG7BQmtAuPk1yVGhn7o0q0gz+suDxzN0Qs7EN0SqHTUrcv6NL0OXu+r16TH0TTDb+hM1Tfg8IjHbBYhofeWUb1ubMXR1FAiGgXYhVuTsYzoJy6Z2+QOvmSB8uZtW/6jh3Qlpg1suDSj28khhpXRio8Ry13I7zt1zJg3KNGiVUJ2btqpHIFSuiyZMYZ9X9ksTHtyuCkgz70LoZ67czYOyJQg3xPfa/uHc5WO4h3+TuqROil3i2h+eL6lmhay6Vavyuv6VsWuzllFszdFnsHNtnALyRPT9tCKRuZ980qiwzqDyg7e5v1eLU02iKbXMYMtz7AsmpYLtETMBC72mEH4jK+McUUk//Cl5P/7bbX+p5+TKZV0hR3gPak1hsO/AP84PhITX2iD5+u80rvj8VfnT7pXk/06irPZv4zCJcQHuq65BBdY3Zok6xamFjupzNAYnWQcI19eYxKGj43pO0nUL/ziDPe/hU6skDZxyPzcML3hGMaFEn+Wm7D4OL159kR0yQwpzNkZ6YgHJKsGJafZV0nzvdnZCFcBMgGuyOuvXN92zoITQ2mCKqSYK+XPqVKO4KQiL/TaN9xdgyr0N/Vwv62mtnQ+g1JIJaQ=
... 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]
>
- [Coq-Club] Typeclass confusions, Benjamin C. Pierce, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Benjamin Pierce, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Benjamin C. Pierce, 06/25/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/25/2017
- Re: [Coq-Club] Typeclass confusions, Matthieu Sozeau, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Gaetan Gilbert, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Emilio Jesús Gallego Arias, 06/24/2017
- Re: [Coq-Club] Typeclass confusions, Abhishek Anand, 06/24/2017
Archive powered by MHonArc 2.6.18.