The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Yes, that's right.

On Sun, Jun 25, 2017 at 2:54 AM Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

Many thanks for the detailed explanations.  So it sounds like always using the {…} syntax for instance declarations is is the simplest approach to teach to beginners (right?).

    - B

On Jun 24, 2017, at 12:33 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi, 

  indeed you're hitting a few confusing things. First the record notation:
Instance has a special syntax [{ foo := bar }] for giving the fields of the class,
while [{| foo := bar |}] was introduced after for introducing values in general record types (parsing

issues prevented to reuse simple braces { }).
 

  There is a discrepancy in how these are typechecked currently: in the Instance : C args := { ... }
case, the type information flows from the arguments of the class type constraint to the parameters
of the constructor, hence you get a typing constraint for your method which readily mentions
bool and eqBool and typechecking succeeds. 

  In the case of {| |}, the record value is typechecked  independently of the typing constraint first, 

and in your example this involves a unification problem 

  forall (x y : ?A) (_ : @eq bool (@eqb ?A ?H x y) true), @eq ?A x y ~= 

  forall (a b : bool) (_ : @eq bool (Bool.eqb a b) true), @eq bool a b

which fails at first. We try to launch typeclass resolution to fill the holes, finding ?A to be nat, 

?H to be eqNat and then the unification fails again as we chose the wrong instance. 

  Bidirectional typechecking making the typing constraint information flow to the parameters, 

avoiding this unexpected behavior, is not on by default (for compatibility reasons mainly), but activated

in Program mode, so this works too:

Program Instance eqdecBool : @EqDec bool eqBool := 

  {|

    eqb_leibniz := Bool.eqb_prop

  |}.       

Sorry for the long explanation... it's definitely confusing.

-- Matthieu

On Sat, Jun 24, 2017 at 5:43 PM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> writes:

> You mean the error gotten by reverting
> a7ea32fbf3829d1ce39ce9cc24b71791727090c5 is in this case better?

Well, certainly I can't make sense of what that commit means.

Looking at the changes and commit message, it looks like the commit was
unfinished, maybe it slipped-in accidentally?

In fact it was coming from a 8.5 merge it seems, so that could explain
it.

E.