Printing Notation regressed compared to 8.7

[RalfJung]

Version

git master

Operating system

Linux

Description of the problem

In the gen_proofmode branch of https://gitlab.mpi-sws.org/FP/iris-coq/, printing notations regressed compared to Coq 8.7. This is visible for example in theories/bi/update.v: What used to be printed as (|==> P) ⊢ P is now printed as (sbi_bi PROP).(bi_entails) (|==> P)%I P.

The relevant notation ⊢ is defined in theories/bi/interface.v:

Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.

bi_entails is a primitive projection, so #6651 could be related. Or maybe this is caused by one of the recent scope handling changes?

[RalfJung]

Small example:

Set Primitive Projections.

Record foo := Foo { foo_n : nat }.

Notation "'■' x" := (foo_n x%type) (at level 50).

Goal forall (f:foo), ■ f = ■ f.

With 8.7, this prints what I typed (■ f = ■ f), with master it prints f.(foo_n) = f.(foo_n)

[JasonGross]

This is almost certainly #6651, because the printing worked fine on the only-slightly-outdated version of master I was previously using (47e43e2)

[RalfJung]

Ah, you're right. I thought the %type was the problem, but actually the problem persists without it.

[ppedrot]

Yes, the problem is that notation matching is completely unaware of primitive projections. The input term to be matched is pretyped to a primitive projection and then back to a GProj, but the notation constr doesn't know anything about that as it is a NApp node. Obviously matching then fails because the two terms are unrelated.

Either we need to handle specially primitive projections in notation matching, or we need to also generate a notation rule for applied primitive projections. I don't know which one is better.

[ppedrot]

I have a potential patch at ppedrot/coq@189528e but it breaks due to pretyping being stupid in the handling of GProj, as hinted by the following comment.

    (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)

On @RalfJung's example I get a pretype error saying that the hole cannot be inferred.

[maximedenes]

I didn't follow how the input GProj is produced, but in any case, it shouldn't be too hard to implement the bidirectional typing rule.

[maximedenes]

But I'm a bit worried that some other parts of the code could distinguish the GApp nodes from GProj, which is why I tried to avoid introducing them (except in the printing, where I forgot to handle notations for such projections).

[ppedrot]

Ultimately, I think my local solution is the best as it tries not to introduce ad-hoc code. Whether this is sane or not w.r.t. bug preservation is another story.

[herbelin]

Good to see this work in making primitive projections better and better! I have a few comments.

• As pointed out by @mattam82 in this comment, there should eventually be a ProjRef global reference so that we don't need to call functions such as Environ.is_projection. Has someone already plans to go in this direction?
• We need a rationale to explain whether t.(p) is intended to mean a (negative) primitive projection GProj or to also mean a compact representation of the (positive) defined named projection GProj false? I believe that it would be less a source of confusion to mean only the first situation, but, by compatibility, we may also want the second.
• In my view, I don't think that NProj should come with a Boolean. It should only correspond to GProj false (in the positive case) and to the only GProj which matters in the negative case. Even for GProj, it is not clear to me that it should come with an unfolded flag (compared to elaborating a Proj true only at pretyping time). This is consistent with having CProj bound to GProj false and no name-based syntax for GProj true (i.e. the syntax for GProj true should be a special form of match in the positive case and being irrelevant in the negative case).

Again, I have no idea about whether we have a common view on the meaning to give to the unfolded flag and on the "negative" vs "positive" distinction, so please comment to tell your view. It may also be the case that I oversought some discussions on this topic, so please tell me if this is the case.

PS: In line 366 here, couldn't there be the case of a projection with a functional type and more arguments coming after the main argument?

[ppedrot]

I have no idea about whether we have a common view on the meaning to give to the unfolded flag

I'd be glad if @mattam82 gave a comprehensive description of the uses of that flag, actually.

PS: In line 366 here, couldn't there be the case of a projection with a functional type and more arguments coming after the main argument?

Yes, I thought about it but I wondered whether one could get around that by using explicit parentheses? I don't remember if we collapse GApp nodes during internalization.

[herbelin]

Yes, I thought about it but I wondered whether one could get around that by using explicit parentheses? I don't remember if we collapse GApp nodes during internalization.

Actually, I'm lost. We have two representations of foo_n x in glob_constr? Is it because we want to preserve a different printing for them?

Actually, I'm not sure that I understand very clearly how to interpret a non-fully-applied projection, nor if we should keep an explicit representation for projections with all its parameters which is distinct from the optimized form.

For instance, let's consider the following cases

Set Primitive Projections.
Record foo := Foo { foo_n : nat }.
Notation "'■' x" := ((x%type).(foo_n)) (at level 50).
Check forall (f:foo), ■ f = ■ f.
(* Should use the notation by principle of reversibility *)
Check forall (f:foo), foo_n f = foo_n f.
(* Should it use the notation, i.e. is it a different expression or not? *)
Notation "# x" := (foo_n (x%type) ) (at level 50).
Check forall (f:foo), # f = # f.
(* Should use the "#" notation by principle of reversibility *)
Check forall (f:foo), f.(foo_n) = f.(foo_n).
(* Should it use the "#" notation or the "■" notation, i.e. is it a different expression or not? *)

(For the record, in today's master, it does not use a notation at all in either cases.)

Otherwise said, shouldn't there be a difference between foo_n x (meaning a Const with all its parameters explicit) and x.(foo_n) (meaning a Proj false with its parameters absent)? By doing so,foo_n alone would make sense as the stand-alone constant, foo_n p would make sense as this constant applied to parameters (at least in printing), while in parsing, we would have the choice. To take benefit of the compact representation of foo_n p, we could directly reinterpret it (and thus print it) as p.(foo_n)? Or, alternatively, to be consistent with the internal representation, we interpret it as foo_n all_its_params p (but loosing the compactness of the representation).

[ppedrot]

@herbelin I think that the compatibility layer is the source of all this fuss. There shouldn't be a confusion between the primitive projection and the corresponding constant. I understand this would be a problem for porting code to primitive projections, but at the same time in the long run it'd save us a lot of ultimately nonsensical questions.

The current situation regarding glob_constr is that:

• When the user writes a term standing for a projection, whether using x.(foo) or foo x, this is always desugared to a GApp by internalization. It is the rôle of the pretyper to trigger ad-hoc code recognizing that a fully applied constant is interpreted as a mkProj.
• Nonetheless, since @maximedenes's patch, the detyper produces GProj nodes when handling primitive projections. So there is an asymmetry here, which is what the notation bug uncovers.

[herbelin]

@ppedrot: So, is the approach that you're proposing the following:

• no compatibility layer, so no positive interpretation of primitive projections
• removing the unfolded flag
• removing the Printing Primitive Projection Compatibility and Printing Primitive Projection Parameters flags
• exclusively providing the t.(proj) syntax for primitive projections, without the parameters of proj (and in particular no partially applied projection)
• adapting manually to the changes of semantics resulting of moving from a positive view of records and tuples to a negative view in existing libraries (in particular, removing the existing instances of match in such types, removing the unfold proj for existing proj-as-constant in such types, turning existing applications of proj in such types to the t.(proj) notation, etc.) [edited for misusing a preposition]

[RalfJung]

I think it would be nice to have an option for proj t, when fully applied, to be turned into t.(proj). Without such an option, we would suffer a severe performance regression as we'd not actually use the primitive projections most of the time. Also, I cannot imagine a situation where one writes a fully applied projection and does not want the compact (parameter-free) representation.

Another open question is: Is there a way to make t.(proj) fail if this is not a primitive projection? IOW, it would be nice to have a guarantee that, when writing t.(proj), we get the compact representation.

[herbelin]

@RalfJung

Is there a way to make t.(proj) fail if this is not a primitive projection?

BTW, related question: would you like the notation {|... ; proj := t; ...|} to fail if not in a type equipped with primitive projections?

Or is your question strictly only about the compactness of the representation of projections and not about the introduction/destruction/reduction/eta rules which are associated to the type, i.e. not about whether these projections are primitive in the logical meaning of "primitive" (i.e. with surjective pairing as eta, without a proper match, without unfold of a projection being allowed) but really about whether they are represented compactly, independently of whether it is an optiimization of the good old existing form of (co)inductive types (with match and unfold-able projections) or a new primitive form of type built from projections (typically in the Abel-Pietka-Sentzer style)? (Hoping that my question makes clear enough sense.)

[herbelin]

Actually, do we really need to keep types without a compact representation of projections?

Is it correct that the only incompatibility (in the "compatibility" mode) is with tactics counting or unfolding subterms occurring in the parameters of a projection? Or maybe also sometimes in how types are inferred when the arguments of a projection are implicit? So, in a context where efficiency matters for scaling, the Compatibility Primitive Projections mode should be on by default, no? And deactivated only when there are too much worries with the irreducible (little?) incompatibilities due to having the parameters of the projection canonically inferred rather than explicitly given?

[herbelin]

Let me rephrase things once more differently.

There are basically three independent design choices to do for types equipped with projections:

1. whether they are defined from projections or defined from match and constructors
2. whether they represent projections in a compact way or not
3. whether the projections are represented with the t.(proj) notation or not (and subsidiary, whether tuples are represented with the {| ... |} notation or not)

Currently, 3. is independent of 1. and 2., and this is precisely the point of @RalfJung's question and of @maximedenes's #6651 to tie 3. to either 1. or to 2.

Currently, demanding a compact representation in 2. is not the default and this is precisely the point of @JasonGross's #6609 to always adopt a compact representation (a priori independently of the degrees of freedom 1. and 3.).

[RalfJung]

would you like the notation {|... ; proj := t; ...|} to fail if not in a type equipped with primitive projections?

I have not thought about that. I was coming mostly from the performance stand-point -- the reason we use primitive projections is because it makes things measurably faster; if we can't even see in the surface syntax whether we are actually applying that optimization, that would be problematic and it would make performance issues harder to debug.

[maximedenes]

I didn't manage to fix this in time for the beta, sorry about that.

If we don't come up with a better with, one easy thing we could do for the final version is to unplug the construction of GProj, so as to undo the effects of my PR while keeping the infrastructure.

[maximedenes]

@RalfJung can you confirm that the Iris problems are solved?

[ejgallego]

Indeed @RalfJung it would be good to know if additional problems with IRIS do exist in 8.9 and master.

[RalfJung]

As confirmed on gitter, this fixes the biggest problem. Our test suite still failed because backtraces for first and last tacticals got "improved" but we don't want these backtraces, I have fixed that since then and now Coq master passes our test suite just fine.

Is there an issue tracking getting this backported into 8.9?

[ejgallego]

Great @RalfJung , it should be scheduled for backporting due to the milestone.

[Zimmi48]

This was an API breaking change so this is why it takes longer to backport.
Cf. #8456 (comment)
cc @gares

[RalfJung]

I am going to reopen this issue until a fix lands in 8.9.

@gares what's the status of the backport?

[gares]

I made an overlay for elpi I think I made a pr... Dunno if someone wrote the overlay file

[gares]

https://github.com/LPCIC/coq-elpi/tree/overlay/8456?files=1 sorry I made a branch, dunno for the overlay file

[RalfJung]

@Zimmi48 @ejgallego is that enough to get a backport started?

[gares]

I think I messed up things, the commit is already part of coq-master.
I guess you need a coq-v8.9 branch and a PR containing that commit? If so I can do the branch and the PR today.

[Zimmi48]

@gares Currently CI for v8.9 is testing commit gares/coq-elpi@12efa57, i.e. before #8552 (using elpi 1.1.0). Creating a v8.9 branch starting from this commit and backporting the fix to this branch (no need to go through a PR), would allow @silene to backport #8456 without backporting #8552.

[gares]

I made a coq-v8.9 branch on master, since master compiles fine with 8.9, and cherry picked there the commit. So the coq-v8.9 branch should compile fine when CProj is removed.

I don't get exactly the before #8852 part. Are you saying that the docker image for v8.9 does not contain elpi 1.1.0 ?

[Zimmi48]

Are you saying that the docker image for v8.9 does not contain elpi 1.1.0 ?

Exactly.

[ejgallego]

Exactly.

The elpi update is supposed to be in the backport queue, right?

[Zimmi48]

It is still in the backport queue indeed. But @silene was hoping he could avoid backporting it. That's the sense of his comment and mine here: #8456 (comment)

[gares]

I don't how much relevant elpi is, but I've just released the first version of coq-elpi and I'd like it (and its minor releases) to work on 8.9. If CI can only test an old version of the code, then I think there is no value in keeping elpi in the CI for 8.9. If on the contrary the image gets updated I'll happily push to the coq-v8.9 branch each minor fix I do in master (as I do from time to time on coq-master).

[ejgallego]

^^ indeed, this was my understanding of the coq-elpi situation for 8.9. Either you drop it or you update it.

[Zimmi48]

That's fine with me.

[silene]

#8456 has been backported.

[RalfJung]

Confirmed, Iris notation tests now pass on the 8.9 branch. Thanks all :)