Fixes #9412: Context command ignored implicit binders

[herbelin]

Kind: bug fix

Fixes / closes #9412

This is a quick fix (which will have to be adapted on top of #12272).

• Added / updated test-suite
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[herbelin]

I added a warning for Context not in a section (but I'm not fully convinced; refining the refman to tell that Context outside a section is like the declarations made Local is maybe lighter).

Maybe the incompatibilities are too important and it'll be preferable to do the fix in two steps... A first release with a warning telling how to fix. The next release w/o the warning??

[SkySkimmer]

Some people use context outside sections a lot, eg https://github.com/mit-pdos/perennial/blob/cdaa737e40d08c1c7c7d514db69a8f9b55814713/src/CSL/RefinementIdempotenceModule.v#L18-L52
Not sure we want to warn for that. Maybe an off-by-default warning?

[herbelin]

Some people use context outside sections a lot, eg https://github.com/mit-pdos/perennial/blob/cdaa737e40d08c1c7c7d514db69a8f9b55814713/src/CSL/RefinementIdempotenceModule.v#L18-L52
Not sure we want to warn for that. Maybe an off-by-default warning?

Thanks. This confirms my view that we should rather change the doc. (But still keep a warning for Context {a : A} outside a section).

To deal with the compatibility, I'm now otherwise considering using the multiple sequence of implicit arguments feature, i.e. to do so that Context (f : forall {x}, ...) behaves as Arguments f {x} ..., x ... (including auto implicit arguments if any). This could even be generalized to all manual declarations of implicit arguments, i.e., when the conclusion of f is rigid, that:

Definition f : forall {x}, ...

behaves (including auto implicit arguments) as:

Arguments f {x} ..., x ...

I suspect that this would be totally compatible, since the extra sequence would be used only when more arguments than expected are used.

Also, this would provide with an alternative way to explicitly give implicit arguments which is lighter than by using the (x:=...) notation.

What do you think?

[Zimmi48]

If this is meant to be a breaking change, the changelog entry should be much more explicit about this.

[herbelin]

If this is meant to be a breaking change, the changelog entry should be much more explicit about this.

I started investigating how to make it (hopefully) a non-breaking change, by using multiple lists of implicit arguments. It is not so clear how to do in an elegant way though:

• First, this has to exclude constants with flexible conclusion as e.g. in type forall X, X -> X, since this kind of constant have an arity difficult to control syntactically.

• Second, it would be too ad hoc to do it only for Context, so it would have to be done for all kinds of declarations.

• Third, it is not fully clear which range of flexibility we may want. For instance, in

  Set Implicit Arguments.
  Context (f : forall {A} B, A -> B -> Type).
  

  it would certainly be natural that:

  • with 4 arguments, it is @f x y z t (no implicit arguments at all)
  • with 2 arguments, it is @f _ _ x y (the automatic + manual implicit arguments)
  • with 1 argument, it is @f _ _ x
  • with 0 arguments, it is @f _ (the maximal manual one)

  But with 3 arguments, should it fail on the principle that it is 2 implicit arguments or none? Or should it make a hierarchy between manual and automatic implicit arguments and consider either that the manual implicit arguments are stronger, giving @f _ x y z, or that the automatic implicit arguments are stronger, giving @f x _ y z. This is the point I arrived in my thinking.

[Slightly related, but for another PR, @mattam82 suggested me to deprecate automatic declaration of not-in-section Context assumptions as instances, as it was done already for Axiom.]

[Zimmi48]

Dear PR author(s) and contributors, it seems to us this PR may need additional work beyond the 8.12 branching deadline on May 15th.

We are thus removing the 8.12+beta1 milestone; please retarget as appropriate, and also consider updating labels to reflect current status, moving the PR to draft status, etc.

We apologize in advance if we misunderstood the PR status.

[herbelin]

This PR implements/fixes what I think is the expected behavior for Context and, to me, there is no doubt that it is good. The problem was to preserve compatibility. User and developer feedback welcome about how to manage the incompatibilities (a flag, an upgrading script, manual updates, ...)?

[Zimmi48]

I'm slightly worried about your ideas for making this a non-breaking change. I'd much rather advertise this as a breaking bug fix (like the one of Export) and implement the only correct behavior. Have you tried preparing overlays for the affected projects? Naively, I'd think that if the implicit binders were ignored, a backward-compatible fix is just to remove the implicit binders from these projects, wherever they create trouble. If backward-compatible overlays are easy to prepare, then the number of affected projects is not a problem: we should just make sure that the fix is properly advertised in the release notes. But there might be something I don't understand because I'm surprised that the compatibility impact is so large.

In any case: this seems slightly too late for 8.12, but this would still be great to finish this!

[Zimmi48]

BTW, the change to the doc is completely independent of the rest of the PR and should have been its own PR (it would have been merged much faster).

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[Zimmi48]

The number of impacted projects seems so huge that I'm having a very hard time believing that there are really this many projects that used an implicit binder in the type of a variable declared in a Context command. It may instead be the effect of a buggy implementation...

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

Hey, I have detected that there were CI failures at commit 9629257 without any failure in the test-suite.
I checked that the corresponding jobs for the base commit c750baa 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 targets: ci-fiat_crypto, ci-fiat_crypto_legacy.

However, you may want to wait until the pipeline for the base commit (c750baa) finishes.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[Alizter]

ping @herbelin what is to be done with this?

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.

[Zimmi48]

@herbelin Was this PR almost ready for the last two years?