Adapt to coq/coq#17836 (sort poly)

[JasonGross]

Maybe we should start versioning this file?

[ppedrot]

Please merge now.

[samuelgruetter]

Please merge now.

The reason I waited with merging this for so long is that this PR does not work with any released version of Coq. I was hoping that Coq would provide some backwards-compatible term destructor functions to deal with this in a minor update (eg in an upcoming 8.18.1 and/or 8.17.2). Is there still some chance this is going to happen?

If not, does this mean that each project that wants to use Constr.Unsafe either needs to implement some Coq version detection mechanism and conditional file inclusion in its Makefile, or refrain from using any Constr.Unsafe parts that are likely getting modified in the future?

[andres-erbsen]

See also https://github.com/coq/coq/pull/17836#issuecomment-1724247453

[ppedrot]

For Unsafe API we make no promise about stability. We try to keep backwards compatibility as much as possible, but sometimes you have to reflect the kernel changes to the upper layer. A way to make the API more robust is to provide a bunch of accessors and view types, but fundamentally the term AST is tied to the Coq version and the current type theory implemented by it.

[samuelgruetter]

Thanks for the clarification @ppedrot :+1: So do you agree that accessors like eg destProj, which exists in Coq-version-specific variants in the rewriter project, would preferably be put directly into Coq's Ltac2 library?

[SkySkimmer]

destProj should be in the Ltac2 stdlib, but note that it's not compatible either (returns a 3-tuple instead of 2-tuple since 8.19).

[JasonGross]

note that it's not compatible either (returns a 3-tuple instead of 2-tuple since 8.19).

This is true, but destProj is much easier to shadow in a Compat file, which would give an easy way to maintain compatibility across at least two to three versions of Coq without having to version code user-side. (Plausibly the PR should have shadowed the entire Constr.Unsafe.kind data type in the Compat file, but that's much heavier.)

[samuelgruetter]

Or instead of destProj, there could be separate accessors for each of the 2 (or 3, starting with 8.19) fields, eg Constr.getProjProjection, Constr.getProjRelevance, Constr.getProjRecord (or preferably better names :stuck_out_tongue:)

[JasonGross]

Or instead of destProj, there could be separate accessors for each of the 2 (or 3, starting with 8.19) fields, eg Constr.getProjProjection, Constr.getProjRelevance, Constr.getProjRecord (or preferably better names 😛)

In this case, it's probably better to have destProj return a record?

[ppedrot]

Records are a bit more robust for elimination rules, but they are not great for introduction rules as one has to provide all the fields. A reasonable balance for robustness is to also provide a helper builder with default values that can be overridden e.g. using with clauses. I've never implemented this yet but now that Ltac2 is getting traction we should be converging towards an API and a coding style enforcing future-proof scripts, so all proposals / comments are welcome.

[ppedrot]

Regardless of the API discussion, IIUC this PR should be closed as an alternative fix was merged?

[samuelgruetter]

Regardless of the API discussion, IIUC this PR should be closed as an alternative fix was merged?

Yes, closing