309f44d007
This PR improves universe level inference for the `inductive` and `structure` commands to be more reliable and to produce better error messages. Recall that the main constraint for inductive types is that if `u` is the universe level for the type and `u > 0`, then each constructor field's universe level `v` satisfies `v ≤ u`, where a *constructor field* is an argument that is not one of the type's *parameters* (recall: the type's parameters are a prefix of the parameters shared by the type former and all the constructors). Given this constraint, the `inductive` elaborator attempts to find reasonable assignments to metavariables that may be present: - For the universe level `u`, choosing an assignment that makes this level least is reasonable, provided it is unique. - For constructor fields, choosing the unique assignment is usually reasonable. - For the type's parameters, promoting level metavariables to new universe level parameters is reasonable. The order of these steps led to somewhat convoluted error messages; for example, metavariable->parameter promotion was done early, leading to errors mentioning `u_1`, `u_2`, etc. instead of metavariables, as well as extraneous level constraint errors. Furthermore, early parameter promotion meant it was too late to perform certain kinds of inferences. Now there is a straightforward order of inference: 1. If the type's universe level could be zero, it checks that the type is an "obvious `Prop` candidate", which means it's non-recursive, has one constructor with at least one field, and all the fields are proofs. If it's a `Prop` candidate, the level is set to zero and we skip to step 4. 2. If the type's simplified universe level is of the form `?u + k`, it will accumulate level constraints to find a least upper bound solution for `?u`. To avoid sort polymorphism, it adds `1 ≤ ?u + k`, ensuring the result stays in `Type _`, or at least `Sort (max 1 _)`. It allows other metavariables to appear in the assignment for `?u`, provided they appear in the type former, or for `structure` in the `extends` clause. 3. If the type's simplified universe level is then of the form `r + k`, where `r` is a parameter, metavariable, or zero, then for every constructor field it will take the `v ≤ r + k` constraint and extract `?v ≤ r + k'` constraints. It will also *weakly* extract `1 ≤ ?v` constraints, using the observation that it's surprising if fields are automatically inferred to be proofs. Once the constraints are collected, each metavariable is solved for independently. Heuristically, if there is a unique non-constant solution we take that, or else a unique constant solution. 4. Any remaining level metavariables in the type former (or `extends` clause) become level parameters. 5. Remaining level metavariables in the constructor fields are reported as errors. 6. Then, the elaborator checks that the level constraints actually hold and reports an error if they don't. In 2 and 3, there are procedures to simplify universe levels. You can write `Sort (max 1 _)` for the resulting type now and it will solve for `_`. The "accidentally higher universe" error is now a warning. The constraint solving is also done in a more careful way, which keeps it from being reported erroneously. There are still some erroneous reports, but these ones are hard for the checker to reject. As before, the warning can be turned off by giving an explicit universe. Note about `extends` clauses: in testing, there were examples where it was surprising if the universe polymorphism of parent structures didn't carry over to the type being defined, even though parent structures are actually constructor fields. **Breaking change.** Universe level metavariables present only in constructor fields are no longer promoted to be universe level parameters: use explicit universe level parameters. This promotion was inconsistently done depending on whether the inductive type's universe level had a metavariable, and also it caused confusion for users, since these universe levels are not constrained by the type former's parameters. **Breaking change.** Now recursive types do not count as "obvious `Prop` candidates". Use an explicit `Prop` type former annotation on recursive inductive predicates. Additional changes: - level metavariable errors are now localized to constructors, and `structure` fields have such errors localized to fields - adds module docs for the index promotion algorithm and the universe level inference algorithm for inductives - factors out `Lean.Elab.Term.forEachExprWithExposedLevelMVars` for printing out the context of an expression with universe level metavariables - makes universe level metavariable exposure more effective at exposing level metavariables (with an exception of `sorry` terms, which are too noisy to expose) Supersedes #11513 and #11524.
10 lines
238 B
Text
10 lines
238 B
Text
/-!
|
||
# Verify that `below` lemmas work in cases where they may need to δ-reduce things
|
||
Fixes issue #2990
|
||
-/
|
||
|
||
def Foo (F : α -> Prop) : Prop :=
|
||
∀ x , F x
|
||
|
||
inductive Bad : Nat -> Prop :=
|
||
| bar e : Foo (fun _ : Nat => Bad e) -> Bad e
|