Improve printing of reverse coercions

[proux01]

When a a term [x] is elaborated into [x'] through a reverse coercion, return the term [rev_coerce x' x] that is convertible to [x'] but printed [x], thanks to the coercion [rev_coerce]. Previously, the returned term was directly [x'].

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[CohenCyril]

Fantastic! 🎊
The only thing that worries me is the universe polymorphic status of the constant rev_coerce. It's likely to be used everywhere at various universe levels, so it would make sense to make sure it is universe polymorphic. On the other hand since the main and only current use of this is in an experimental HB/mathcomp branch and HB does not support universe polymorphism yet, it would be premature to make rev_coerce universe polymorphic (unless it already works out of the box, because it might not interact too much with HB?).

• @gares what's your take on it?
• @proux01 would you mind trying making it universe polymorphic?

Nitipicking: since rev_coerce is neither input by the user, nor displayed, I would advise to give it a longer, more "english" name, like reverse_coercion. (And the same for the dummy source and target, spelling out all words, including ReverseCoercionSouce and ReverseCoercionTarget.)

[gares]

A constant, x or x', is always either upoly or not.
We could have 2 reverse_coercion, one of which is upoly.
Moreover, if you don't need upoly you don't want to have an upoly constant around. Maybe I'm just too conservative, but it used to be the case upoly code was more buggy (eg tactics), so I'd rather play safe.

[proux01]

@CohenCyril you're right, done. (there was only one HB.instance not going through in MathComp, but it was easy to workaround (c.f. math-comp/math-comp@9f0ffef) so let's go for it)

[proux01]

@gares do you mean that universe monomorphic constants could'nt cause universe issues with a monomorphic reverse_coercion? I'm not convinced that two different monomorphic constants with different universe levels couldn't cause a conflict by setting additional universe constraints with a monomorphic reverse_coercion (which in my understanding is what @CohenCyril (and I) fear).

[gares]

I think you are right, but then this approach is a bit scary ;-)

I wonder if an uglier encoding would be better, eg .. x .. -> .. (let _original_term : T := x in x') .. and have a special rule for printing this degenerate letin which uses a recognizable ident.

[proux01]

Sounds good except that Eval simpl in (let _original_term := x in x') yields x' which means the nice printing would disappear at the first simplification. Maybe not what we want?

[Janno]

I am very confused by this change but I have no experience with reversible coercions. In any case, instead of changing what is printed this PR seems to change the inferred term instead. Is my understanding correct?

In that case this seems like a very dangerous thing to do. Syntactic pattern matching will have to account for the newly introduced term. Another (related) problem that comes to mind immediately is that this will either slow down or break TC search on classes whose arguments are inferred this way. (Again, I haven't really played with reversible coercions so this might not be possible?) Instead of MyClass my_inferred_structure my_value the inferred term could be MyClass (rev_coerce my_inferred_structure my_original_structured) my_value. If the TC database is transparent by default and my_structure is hint opaque then the search can no longer discriminate based on my_structure and will likely yield too many applicable (but ultimately unsuccessful) hints. If the database is opaque by default the search will likely fail entirely unless the hints similarly have rev_coerce in them, which I don't think is always going to be the case.

On the other hand since the main and only current use of this is in an experimental HB/mathcomp branch

I am not sure what "of this" refers to exactly. If it refers to reversible coercions I know that they already showed up in unexpected (but not unwelcome) places in the form of terms that typecheck in 8.16 when they hadn't before. So they are definitely used in the wild even if people don't necessarily notice.

Sorry if I misunderstood what is going on. I just want to avoid being even more surprised in future coq by what terms really look like compared to what is printed.

[proux01]

I am very confused by this change but I have no experience with reversible coercions. In any case, instead of changing what is printed this PR seems to change the inferred term instead. Is my understanding correct?

Yes and no. This indeed changes the infered term (to something convertible) in order to improve the printing. That's the behavior of (usual, direct) coercions: when one types a : A where a B is expected and f : A -> B is a coercion, then the elaborator replaces a with f a which is displayed as a, unless Set Printing Coercions is activated. Comparatively, for reverse coercions, when the user types b : B where a A is expected and f : A -> B is a reversible coercion such that some a satisfying f a = b can be inferred (via unification, CS or TC search), then the elaborator replaces b with a in the elaborated term. The resulting term is then displayed a whereas we would like it to be displayed b (as in the input term, unless Set Printing Coercions is activated). That's the goal of the current PR: replacing a with something convertible that we could display as b.

[gares]

Sorry if I misunderstood what is going on. I just want to avoid being even more surprised in future coq by what terms really look like compared to what is printed.

If I type 3 where a Z is expected, and Coq fixes it for me, today I see 3 since Z.of_nat is hidden.
If I type nat where an eqType is expected, and Coq fixes it for me, I'd like to see nat as well, but also be able to unravel than the term is actually nat_eqType. This is all this PR tries to do.

Maybe not what we want?

I agree it would be unfortunate. And that we have Opaque for constants, but not for some letins.
I'm fine with the current approach, I'm just scared that using upoly will open a can of worms.

[proux01]

I'm just scared that using upoly will open a can of worms.

Well, that might be a good opportunity to fix many things. (just trying to look at the bright side of it, I perfectly agree with you)

[andres-erbsen]

While I would be very excited to have more concise printing of elaborated code, I think the approach to achieve this needs more discussion. In short, I share the concerns @Janno posted above.

More generally, this PR seems to be based on a unknown-to-me vision of how elaboration and tactic programming would interact, so I have a hard time understanding it. Specifically, I don't see what use coercions would be if using them produced different terms than writing out what you meant in painful detail, because I don't expect most tactics to work on the coercion-derived code. I am getting the sense that the PR authors would consider this acceptable and expected, but I would consider any instance where printing (or anything else) depends on whether the term was originally elaborated using coercions or without to be a bug (and considering "the term" to include a constant specific to the coercion mechanism would be deeply dissatisfying). Concretely, would congruence (and other tactics) need to be updated to interpret (ignore) the new constant to retain their power?

Syntactic pattern matching will have to account for the newly introduced term. Another (related) problem that comes to mind immediately is that this will either slow down or break TC search on classes whose arguments are inferred this way

IIUC, anything like this would be quite costly to support in fiat-cryptography tactics, so if that's the only available behavior, the features affected by this change would be broken as far as I'm concerned. This may not be an immediate practical concern as I am not sure whether we use reversible coercions at all.

[proux01]

[...] whether the term was originally elaborated using coercions or without [...] Concretely, would congruence (and other tactics) need to be updated to interpret (ignore) the new constant to retain their power?

No: reverse coercions are only a way to give a meaning to term that did not typecheck before their introduction. So any tactic will "retain its power" in the sense it should keep handling anything it previously handled in the same way (assuming it is not calling the elaborator and handling its failures in a specific way but most tactic work on already elaborated terms).

Syntactic pattern matching will have to account for the newly introduced term.

Of course, if you start using reverse coercions and feeding this new terms to your own specific tactics, some adptation might be needed to handle the new terms but that's life. Again, this should only be about the new terms, backward compatibility should hold.

Another (related) problem that comes to mind immediately is that this will either slow down or break TC search on classes whose arguments are inferred this way

Here things are likely to work out of the bow as typeclass search will simply unfold the identity reverse_coercion.

I am not sure whether we use reversible coercions at all.

Basically, if your code compiles with any Coq < 8.16, it means you are not.

[Janno]

Another (related) problem that comes to mind immediately is that this will either slow down or break TC search on classes whose arguments are inferred this way

Here things are likely to work out of the bow as typeclass search will simply unfold the identity reverse_coercion.

I suspect you allude to this with "likely" but I'd like to make this a bit more concrete for the benefit of people who do not work with typeclasses a lot: This is only true for hint databases that treat constants as transparent by default. Granted, that is often the case because the opposite behavior makes TC search infeasible outside of very specific and restrictive scenarios. However, when performance is a concern, the only way I know to use TC search effectively and efficiently is to use a transparent-by-default database and to make almost all definitions TC opaque explicitly to benefit from the discrimination nets. Failing hint applications can be very, very expensive and even if every individual one is cheap they add up incredibly quickly when hints look too applicable to the discrimination net. In the development I work on a single missed opacity annotation can make a proof 25%, 50%, 100%, or even 500% slower (depending on where the term in question appears in hint patterns and goal terms).

Obviously one can make reverse_coercion TC opaque but then we might see failing TC searches, especially in databases with tight opacity settings.

[andres-erbsen]

@proux01, thank you for the explanation. My concerns are about keeping the effort required to maintain and write reusable tactics low, not backwards compatibility in the strict sense of whether old code will keep compiling. I understand that code from before reversible coercions were released would not be broken by this change. However, it seems that from a tactic-maintainer's perspective, reverse_coercion might as well be a part of the term AST: unsuspecting users of the tactic would read the Coq reference manual and write terms that appear distinct to the tactic. Further, leaving reverse_coercion uninterpreted is wrong from the perspective of (almost?) all tactics: it instead should be ignored, but not unfolded so that it remains in the output.

The specific example with Fiat Cryptography is also of this form: Jason Gross, Samuel Gruetter, and I maintain a large library of Ltac&Ltac2 code that is used by less experienced but independent and competent engineers, and our tactics not working with code that they wrote following the Coq reference manual would be unwelcome friction. Examples of this kind of issues that we already are running into include primitive vs nonprimitive projections and unipoly annotations. Porting tactics to handle new features in the elaborator's output language is evidently costly: many standard-library tactics have not been updated for those two cases yet, and even those that have been took a while. Thus, I think we should at least consider alternative strategies to achieve the printing improvements in this PR.

[proux01]

However, it seems that from a tactic-maintainer's perspective, reverse_coercion might as well be a part of the term AST:

Right, but its an elaborator think, no need to make it into the kernel.

unsuspecting users of the tactic would read the Coq reference manual and write terms that appear distinct to the tactic.

That's the whole point of having an elaborator.

Further, leaving reverse_coercion uninterpreted is wrong from the perspective of (almost?) all tactics: it instead should be ignored, but not unfolded so that it remains in the output.

I'm not sure I understand this? What do you mean by "leaving reverse_coercion uninterpreted"? What do you mean by "it instead should be ignored, but not unfolded so that it remains in the output."? If you unfold reverse_coercion it will basically disappear since it is just an elaborated identity.

I think we should at least consider alternative strategies to achieve the printing improvements in this PR.

What alternative strategies do you offer?

[Janno]

What alternative strategies do you offer?

The question wasn't direct at me but I wonder if one alternative could be a new kind of cast. A lot of tactics already know to deal with casts and even if the current behavior for casts would need to be adapted at least the adaptation would be a in place that would not be surprising at all for developers precisely because casts already need special handling now.

[gares]

I've mixed feelings about casts. They are source of bugs in many places, but using them here could solve the universe polymorphism problem. x "reverse corced" to x' would be represented as Cast( x' , CastReverseCoercion x) and the pretty printer would display x in normal mode, and x' in printing all mode.

The only problem is that Cast reaches the kernel, and one has to add a line saying that CastReverseCoercion has nothing to do with typing, only with displaying. Hence I summon @coq/kernel-maintainers to get their opinion.

[proux01]

@coqbot run full ci

[tabareau]

@coqbot merge now

[andres-erbsen]

What happened here? (Right until the merge I was under the impression that this was blocked on finding a satisfactory story for tactic compatibility, but it looks like it got merged without that?)

[Janno]

I am equally confused. Was there private discussion that isn't reflected in this MR? It would be nice to understand the reasoning.

[Janno]

Seeing #17484 I am now wondering if the new term will result in more difficulties in tactics that construct terms unsafely. It seems that the application of reverse_coercion to its arguments is typechecked automatically but is there any guarantee that the resulting universe constraints are sufficient to typecheck reverse_coercion in the context into which it is inserted (assuming it would have typechecked without the added reverse_coercion term)?

If this is guaranteed, why did HB need changes?

Also, given that every inserted reverse_coercion term gets fresh universes should this MR have had a benchmark? There could be Qed performance regressions. (Although I am not sure we would catch them given how reverse coercions in general are relatively new and probably not often used.)

[proux01]

If this is guaranteed, why did HB need changes?

HB was designed at a time coq-elpi had no support for universe polymorphism so this kind of bug was somewhat expected.

Also, given that every inserted reverse_coercion term gets fresh universes should this MR have had a benchmark? There could be Qed performance regressions. (Although I am not sure we would catch them given how reverse coercions in general are relatively new and probably not often used.)

You have your answer, reverse coercions are too recent to get enough use in the CI codebase for a benchmark to be of any interest.

[gares]

If this is guaranteed, why did HB need changes?

Since Coq 8.5 a term which is well typed can be rejected by the kernel if it is not accompanied by its universe constraints (even if the kernel is able to infer the missing ones, a bad choice IMO, but that is OT). Tthat explains the bug:
the code in HB was wrongly passing to the kernel well typed terms without all the universe constraints, the extra calls to coq.typecheck are amending that (typecheck is not the kernel typecheck, it is the pretyper one which happily infers the constraint and, in the elpi API, stores then in the current state).

In some sense this patch exposed a bug which was already there (w.r.t. the spec of Coq's kernel).

[Janno]

I am aware of the kernel's requirements. In the kind of automation I write I usually insert strategic calls to typechecking to generate exactly the constraints that are necessary to make the kernel accept the full proof term. In many cases this boils down to typechecking a partial application to which the remaining arguments are then added unsafely. But most of the time we can bypass typechecking entirely since we know exactly that all the constraints are already established by some other mechanism.

I was wondering if I should except breakage from schemes like that due to reverse_coercion possibly showing up with fresh universes.

[gares]

Given your code does not use the feature of reverse coercions, I think you should not see any change.