Spurious universe inconsistencies in Coq 8.19 with abstracted proofs.

[silene]

Some of my large proofs break in Coq 8.19. Inserting the following command at the failure point

exfalso ; clear ; assert True by abstract (exact I).

gives

Universe inconsistency. Cannot enforce Set = Foo.154 because Set < Foo.154.

Forcefully ending the proof with apply FALSE. Qed. succeeds without triggering an universe inconsistency. So, the inconsistency does not seem to be present in the current proof term, but instead to be in the proof term created by abstract (or in its application to the current goal).

Unfortunately, I do not have a small reproducer. (This can be triggered by compiling the master branch of CoqInterval.)

[silene]

Here is a reduced testcase.

Polymorphic Axiom array@{u} : Type@{u} -> Type@{u}.
Polymorphic Axiom get : forall {A} (t : array A), A.

Lemma foo (t: array nat): True.
Proof.
assert True by abstract exact I.
assert (v := get t).
abstract exact I. (* Universe inconsistency. Cannot enforce Top.5 = Set because Set < Top.5. *)
Qed.

[ppedrot]

Probably a side-effect of #17745, cc @SkySkimmer

[SkySkimmer]

The reason the first abstract changes the behaviour is that it changes which branch we take in

coq/vernac/declare.ml

Line 1826 in 3d86c1d

|| not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))

Why we have this code is not clear but removing it (so it becomes just if not poly && keep_body_ucst_separate) causes undefined universe anomaly at

coq/test-suite/success/rewrite.v

Line 50 in 3d86c1d

Qed.

In any case with this code and fea5fcc (indeed from #17745) we use an unminimized initial_euctx which has {foo.5} |= Set = foo.5 which is added to the global env (we are in univ monomorphic mode), and since monomorphic universes are declared > Set we get the error.

I guess short term we should revert fea5fcc and long term we should look into not checking is_empty_private_constants.

[SkySkimmer]

revert at #18640