Add a deprecation warning to > in Class

[proux01]

This follows a discussion in #2643

Currently, field :> field_type declares field a coercion in every record declaration, except typeclasses where it is instead declared a typeclass instance. It seems more principled to remove that exception (so in typeclasses, both an instance and a coercion are declared).

This is currently only introducing a warning to start a deprecation phase.

Adresses #2643 #9014

• Added / updated test-suite.
• Added changelog.
• Added / updated documentation.

Overlays (backward compatibles, kindly provided but don't need to be merged in sync with the current PR):

• Adapt to coq/coq#15802 math-comp/analysis#599
• Adapt to coq/coq#15802 HoTT/Coq-HoTT#1640
• Adapt to coq/coq#15802 mit-plv/fiat#68
• Adapt to coq/coq#15802 jwiegley/category-theory#27

[coqbot-app]

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

[coqbot-app]

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

[coqbot-app]

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

[coqbot-app]

🔴 CI failures at commit a876a4a without any failure in the test-suite

✔️ Corresponding jobs for the base commit 47ad43b succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-hott

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

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

[coqbot-app]

🔴 CI failures at commit 4abedb4 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 47ad43b succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-hott

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

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

[SkySkimmer]

This isn't a deprecation, it's a behaviour change.

[proux01]

Yes, you read it before I had time to update the title, fixed.

[SkySkimmer]

We should have a deprecation phase

[proux01]

You mean putting a warning telling a coercion will be added in the future? why not.

[Alizter]

I think it will take at least 3 version before we can make :> mean coercion. We need two for the deprecation phase, and ideally we would leave one version where it isn't supported at all to make sure nobody accidentally starts using coercions.

I see that you've used export for the locality of the existing instances, was this the case before?

[proux01]

and ideally we would leave one version where it isn't supported at all to make sure nobody accidentally starts using coercions.

I'm not sure I get this last one, we are talking about adding coercions, not deleting anything. So for me, this third version would be the exact same as currently: no change and no warning, what's the point?

[proux01]

We could have a version where :> in Class gives a plain error, but that's likely to break much more code than needed. About a small third of the CI (14 to 19 targets) seems to use the feature (instance), most of them not caring about the coercion and some explicitly declaring them. In the CI, only category-theory needs the instances but is harmed by the coercions.

[RalfJung]

I agree that having the same syntax do two different things is confusing, and I was startled by this myself many years ago. However, the new behavior of :> on a Class (both instance and coercion) is essentially never what you want, and it is still different from what :> does everywhere else. So this makes the situation strictly worse than it was before.

The proper solution, IMO, is to have a syntax for only the coercion, and a syntax for only the instance. I think the transition plan for this should look as follows:

• Add the "only instance" syntax
• A release later, deprecate the :> instance in Class
• A release (or several releases) later, change the meaning of :> in Class from "only instance" to "only coercion"

This gives precedence to the :> usecase outside of Class. My personal preference would be for :> to mean "only instance" and use some other syntax for "only coercion". At least for the code I maintain, that would lead to much less churn -- but this of course depends heavily on the style of one's codebase.

[SkySkimmer]

A release later, deprecate the :> instance in Class

Why wait? If we want 2 releases with both syntaxes we can just keep warning for both releases.

[SkySkimmer]

cc @ppedrot we may want to revert this PR for 8.16

[RalfJung]

Why wait? If we want 2 releases with both syntaxes we can just keep warning for both releases.

We'll have to allow that warning in std++ and Iris then if we want to support more than one Coq release. I think it is nicer to users to wait a bit before deprecating things in favor of new things that have only just been introduced. (The quick deprecation of Hint Rewrite without Global/Local is still rippling through our ecosystem.)

For now this is only a deprecation, and we don't have plans to go through with removing it until we provide an alternative shorthand for instances.

Ah, I misunderstood then, I thought this was a behavior change. Thanks for clarifying.

Still I think this deprecation is too early. Unless there is some automatic way for us to adjust the code to the new style, we will just allow the warning and wait for such an automatic way to be available -- which seems a lot easier when it is about replacing :> with ::, rather than adding some Existing Instance stuff after the Class declaration.

[SkySkimmer]

We'll have to allow that warning in std++ and Iris then if we want to support more than one Coq release. I think it is nicer to users to wait a bit before deprecating things in favor of new things that have only just been introduced

I disagree, IMO the warning is the primary way to communicate intended changes to users (we can't expect everyone to watch PRs) so it's better to have it early. Allowing the warning if you don't want to deal with it immediately is a fine solution.

[RalfJung]

Could the warning state that the suggested alternative needs Coq version X to work? The Hint Rewrite thing comes up every few months (some repo I haven't looked at in a while triggers the warning) and basically each time I first add the Local and then CI tells me I broke some older Coq version that we still support. This costs a lot more time than it has to. I cannot keep in my head for all Coq features which exactly is the minimal version they need.

[proux01]

* I don't see any way to take _advantage_ of the coercion (and nobody has claimed there is)

As noted above, in the CI all projects but category-theory are unharmed by the extra coercions and a few project even actually want them. So this statement looks pretty wrong.

Anyway, there is now a specific request for a syntax to make field instances (but not coercions),
so I guess we should proceed as follows:

• add a new syntax, as offered by @Alizter above in version X (either 8.16 or 8.17, and removing the current warning if X=8.16)
• update the warning to mention that the new syntax is available since version X
• in version X+2, remove the deprecation and fix :> to finally mean coercion everywhere

[Zimmi48]

Could the warning state that the suggested alternative needs Coq version X to work? The Hint Rewrite thing comes up every few months (some repo I haven't looked at in a while triggers the warning) and basically each time I first add the Local and then CI tells me I broke some older Coq version that we still support. This costs a lot more time than it has to. I cannot keep in my head for all Coq features which exactly is the minimal version they need.

That's a good idea, and this is still time to do it right for the Hint Rewrite warning. Feel free to open a PR.

[Zimmi48]

I support @SkySkimmer's suggestion to revert this PR in 8.16 if the new plan is #16224.

[RalfJung]

As noted #15802 (comment), in the CI all projects but category-theory are unharmed by the extra coercions and a few project even actually want them. So this statement looks pretty wrong.

Based on many years of painful experience, I consider all coercions harmful by default until proven otherwise.

Of course, adding a coercion doesn't break a build, but it can still break printing by making goals impossible to interpret. CI wouldn't catch almost any of the things that make coercions painful.