Introduce PolyFlags to gather flags for polymorphic defs

[mattam82]

Adapt the whole code base to use this instead of the multiple poly/"sort_poly"/cumulative flags. Actually the sort_poly flag is renamed collapse_sort_variables as it is the only thing it will govern. We use PolyFlags.univ_poly to check for universe polymorphism (= sort and level polymorphism).

Consistently name the argument ~poly:PolyFlags.t. Also adds an attribute poly : PolyFlags.construction_kind -> PolyFlags.t attribute that decides depending on the construction (assumption, definition or inductive) which flags are supported and how they should be set. Subsequent PRs will add new options for cumulativity of assumptions and definitions (in this PR they are still unsupported as before), and will use collapse_sort_variables to govern implicit sort polymorphism (do metavariable sorts default to Type (the current default) or not).

These flags are not used in all places they are passed yet, but will be in the upcoming PRs around sort-elim/univ-poly/variances and cumulativity. The goal is just to do a functionality-preserving API change here, that should reduce conflicts down the road for these feature PRs, with this one requiring simple overlays.

In particular this is a prerequisite for @TDiazT 's subsequent PRs on adding sort elaboration.

• Added changelog.

• Opened overlay pull requests.
  • Adapt to rocq-prover/rocq#21419 mit-plv/rewriter#188
  • Adapt to rocq-prover/rocq#21419 Lysxia/coq-simple-io#87
  • Adapt to rocq-prover/rocq#21419 impermeable/coq-waterproof#224
  • Adapt to rocq-prover/rocq#21419 Mtac2/Mtac2#419
  • Adapt to rocq-prover/rocq#21419 rocq-community/paramcoq#148
  • Adapt to rocq-prover/rocq#21419 smtcoq/smtcoq#159
  • https://gitlab.inria.fr/fbesson/itauto/-/merge_requests/20
  • Adapt to Rocq PR#21419 mattam82/Coq-Equations#682
  • Adapt to rocq-prover/rocq#21419 LPCIC/coq-elpi#942
  • Adapt to rocq-prover/rocq#21419 MetaRocq/metarocq#1224
  • Adapt to rocq-prover/rocq#21419 QuickChick/QuickChick#421

[yannl35133]

General comments:

• Is the future umbrella term not going to be Universe Polymorphism? I believe the structure should be called UnivPolyFlags rather than SortPolyFlags
• There are a few SortPolyFlags.of_poly and a fewSortPolyFlags.make ~level_polymorphic:poly ~sort_polymorphic:false ~cumulative:false, why such a difference ?

[mattam82]

General comments:

• Is the future umbrella term not going to be Universe Polymorphism? I believe the structure should be called UnivPolyFlags rather than SortPolyFlags

I would also like to explain it like this: A universe is a sort and an optional universe level Prop|SProp|Set|Type@u|Global@{s;u}|Local@{s;u}) The we consistently use sort polymorphism, universe level polymorphism and universe polymorphism is their union. Does everyone agree?

• There are a few SortPolyFlags.of_poly and a fewSortPolyFlags.make ~level_polymorphic:poly ~sort_polymorphic:false ~cumulative:false, why such a difference ?

They should all be UnivPolyFlags.of_level_poly indeed, I just introduced the abbreviation too late ;)

[ppedrot]

universe level polymorphism

Just say "level polymorphism".

[mattam82]

Thanks for the feedback. So I will correct the little mistakes here and there and:

• have the type defined in engine/polyFlags.ml{,i}
• make it private to not redefine the projections
• is_polymorphic -> is_level_polymorphic
• of_poly -> of_level_poly (most should have a FIXME comment here, it means something probably does not yet support sort_poly/cumulativity when it should)

Please +1 this message or state your disagreement :)

[ppedrot]

have the type defined in engine/polyFlags.ml{,i}

Why not as an abstract type in UState? I'm still not a fan of having to write PolyFlag.t.

[yannl35133]

is_polymorphic -> is_level_polymorphic

Either you remove the alias or you consider it as more than an alias and you properly document the fact.
I tend to prefer the latter, considering the use cases.

[SkySkimmer]

What are the flags when doing Polymorphic Definition id@{s;u} (A:Type@{s;u}) (a:A) := a. ?
If it's level_poly = true, sort_poly = false then that seems wrong since we are sort polymorphic
If they're both true then what's the difference between level_poly and sort_poly?

[mattam82]

have the type defined in engine/polyFlags.ml{,i}

Why not as an abstract type in UState? I'm still not a fan of having to write PolyFlag.t.

You prefer to write UState.poly_flags then? And then the projections as UState.level_polymorphic poly? I'm fine with that too, even if I would prefer to qualify as PolyFlags.level_polymorphic

[mattam82]

@SkySkimmer just a PolyFlags.pr : t -> Pp.t would satisfy you ?

[mattam82]

@SkySkimmer Also, any idea about the artifact errors on the CI?

[SkySkimmer]

@SkySkimmer just a PolyFlags.pr : t -> Pp.t would satisfy you ?

and the stuff in top_printers.ml / top_printers.dbg to get it automatically in ocamldebug

[SkySkimmer]

@SkySkimmer Also, any idea about the artifact errors on the CI?

no

[mattam82]

I added the debug printer stuff now

[mattam82]

I don't think this needs another full ci

[ppedrot]

@coqbot run full ci

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 21419-mattam82-sort-poly-flags.sh