Take into account position of main argument of a projection when inserting implicit arguments for syntax t.(f)

[herbelin]

Kind: fix and enhancement

Depends on mattam82/Coq-Equations#413 (or at worst on tolerant Loc.merge in #14618).

Fixes #4167 and improve error message when a field has a wrong number of explicit parameters

This is done by introducing special functions for interning/externing which cut the implicit arguments signature of a projection into a parameter part and an extra functional part (if ever the projection happens to return a function with its own implicit arguments).

• Added / updated test-suite
• Entry added in the changelog

[coqbot-app]

Hey, I have detected that there were CI failures at commit b711386 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 8560c27 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-argosy.

[coqbot-app]

Hey, I have detected that there were CI failures at commit b711386 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 8560c27 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-argosy.

[coqbot-app]

Hey, I have detected that there were CI failures at commit b711386 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 8560c27 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-argosy.

[coqbot-app]

Hey, I have detected that there were CI failures at commit 5b9df34 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 444aa95 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-metacoq.

[ppedrot]

Use List.count and Option.is_empty.

[herbelin]

Good idea.

[ppedrot]

This PR is making the t.(p) notation straying further than the application it used to stand for. Maybe we should take the decision soon. Note that the comment above about "officiality" is wrong, IIUC the code still takes the projection path when the head is an arbitrary reference.

[herbelin]

This PR is making the t.(p) notation straying further than the application it used to stand for.

Yes and no. In this PR, it is still an application but with a treatment of implicit arguments which takes into account that the main argument splits the implicit arguments into two parts.

So, unless I'm missing something. nothing is changed wrt references which have no implicit arguments.

Note that the comment above about "officiality" is wrong

Would replacing "An official projection" by "A reference registered as projection" be ok?

IIUC the code still takes the projection path when the head is an arbitrary reference.

If by projection path you mean intern_proj, yes, since intern_proj is called whenever the t.(f) syntax is used. Is that ok or do you expect something else? For instance, would you prefer that another terminology than "proj" is used to talk about the t.(f) notation?

[herbelin]

@ppedrot: I used "A reference registered as projection", hoping it is compatible with your view. Should the names of functions (like intern_proj, etc.) be reconsidered further to avoid any ambiguity? Did I address your questions?

In any case, dependency is merged, will you assign?

[bedrock2's failure is waiting about mit-plv/bedrock2#190]

[ppedrot]

Use List.is_empty.

[herbelin]

Granting your wish.

[RalfJung]

Is it possible that this is the cause of #14703?

[RalfJung]

It looks like this PR also changed notation parsing:
(Σ[ ty; rc ty ]).(ty_size) now fails ("unknown interpretation for notation") where ty_size (Σ[ ty; rc ty ]) still works; here Σ[...] is a notation in a scope that is not opened globally but via Arguments ty_size.

[herbelin]

I could not reproduce. Could you give an example if possible?

[herbelin]

For instance, the following works:

Declare Scope foo_scope.
Delimit Scope foo_scope with foo.
Record prod A B := pair { fst : A ; snd : B }.
Notation "[[ t , u ]]" := (pair _ _ t u) : foo_scope.
Arguments fst {A B} p%foo.
Check [[2,3]].(fst).

@RalfJung : How different is your real example?

[RalfJung]

This is the change that was required. I can try to minimize this.

[RalfJung]

Hm, my attempt to isolate this also failed:

From Coq Require Import List.
Export ListNotations.

Record type :=
  { ty_size : nat;
    ty_own : list nat -> Prop;
    ty_size_eq vl : ty_own vl -> length vl = ty_size;
  }.

Declare Scope lrust_type_scope.
Delimit Scope lrust_type_scope with T.
Bind Scope lrust_type_scope with type.

Axiom sum : list type -> type.

Notation "Σ[ ty1 ; .. ; tyn ]" :=
  (sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.

Axiom t : type.
Check (ty_size Σ[t; t]).
Check ((Σ[t; t]).(ty_size)).

Something must still be different than in the full lambda-rust, but I have no idea what.

[herbelin]

Actually, this has nothing to do with scopes and notations. It is another instance of the class argument of ty_size being forced to be explicit and in position of main argument when using the .( ) notation! No more worries than #14703!

[RalfJung]

I don't see that. Σ[ ty; rc ty ] is of type type and ty_size is a primitive projection of type.

Using foo.(ty_size) works in many other places, it just does not work here. And the error explicitly talks about "unknown interpretation for notation". I am pretty sure this is a different issue than #14703.

[RalfJung]

For example, further up the same file we do new [ #(option ty).(ty_size) ] and that works just fine. That should require exactly the same kind of inference as new [ #(Σ[ ty; rc ty ]).(ty_size) ].

[herbelin]

You're right, there is a bug (I did not test on the right branch apparently). I'm going to submit a fix soon.

[RalfJung]

Awesome, thanks. :)

[SkySkimmer]

There's a changelog, but shouldn't there be something in the doc too?