Incompatible prefix warning

@tperami Could you help us out, since you changed the levels for the notation in question in !533 (merged)

@Blaisorblade Your feedback as our Coq notation expert would be useful too

I tried to fix this and nothing seemed to work. The Coq warning can be addressed by having both notations with the exact same levels (including for arguments), but this would require the {[ _ ]} notation (for singletons) to also have its argument be as pattern.

To be clear, the notations are both compatible (at least currently; a change in camlp5 may break something). Interestingly they both work even without as pattern in the propset notation.

It also isn't possible to suppress the warning locally due to a Coq limitation: https://github.com/coq/coq/issues/19536

I guess Coq actually has a point here -- without unbounded lookahead, how is the parser supposed to know how the first _ after {[ should be parsed? We'd have to see the | to know whether it is to be parsed as a pattern or a term, which can't work.

So we should probably change the notation.

This notation actually has a comment in the code...

(** Here we are using the notation "at level 200 as pattern" because we want to
    be compatible with all the rules that start with [ {[ TERM ] such as
    records, singletons, and map singletons. See
    https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#binders-bound-in-the-notation-and-parsed-as-terms
    and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003 *)
Notation "{[ x | P ]}" := (PropSet (λ x, P))
  (at level 1, x at level 200 as pattern, format "{[  x  |  P  ]}") : stdpp_scope.

The (unmentioned) alternative here is to use x binder, which would obviously work even less. But it seems now that using as pattern also does not work any more -- are patterns and terms (going to become) different nonterminals in the grammar?

Cc @tperami who adjusted this notation in !533 (merged).

I saw the comment (and read the linked references) and this is exactly why I mentioned in my comment that both notations are compatible even without as pattern. Let me be explicit that the comment is inaccurate (or outdated): as pattern is not required for compatibility. I don't understand why, but a quick empirical test doesn't lie:

Notation "{[ x | P ]}" := (PropSet (λ x, P))
  (at level 1, x at level 200, format "{[  x  |  P  ]}") : stdpp_scope.

Check {[ 2 ]}.
Check {[ x | x < 3 ]}.

I don't understand how both of these are being parsed. It seems like there's more than one token of lookahead, but I thought that was impossible.

To your comment about as pattern does not work any more - it's quite possible in my mind that it does actually work (and there is some vague promise it will continue to work), but the incompatible-prefix-warning code just doesn't recognize this case as safe (similar to how we think the warning should not trigger if a notation is only printing). That would be good to convey to the Coq devs to try to get them to update the warning.

a quick empirical test doesn't lie:

Does that also support writing {[ (a,b) : A * B | a = b ]}? That's what the MR was about. Your example already worked before !533 (merged).

That doesn't work, but that's unsurprising since it's the functionality of as pattern (it changes the grammar x is parsed under). The comment above this notation implies the as pattern is needed for the singleton and propset notations to be compatible, which doesn't seem to be true, and that's all my test was intended to illustrate.

For the grammar conflict: The point of at level 200 as pattern is to make the non-terminal in the grammar be a term and not a pattern. Then afterwards, if the parsed term is not a valid pattern, an error is thrown. This works because the set of productions of pattern is a subset of those of term.

Therefore, I think this is a problem in the warning that is a bit too eager to flag an incompatibility when there isn't one here (because of the "hack" of parsing a term first, then converting to pattern). The common prefix of both rules is "{|"; term LEVEL "200" and there is disambiguation on the third token that may be "|" or "]}" (or ":=").

When leaving just at level 200, I suspect, that given that x is used as a lambda binder, as pattern is kind of added automatically, but it might also be as ident.

So in at level 200 as pattern, the at level 200 is needed for compatibility with other rules, whereas the as pattern is needed to allow complex patterns such as (a,b) : A * B and not just x

Thanks for this clarification! I had assumed that as pattern was the relevant part of this for disambiguating the notations, but it's actually at level 200 that makes it work.

The comment above this notation implies the as pattern is needed for the singleton and propset notations to be compatible,

I don't think that is the intent of the comment. The comment was added in !533 (merged), the notations were already compatible before, but only for the "trivial binder" case.

Therefore, I think this is a problem in the warning that is a bit too eager to flag an incompatibility when there isn't one here (because of the "hack" of parsing a term first, then converting to pattern). The common prefix of both rules is "{|"; term LEVEL "200" and there is disambiguation on the third token that may be "|" or "]}" (or ":=").

Okay, thanks! We should file this as an issue with the Coq devs then.

Filed a Coq issue: https://github.com/coq/coq/issues/19541

mentioned in merge request iris!1080 (merged)

Our atomic triple notations also his this warning, and so far I don't understand why -- seems like an incorrect warning to me.

File "./theories/logatom/herlihy_wing_queue/hwq.v", line 5, characters 0-46:
Warning:
Notations "AU <{ ∃∃ _ .. _ , _ }> @ _ , _ <{ ∀∀ _ .. _ , _ , COMM _ }>"
defined at level 20 with arguments binder, constr at level 200, constr
at level 200, constr at level 200, binder
and "AU <{ ∃∃ _ .. _ , _ }> @ _ , _ <{ _ , COMM _ }>" defined at level 20
with arguments binder, constr at level 200, constr at level 200, constr
at level 200, constr at level 200 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default]

My expectation was that it would use the present of ∀∀ after the common prefix to disambiguate. And that in fact works fine, so when the warning says one will "likely not work", that's not what we see in practice.

There are two Coq PRs that fix the known instances of this warning in our repos:

Once they both land we should check again which warnings remain in a coq.dev build.

With those two PRs merged and !578 (merged) on our side, std++ and Iris build without any "incompatible prefix" warning. :)

Incompatible prefix warning

Designs

Child items ...

Activity