Global sorts don't block template polymorphism

[yannl35133]

Description of the problem

Global sorts don't block template polymorphism, even though it can't work.

Small Rocq / Coq file to reproduce the bug

Sort s.
Inductive I : Type@{s; _} := C.
(* Universe inconsistency. Cannot enforce Prop <= Type@{s | Set}. *)

Version of Rocq / Coq where this bug occurs

9.1,9.2

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

before global sorts?

[SkySkimmer]

What does "it can't work" mean?
AFAIK Inductive I@{u} : Type@{s; u} := C. should be possible to be template poly on u

[yannl35133]

I might have been a bit presumptuous in my statement since I don't know how well template polymorphism and non-ground sorts interact, but I thought not being Relevant would prevent template from working. (AFAIU global sorts still have variable relevance)

[SkySkimmer]

RelevanceVar of a global sort should be considered just a constant relevance as far as template poly is concerned.

[yannl35133]

This is where the problematic constraint is enforced:

rocq/vernac/comInductive.ml

Lines 393 to 400 in 980755c

	let non_template_levels sigma ~params ~arity ~constructors =
	let ctx, u = EConstr.destArity sigma arity in
	(* locally making the conclusion qvar above_prop means its
	appearances in relevance marks aren't counted *)
	let sigma = match ESorts.kind sigma u with
	| QSort (q, _) -> Evd.set_above_prop sigma (QVar q)
	| _ -> sigma
	in

I don't know how to change this, do you want to take over?

[SkySkimmer]

We could do the set_above_prop only when the qvar is a unif qvar (ie not a global).
(maybe global qualities shouldn't be in qvar.t.)

Inductive ofTy A : Type@{s;_} := OfTy (_:A).

is also interesting, with my proposed change it fails with "Cannot handle sometimes squashed template polymorphic type."

with your change, or equivalently

Definition s := Type@{s;_}.
Inductive ofTy A : s := OfTy (_:A).

it infers A in sort s (at separate, non template poly universe).

[SkySkimmer]

#21668

[yannl35133]

(maybe global qualities shouldn't be in qvar.t.)

I imagine at some point ground sorts and global sorts will have to be merged.

Definition s := Type@{s;}.
Inductive ofTy A : s := OfTy (:A).

it infers A in sort s (at separate, non template poly universe).

Why does it do that? This looks like a bug to me.