Only allow universe level comparisons to fail with type-in-type

[yannl35133]

Discussion is needed on what to do with Prop ≤ Type

Fixes: #20241 #20667
Related: #15270 #16620 #21351

Overlays

• (awaiting a better fix) Adapt to rocq-prover/rocq#21531 (stricter Type in Type) math-comp/hierarchy-builder#573
• Adapt to rocq-prover/rocq#21531 (stricter type-in-type) rocq-community/rocq-lean-import#57

[ppedrot]

what to do with Prop ≤ Type

I'd say this always holds.

[yannl35133]

The better question would be what to do with Type ≤ Prop ?

[ppedrot]

This one should probably fail, even though that's not what we've been doing so far. Allowing this we can probably get into trouble with the rules for impredicativity, leading to SR breakage. It's not because we're inconsistent that we don't care about other good metatheoretical properties!

[mattam82]

I think we should disallow Type <= Prop still in -type-in-type mode

[yannl35133]

That should be what happens in this PR, and most errors in the test suite are due to this (some are due to Type ≤ SProp not holding)

[ppedrot]

I don't really care about the tests but I'm mostly concerned about the legendary type-in-type development known as UniMath. Let's @coqbot run full ci

[yannl35133]

Tested locally, Unimath compiles after the minor overlay (fixes a test)

[yannl35133]

This was in draft because it needs discussion, but it can actually still get reviewed at the same time.

[ppedrot]

The changes seem desirable to me. There are probably a few places that are still behaving weirdly in the upper layers with type-in-type, but the kernel changes are a net improvement.

[yannl35133]

I went over all calls to type_in_type in the codebase and hopefully made them all align with the new semantics. In practice, the only remaining calls are in UGraph and UState, the rest is all about printing whether the flag is set.

[yannl35133]

• lean-importer needs to unsafely eliminate from SProp to Type, so either a flag to reenable this or a way to allow an SProp ~> Type elimination constraint globally will be needed at some point.
• hb_test needs fixing as well, but I don't understand the test well enough to fix it
• 3 tests in the test-suite need fixing, not clear how to though
  • bug_20242 can be changed to stop relying on type in type
  • I don't think bug_16204 can be adapted, a universe level issue wouldn't have caused the anomaly
  • bug_4403 the issue and the test look unrelated, the test can obviously not work anymore

[SkySkimmer]

@JasonGross the lean importer will need some adaptation to this PR, not entirely sure how.
Essentially inductives in lean Prop with unrestricted elimination will not have it in rocq SProp with default flags if they have a constructor.
Typically I think this means either prod, which gets turned into a primitive record so it's fine, and Acc.
For Acc we currently unset universe checking which gives it unrestricted elimination, with this PR it doesn't work.

One possibility is to have a new flag in rocq to unset the problematic checking elimination, separate from universe checking.

@ppedrot suggested generating the recursor with guard checking off and a dummy unit argument, ie
Acc_rect A R P f := (fix Acc_rect (x:A) (a:Acc R x) (dummy:unit) {struct dummy} := match a with Acc_intro a' => f x a' (fun y r => Acc_rect y (a' y r) dummy) end) tt
not sure how well that would work

[yannl35133]

I added a typing flag for backwards compatibility of plugins (it's not accessible from the outside).
It's not entirely polished, it's especially missing indications of its inherent danger (by putting it in Internal), this is to get some feedback for now.

[ppedrot]

I know we already don't do that with UGraph, but I think this is an API defect: this function should be one-off, i.e. of type t -> t so that there is no way to go back to a state where we check constraints again. After setting it all hell breaks loose and invariants are obliterated.

[ppedrot]

Hmm, should have turned my tongue seven times in my mouth: we do want to be able to set the flag locally, so no, the API is fine. That said I have no idea what it means in the semantics.

[yannl35133]

I can't see it be worse than how type-in-type currently behaves, which is the best we can hope for.

[ppedrot]

🤷

[ppedrot]

@coqbot run full ci

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 21531-Yann-Leray-stricter-type-in-type.sh