Add elaboration of qualities

[TDiazT]

This PR depends on #21417 .

This PR adds elaboration of (implicit) qualities, which is enabled by setting the flag Universe Polymorphism and disabling a new flag Collapse Sorts ToType.

Associated RFC : rocq-prover/rfcs#111.

Examples

The test file test-suite/success/sort_poly_elab.v has been updated with more examples.

Set Universe Polymorphism.
Unset Collapse Sorts ToType.

Definition qsort := Type.
(* qsort@{α ; u |} = Type@{α ; u} : Univ@{u+1} *)

Definition qsort' := Type.
(* qsort'@{u} : Type@{u+1} *)

Inductive implicit := mk.
(* implicit@{α ; u} : Type@{α ; u} *)

Inductive foo1 : Type := .
(* foo1@{α ; u |} : Type@{α ; _} :=  . *)

Inductive sigma (A:Type) (B:A -> Type) : Type
    := pair : forall x : A, B x -> sigma A B.
  (* sigma@{α α0 α1 ; u u0 u1} : forall (A : Type@{α ; u}) (_ : forall _ : A, Type@{α0 ; u0}), Type@{α1 ; u1} *)

(* Elimination constraints are added *)
Definition pr1 {A B} (s:sigma A B) : A
  := match s with pair _ _ x _ => x end.
(* α α0 α1 ; u u0 u1 |= α1 -> α *)

Definition pr2 {A B} (s:sigma A B) : B (pr1 s)
  := match s with pair _ _ _ y => y end.
(* α α0 α1 ; u u0 u1 |= α1 -> α
                                    α1 -> α0 *)

Overlays

• Adapt to rocq-prover/rocq#21450 (Update esearch_fix_guard to return evd) mattam82/Coq-Equations#688

---

• Added / updated test-suite.
• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
• Opened overlay pull requests.

[tabareau]

@coqbot run full ci

[TDiazT]

I found a bug when declaring a variable in Type in a section, so I still need to check that.

Set Universe Polymorphism.
Unset Collapse Sorts ToType.

Section Test.
  Variable (A : Type).
  (* Anomaly "File "kernel/safe_typing.ml", line 698, characters 11-17: Assertion failed." Please report at http://rocq-prover.org/bugs/. *)

Which comes from this check:

  let check_quality q =
    Sorts.QVar.is_global q &&
    not (QGraph.is_declared (Sorts.Quality.QVar q) (Environ.qualities senv.env))
  in
  let () = assert (Sorts.QVar.Set.for_all check_quality (fst qctx)) in

Apart from that, I think the projections are now currently elaborated with their appropriate elimination constraints, not just collecting.

[SkySkimmer]

Currently we expect that all qvars in the global env (including section qualities) are QVar.is_global, this check enforces that.
The alternatives are Unif and debruijn variables so neither really seem to fit in the section context. (debruijn variables wouldn't work with instantiating pomymorphic objects I think)

[TDiazT]

@ppedrot Why should sort variables be only global inside a section? According to the assertion:

  let check_quality q =
    Sorts.QVar.is_global q &&
    not (QGraph.is_declared (Sorts.Quality.QVar q) (Environ.qualities senv.env))
  in
  let () = assert (Sorts.QVar.Set.for_all check_quality (fst qctx)) in

What cases is this assertion protecting from?

[SkySkimmer]

The change in the output for FixpointNoElim is because in master this search_guard fails, and in this PR we ignore the returned evar map (which would have an added s -> Prop) and then the kernel fails.

I'm not sure to what extent this is a problem, but it doesn't seem great.

[SkySkimmer]

why isn't this using Constr.fold?

[TDiazT]

Because I didn't notice there was that function 🤷

[SkySkimmer]

instead of comments which are not checked by anything, this should be an output test (with an added About instead of the comment)

alternatively we could write some code to check that the expected thing is produced but it would get verbose, eg to check that an expected definition foo@{s s'; | s -> s'} we have to do

Fail Definition foo_check@{s s';|} := foo@{s s';}. (* missing elim constraint *)
Definition foo_check@{s s';|s -> s'} := foo@{s s';}.

and if there is more than 1 elim constraint fully checking it gets exponential (we have to check that every strict subset of the constraints is rejected)

[TDiazT]

Yup, those were more for documentation, if someone looks at the test without needing to run them. I'll add the output tests.

[SkySkimmer]

I'd prefer for the whole test to be moved to output and every comment be accompanied by a About

[TDiazT]

Ok

[SkySkimmer]

this API seems a bit awkward (to_type is ignored when collapse = false) but IDK what would be better

[TDiazT]

Yeah, I agree. The only use I've seen for collapse is for template I think.

[SkySkimmer]

not sure what "possible sorts" means, is it "for each fixpoint the pair of structural argument's sort and output's sort"?
also since type in type isn't per-fixpoint it should be _ array option not _ option array

[TDiazT]

I'll edit it, don't actually remember.

[SkySkimmer]

@ppedrot Why should sort variables be only global inside a section? According to the assertion:

  let check_quality q =
    Sorts.QVar.is_global q &&
    not (QGraph.is_declared (Sorts.Quality.QVar q) (Environ.qualities senv.env))
  in
  let () = assert (Sorts.QVar.Set.for_all check_quality (fst qctx)) in

What cases is this assertion protecting from?

It stops us from putting Var qvars in the section context (this would either produce errors or cause inconsistencies), and also Unif qvars (they would probably work ok but it's strange to have "unification" variables in the section context).

changed

[TDiazT]

It stops us from putting Var qvars in the section context (this would either produce errors or cause inconsistencies), and also Unif qvars (they would probably work ok but it's strange to have "unification" variables in the section context).

How is it handled for universe levels ? Can we use the same approach?

[SkySkimmer]

For univ levels unif and global are the same
This is generally considered not great
@ppedrot ?

[ppedrot]

How is it handled for universe levels ? Can we use the same approach?

No, we shouldn't reflect the level implementation for sorts, and this is a hill I will die on. Monomorphic sorts are like constants, not unification variables.

For sections I'm open to discussion, but I'm still quite convinced that allowing unification of section-local sorts is a bad idea. It's less crazy than unification of global sorts since there is an explicit scope, but still. As for the precise way to implement it, I don't know whether we should use QVars or globals, but this is mostly an implementation detail, both are observationally equivalent except maybe for some printing functions.

[TDiazT]

Monomorphic sorts are like constants, not unification variables.

Sounds fair.

For sections I'm open to discussion, but I'm still quite convinced that allowing unification of section-local sorts is a bad idea. It's less crazy than unification of global sorts since there is an explicit scope, but still. As for the precise way to implement it, I don't know whether we should use QVars or globals, but this is mostly an implementation detail, both are observationally equivalent except maybe for some printing functions.

I'm unfamiliar with how exactly the section context works wrt. to definitions in the section, so in order to clarify a little bit:

With the local assumption Variable (A : Type) I would get a fresh Unif sort variable for Type. Then, what exactly is it that you are suggesting?

• That we should elaborate this sort variable as a Var/Global one, instead of a Unif, when inside a section?
  I imagine not, since there shouldn't be section-specific logic in the elaboration/pretyping phase.
• that we should somehow store this unif variable in the section context as a QVar or Global one?
  In this case, I imagine there might be issues when typing other terms, since the sort variable for A is different than the one in the context. Unless you keep some kind of mapping between them?
  Otherwise, maybe substitute these Unif variables for the QVar ones that are now stored in the context? (This doesn't sound good to me)
  I'm lost here because I don't really know the ramifications of this idea of having QVars instead of the Unifs that were generated.
• Something else entirely?

For sections I'm open to discussion, but I'm still quite convinced that allowing unification of section-local sorts is a bad idea.

Why do you think it's bad ?

[SkySkimmer]

Maybe we could have version of the PR where section variables do not support elaborating qualities (error not yet implemented if there are non empty implicit qualities / elim constraints to add to the section context), then I think it would be mergeable and we can think about sections separately.