a19ff61e15
This PR adds support for `structure` in `mutual` blocks, allowing inductive types defined by `inductive` and `structure` to be mutually recursive. The limitations are (1) that the parents in the `extends` clause must be defined before the `mutual` block and (2) mutually recursive classes are not allowed (a limitation shared by `class inductive`). There are also improvements to universe level inference for inductive types and structures. Breaking change: structure parents now elaborate with the structure in scope (fix: use qualified names or rename the structure to avoid shadowing), and structure parents no longer elaborate with autoimplicits enabled. Internally, this is a large refactor of both the `inductive` and `structure` commands. Common material is now in `Lean.Elab.MutualInductive`, and each command plugs into this mutual inductive elaboration framework with the logic specific to the respective command. For example, `structure` has code to add projections after the inductive types are added to the environment. Closes #4182
30 lines
3.1 KiB
Text
30 lines
3.1 KiB
Text
univInference.lean:25:48-25:54: error: resulting type is of the form
|
|
Type ?u
|
|
but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using
|
|
Sort (max (max 1 u) v)
|
|
if the resulting universe level should be at the above universe level or higher.
|
|
|
|
Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form '?u+1'. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s):
|
|
u ≤ ?u+1
|
|
v ≤ ?u+1
|
|
However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary.
|
|
S6 : Sort (max w₁ w₂) → Type w₂ → Sort (max w₁ (w₂ + 1))
|
|
univInference.lean:45:48-45:62: error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:
|
|
Sort (max u v)
|
|
Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.
|
|
univInference.lean:64:48-64:54: error: resulting type is of the form
|
|
Type ?u
|
|
but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using
|
|
Sort (max (max 1 u) v)
|
|
if the resulting universe level should be at the above universe level or higher.
|
|
|
|
Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form '?u+1'. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s):
|
|
u ≤ ?u+1
|
|
v ≤ ?u+1
|
|
However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form 'Sort (_ + 1)' and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary.
|
|
univInference.lean:73:48-73:62: error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:
|
|
Sort (max u v)
|
|
Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.
|
|
univInference.lean:81:48-81:62: error: invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:
|
|
Sort (max u v)
|
|
Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.
|