Put cyclic numbers in sort Set instead of Type

[VincentSe]

Kind: Performance.

Numbers are in Set, there is no need to send them into higher universes.

Overlays PRs:

• Put cyclic numbers in sort Set instead of Type coq-community/bignums#47
• Put cyclic numbers in sort Set instead of Type fblanqui/color#30
• Put cyclic numbers in sort Set instead of Type thery/coqprime#25

[VincentSe]

@Zimmi48 Hello, this pull request should be executed and merged together with that PR in bignums coq-community/bignums#47. Do you know how to do that ?

[Zimmi48]

You can add an overlay to this PR (see https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md) to make CI pass. Then, it's up to the assignee to merge the two at the same time or to request one of the core developers to merge the bignums PR once this one is merged.

[Zimmi48]

Testing with the overlay for bignums shows that there is still a compatibility issue.

[VincentSe]

@Zimmi48 I just fixed the bignums pull request. How can we restart the continuation integration in this PR ?

[Zimmi48]

@VincentSe See https://github.com/coq/coq/blob/master/CONTRIBUTING.md#gitlab-documentation-tips-and-tricks. If you request access to the Coq organization on GitLab, this will give you the ability to restart failing jobs.

[Zimmi48]

As far as I understood, the bignums overlay is not backward-compatible. This was already a bit of an edge-case, because a change to the standard library should in principle always come with backward-compatible fixes. However, given that bignums is a plugin and quite close to Coq, it still seemed OK. However, now I see that coqprime (and maybe others like color?) may need overlays as well. Are those backward-compatible? We really shouldn't merge this change if we cannot provide backward-compatible fixes because we must always preserve the ability for Coq library authors to be compatible with two successive versions of Coq.

[VincentSe]

@Zimmi48 Then what do you propose ? We could duplicate Set and Type versions of cyclic numbers in the stdlib and only change bignums to use the new Set version.

[Zimmi48]

I have no idea because I'm far from being a sort and universe expert, but I am surprised that there is no way to get backward-compatible fixes for this kind of changes (cc @coq/universes-maintainers). As for the solution you propose, it would still have the drawback that people who depend on bignums wouldn't be able to maintain compatibility with two successive Coq versions (unless the duplication is also done in bignums, with some deprecation for the old version).

[VincentSe]

The problem is this type of binary trees

Fixpoint word (w:Type) (n:nat) : Type :=
 match n with
 | O => w
 | S n => zn2z (word w n)
 end.

When the node type w is in Set, Coq fails to prove that word w n is also in Set.

[SkySkimmer]

It could be made universe polymorphic (as a transition step or permanently)

[SkySkimmer]

The overlays seem to be all about replacing some Type occurences with Set, an alternative though perhaps a bit hacky would be to have them define Definition univ_of_cycles := ltac:(first [idtac;let _ := constr:(word : Type -> Type) in exact Type | exact Set]) or some such thing and then use that.
Or as a transition step we can define univ_of_cycles := Type in 8.13 and change it to Set in 8.14.

[VincentSe]

@SkySkimmer Making word universe polymorphic helps, but this still fails in bignums

Definition titi : Set := BigN.t.

It should succeed because BigN.t is int which is in Set. I suspect module types to prevent the universe checker to do its job.

@Zimmi48 These universe polymorphism and ltac hacks, even if I managed to make them work, hide a bug. Numbers should have been in Set in the stdlib right from the beginning. Because they were not, the bug leaked to packages bignums, coqprime and color. Is backward compatibility a reason for not fixing bugs ? What's the problem with upgrading 3 more packages when people choose to upgrade Coq ?

[Zimmi48]

By submitting a backward-incompatible overlay to Coq libraries, we break the contract with their maintainers. Indeed, this means that until Coq 8.13 is released, their main branch won't be compatible with any released version of Coq anymore. Furthermore, many Coq users and library authors like to keep projects that are compatible with several versions of Coq. The fact that we have to fix several CI projects in a backward-incompatible way can mean that there will be several more out-of-CI projects that will need to be fixed in the same way.

Yes, bugs should be fixed, but some bugs take longer to be fixed than others because of the consequences of fixing them. In this case, the absence of an easy backward-compatible fix shows a limitation of Coq (you cannot easily say "give me the universe of this object"). The solution proposed by @SkySkimmer to introduce a univ_of_cycles in 8.13 and rely on it to provide a backward-compatible fix for this bug fix in 8.14 looks reasonable to me even though it will delay everything.

[spitters]

Mike Shulman once managed to abuse the strange behavior of modules wrt universes:
https://homotopytypetheory.org/2015/07/05/modules-for-modalities/

Meanwhile, that use has been removed from the HoTT library.

Is there a rationale of the way modules currently work wrt universes?

[VincentSe]

@Zimmi48 @SkySkimmer @spitters I implemented the ltac trick of @SkySkimmer in all 3 overlays, which now build against stdlib both before and after this fix. Is it enough for backward compatibility ?

[JasonGross]

The solution proposed by @SkySkimmer to introduce a univ_of_cycles in 8.13 and rely on it to provide a backward-compatible fix for this bug fix in 8.14 looks reasonable to me even though it will delay everything.

The Ltac trick is fine, but this one is not, as fiat-crypto depends on coqprime, and I would like to keep fiat-crypto compatible with the latest version of Coq released in apt packages in a stable Ubuntu distribution (which is currently 8.11; note that fiat-crypto is currently maintaining backwards compatibility with 8.9, but we'd be willing to bump that to 8.11).

[VincentSe]

@JasonGross

The Ltac trick is fine, but this one is not

I don't understand, I thought I implemented the ltac trick. What would you have done ?

[JasonGross]

@VincentSe, sorry, the solution you implement is fine; I was objecting to "Or as a transition step we can define univ_of_cycles := Type in 8.13 and change it to Set in 8.14."

[SkySkimmer]

univ_of_cycles can be used in a more backward compatible way too. Suppose Coq 8.13 defines univ_of_cycles := Set, libraries can define a compat module containing univ_of_cycles := Type, then import the compat module before the Coq one:

• pre 8.13 gets the compat module's univ_of_cycles
• 8.13+ Coq's univ_of_cycles shadows the compat one

[Zimmi48]

This is fine to me but the compatibility-breaking change needs to be documented in the changelog (and instead of explaining the Ltac trick there, a link could be provided to an example of commit with the backward-compatible fix).

Also, this PR needs an assignee from the @coq/stdlib-maintainers and after it has been approved but before it is merged the overlays should get merged by the various project maintainers (any Coq core dev for bignums).

[VincentSe]

@Zimmi48 changelog added.

[anton-trunov]

@VincentSe I took the liberty to put a small TODO list in the top comment to keep track of the overlay PRs.

[VincentSe]

@anton-trunov Thanks !

[coqbot-app]

For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit 0c39f0b: Put cyclic numbers in sort Set instead of Type

[coqbot-app]

For your complete information, the job test-suite:base+async in allow failure mode has failed for commit 0c39f0b: Put cyclic numbers in sort Set instead of Type

[VincentSe]

@anton-trunov Hello, the pull requests to coqprime and color have been merged, can you merge the last overlay in bignums, and then this pull request to the stdlib ?

[anton-trunov]

@VincentSe Great, thank you! Looks like I'm not authorized to merge those changes in bignums. @Zimmi48 could you please help us ping the relevant maintainers?

[Zimmi48]

PR merged

[anton-trunov]

@Zimmi48 Thanks! coqtail failure in CI looks unrelated. Should we proceed with merging then?

[Zimmi48]

Yes, it's unrelated.