feat: Remove Type eliminates to any sort by default

[TDiazT]

This PR depends on #21417 .

This PR removes the default behavior of Type eliminating to any sort.

Associated RFC : rocq-prover/rfcs#111.

---

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
• Opened overlay pull requests.

[SkySkimmer]

Why?

[JasonGross]

Right now we have eq in Type implies eq in SProp, and not the other way around.
Is this PR going to allow the possibility of reversing this, so that we can have a nonfibrant sort with univalence and a variant of SProp that can be treated to some extent as reflecting judgmental equality? (Or do we already have that possibility, so long as we don't say that Type is the fibrant sort?)

[thomas-lamiaux]

I do imagine we would want to keep Type -> Prop / SProp but potentially not for any fresh shorts we would add ?
I don't think there are much SortPoly code out there that would rely on Type eliminating to every sort, so it should be fine

[tabareau]

@coqbot run full ci

[tabareau]

Why?

Type eliminates to any sort is an unnecessary constraint. In particular, it is not compatible with a more general mechanism for erasure/extraction that @jrosain is working on.

[tabareau]

Right now we have eq in Type implies eq in SProp, and not the other way around. Is this PR going to allow the possibility of reversing this, so that we can have a nonfibrant sort with univalence and a variant of SProp that can be treated to some extent as reflecting judgmental equality? (Or do we already have that possibility, so long as we don't say that Type is the fibrant sort?)

Indeed, the idea for adding a univalent sort would rather be "don't say that Type is the fibrant sort". Note that the fact that equality in SProp can be eliminated to other sorts (as in observational type theory) is not an elimination constraint but rather a specific rule for equality which admit a "cast" operator that can be used to emulate J/elimination of equality.

[SkySkimmer]

Does this interact properly with nested schemes (#21429 etc)?

With nested schemes the _all scheme puts arbitrary sort data in a Type, eg prod_all:

Inductive prod_all@{sPA sPB;+} A (PA:A -> Type@{sA;_}) B (PB:B -> Type@{sB;_}) : Type :=
  pair_all a (_:PA a) b (_:PB b) : prod_all A PA B PB (pair a b).

for scheme generation we don't actually eliminate it, but when we want to use the scheme we will want to eliminate it and typically expect prod_all A PA _ _ (x,y) -> PA x to hold.

[thomas-lamiaux]

ind_all is in the same sort as the sort of ind so that it is possible to prove ind_all_forall.
This could be generalised once sort constrains PR are fully merged

[TDiazT]

Does this interact properly with nested schemes (#21429 etc)?

With nested schemes the _all scheme puts arbitrary sort data in a Type, eg prod_all:

Inductive prod_all@{sPA sPB;+} A (PA:A -> Type@{sA;_}) B (PB:B -> Type@{sB;_}) : Type :=
  pair_all a (_:PA a) b (_:PB b) : prod_all A PA B PB (pair a b).

for scheme generation we don't actually eliminate it, but when we want to use the scheme we will want to eliminate it and typically expect prod_all A PA _ _ (x,y) -> PA x to hold.

I don't know, but at a first glance it seems like it would conflict and that someone (?) would need to add the Type -> sB constraint in the eliminator (if I'm understanding correctly)

[tabareau]

Does this interact properly with nested schemes (#21429 etc)?
With nested schemes the _all scheme puts arbitrary sort data in a Type, eg prod_all:

Inductive prod_all@{sPA sPB;+} A (PA:A -> Type@{sA;_}) B (PB:B -> Type@{sB;_}) : Type :=
  pair_all a (_:PA a) b (_:PB b) : prod_all A PA B PB (pair a b).

for scheme generation we don't actually eliminate it, but when we want to use the scheme we will want to eliminate it and typically expect prod_all A PA _ _ (x,y) -> PA x to hold.

I don't know, but at a first glance it seems like it would conflict and that someone (?) would need to add the Type -> sB constraint in the eliminator (if I'm understanding correctly)

No as @thomas-lamiaux was saying, we fix the return sort of prod_all to be the same as the one of prod, not necessarily Type. So we use reflexivity of elimination constraints.

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

Suggested change

	`Type` does not eliminate to any sort by default
	`Type` does not eliminate to every sort by default

? it still eliminates to Prop & SProp right?