Do not rely on floating universes in the upper layers #18956
Conversation
ppedrot
added
kind: cleanup
coqbot-app
bot
removed
the
request: full CI
| @@ -491,11 +492,12 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~variances ~ctx_param | |||
| constructors | |||
| in | |||
| let sigma, (default_dep_elim, arities) = inductive_levels env_ar_params sigma arities ctor_args in | |||
| let sigma = Evd.minimize_universes sigma in | |||
| let lbound = if poly then UGraph.Bound.Set else UGraph.Bound.Prop in | |||
| let sigma = Evd.minimize_universes ~lbound sigma in | |||
There was a problem hiding this comment.
Having to to this is IMO an indication that we're not doing the right thing.
If we naively always pass Set a problem appears with
Inductive T A := C : A -> T nat -> T A.(a version with option A instead of nat appears in the test suite)
before minimization we have generated T : Type@{Type|u} -> Type@{q|v} with Set <= u, u <= v
(Set <= u from the application T nat, u <= v from include_constructor_argument)
Minimization collapses q := Type and sets u = v, with lbound Set it also forgets Set <= u. We then think the inductive can be template and the kernel will reject it.
Probably we need to
- in
include_constructor_argumentin monomorphic mode do not ignore qualities, such thatSet <= Type@{q|u}producesq := Typeinstead of leaving it floating, this would make the example generateq := Type. (include_constructor_argumentcurrently has a comment that ignoring qualities only impacts squashing but that's not correct once we use sort qualities in monomorphic mode) - when determining if an inductive may be template, the parameters binding a universe must be at floating (possibly above_prop) quality (this is an interpretation of unbounded_from_below now that we can't check the presence of
Set <= uconstraints) - to be able to do this check we need to delay sort quality collapse (currently done in minimize_universes)
then we should be able to forget Set <= u constraints in minimization ie always use lbound = Set (and the lbound concept can then be deleted since this is the last user)
Should be backwards compatible and future-proof.
Should be backwards compatible and future-proof.
|
The CoqHammer backwards compatible overlay has been merged, this is ready to go. |
|
@coqbot run full ci |
|
I don't see how you can do it without hacking the lbound at some point, though. |
|
You have to actually use the sort qualities instead of the current state of the PR which AFAICT uses them possibly by accident to make automatic Prop lowering work and then collapses them. |
|
I definitely want to refine the criterion to rely on sort qualities in the future, but this is a quick (and dirty) cleanup that ensures that nobody can rely on the lbound hack anymore, because it's just not part of the data structures anymore. If there is time for 8.20 then I can try to come up with the refinement asap, but I thought that the current state was already a net progress. |
I don't agree. |
github-actions
bot
added
the
needs: rebase
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
template-no-lower-bound
branch
from
9998efd
to
446d4e5
Compare
coqbot-app
bot
removed
needs: rebase
ppedrot
added
the
request: full CI
This is not used yet, but it will allow preserving the behaviour where Type in a template polymorphic inductive type means Type or Prop.
This removes the lbound parameter from the universe unification state, but we still have to handle universe minimization of inductive types in a special way.
We introduce a specific function to push the template universes in the environment context rather than modifying this globally. We should do this in a more principled way but I will leave this to further enhancement.
ppedrot
force-pushed
the
template-no-lower-bound
branch
from
446d4e5
to
8c2745f
Compare
coqbot-app
bot
removed
the
request: full CI
|
@coqbot merge now |
We remove the lower universe bound from the UState and environment data types, and rely instead on passing a flag to the pretyper to generate sort-polymorphic universes. The kernel still requires pushing floating template universes, but I will defer this cleanup to a later PR.