8f1c18d9f4
This PR improves pretty printing of level metavariables: they now print with a per-definition index rather than their per-module internal identifiers. Furthermore, `+` is printed uniformly in level expressions with surrounding spaces. **Breaking metaprogramming change:** level pretty printing should use `delabLevel` or `MessageData.ofLevel`; functions such as `format` or `toString` do not have access to the indices, since they are stored in the current metacontext. Absent index information, metavariables print with the raw internal identifier as `?_mvar.nnn`. **Note:** The heartbeat counter also increases quicker due to counting allocations that record level metavariable indices. In some tests we needed to increase `maxHeartbeats` by 20–50% to compensate, without a corresponding slowdown.
384 lines
11 KiB
Text
384 lines
11 KiB
Text
/-!
|
||
# Tests of universe constraint testing in the `inductive` command
|
||
-/
|
||
|
||
set_option pp.mvars false
|
||
set_option pp.universes true
|
||
|
||
/-!
|
||
Infers the resulting universe `Sort ?u`.
|
||
Here, `x : Nat : Type`, so `1 ≤ ?u` gives `Type` as least universe.
|
||
-/
|
||
inductive ExResultUni1 where
|
||
| mk (x : Nat)
|
||
/--
|
||
info: inductive ExResultUni1 : Type
|
||
number of parameters: 0
|
||
constructors:
|
||
ExResultUni1.mk : Nat → ExResultUni1
|
||
-/
|
||
#guard_msgs in #print ExResultUni1
|
||
|
||
/-!
|
||
Infers the resulting universe `Sort ?u`.
|
||
Here, `x : α : Sort v`, so `v ≤ ?u` and the additional `1 ≤ ?u` gives `Sort (max 1 v)`.
|
||
-/
|
||
inductive ExResultUni2 (α : Sort v) where
|
||
| mk (x : α)
|
||
/--
|
||
info: inductive ExResultUni2.{v} : Sort v → Sort (max 1 v)
|
||
number of parameters: 1
|
||
constructors:
|
||
ExResultUni2.mk : {α : Sort v} → α → ExResultUni2.{v} α
|
||
-/
|
||
#guard_msgs in #print ExResultUni2
|
||
|
||
/-!
|
||
Infers the resulting universe `Sort ?u`.
|
||
Here, `x : α : Type v`, so `v + 1 ≤ ?u`. The `1 ≤ ?u` isn't necessary. Get `Type v`.
|
||
-/
|
||
inductive ExResultUni3 (α : Type v) where
|
||
| mk (x : α)
|
||
/--
|
||
info: inductive ExResultUni3.{v} : Type v → Type v
|
||
number of parameters: 1
|
||
constructors:
|
||
ExResultUni3.mk : {α : Type v} → α → ExResultUni3.{v} α
|
||
-/
|
||
#guard_msgs in #print ExResultUni3
|
||
|
||
/-!
|
||
Infers the resulting universe `Sort ?u`.
|
||
Even though this *could* be a syntactic subsingleton with `?u = 0`, it is recursive so, heuristically,
|
||
we don't use that solution.
|
||
From `x : α : Sort v` and `y : ExResultUni4 α : Sort ?u` we get `v ≤ ?u` and `?u ≤ ?u`.
|
||
With the additional `1 ≤ ?u`, we get `Sort (max 1 v)
|
||
-/
|
||
inductive ExResultUni4 (α : Sort v) where
|
||
| mk (x : α) (y : ExResultUni4 α)
|
||
/--
|
||
info: inductive ExResultUni4.{v} : Sort v → Sort (max 1 v)
|
||
number of parameters: 1
|
||
constructors:
|
||
ExResultUni4.mk : {α : Sort v} → α → ExResultUni4.{v} α → ExResultUni4.{v} α
|
||
-/
|
||
#guard_msgs in #print ExResultUni4
|
||
|
||
/-!
|
||
An "unnecessarily high" universe warning. (Though erroneous!)
|
||
The use of `List` causes the resulting universe to be `Type ?u`.
|
||
From `x : α : Sort v` we get `v ≤ ?u + 1`, and from `y : List (ExResultUni5 α) : Type ?u` we get `?u ≤ ?u`.
|
||
There's a potential universe bump here, since ideally we would create `Type (v - 1)` as the level,
|
||
if there were such a thing as level subtraction, but instead the only solution is `Type v`.
|
||
|
||
Unfortunately, this check does not realize that `List (ExResultUni5 α)` forces `Type v`.
|
||
It's a warning, and it can be silenced with an explicit universe level.
|
||
-/
|
||
/--
|
||
warning: Inferred universe level for type may be unnecessarily high. The inferred resulting universe is
|
||
Type v
|
||
but it possibly could be
|
||
Sort (max 1 v)
|
||
Explicitly providing a resulting universe with no metavariables will silence this warning.
|
||
|
||
Note: The elaborated resulting universe after constructor elaboration is
|
||
Type _
|
||
The inference algorithm attempts to compute the smallest level for `_` such that all universe constraints for all constructor fields are satisfied, with some approximations. The following derived constraint(s) are the cause of this possible unnecessarily high universe:
|
||
v ≤ _ + 1
|
||
For example, if the resulting universe is of the form `Sort (?r + 1)` and a constructor field is in universe `Sort u`, the constraint `u ≤ ?r + 1` leads to the unnecessarily high resulting universe `Sort (u + 1)`. Using `Sort (max 1 u)` avoids this universe bump, if using it is possible.
|
||
-/
|
||
#guard_msgs in
|
||
inductive ExResultUni5 (α : Sort v) where
|
||
| mk (x : α) (y : List (ExResultUni5 α))
|
||
-- Silenced:
|
||
#guard_msgs in
|
||
inductive ExResultUni5' (α : Sort v) : Type v where
|
||
| mk (x : α) (y : List (ExResultUni5' α))
|
||
|
||
/--
|
||
Inference can handle `Sort (max _ 1)` as the resulting universe.
|
||
-/
|
||
inductive ExResultUni6 (α : Sort v) (β : Sort w) : Sort (max _ 1) where
|
||
| mk (x : α) (y : β)
|
||
/-- info: ExResultUni6.{v, w} (α : Sort v) (β : Sort w) : Sort (max (max v w) 1) -/
|
||
#guard_msgs in #check ExResultUni6
|
||
|
||
/--
|
||
Inference can also handle parameters already existing in the resulting universe.
|
||
-/
|
||
inductive ExResultUni7 (α : Sort v) : Sort (max v _) where
|
||
| mk (x : α)-- (n : Nat)
|
||
/-- info: ExResultUni7.{v} (α : Sort v) : Sort (max v 1) -/
|
||
#guard_msgs in #check ExResultUni7
|
||
|
||
/--
|
||
The universe of `α` is inferrable here, since it's known to be a `Type _` (from
|
||
the use of `List`), and inference will use level constraints to assign level metavariables
|
||
if they imply a unique solution, ignoring constant solutions if there's a non-constant solution.
|
||
-/
|
||
inductive ExParamUni1 (x : α) : Type v where
|
||
| mk (ys : List α) (h : [x] = ys)
|
||
/--
|
||
info: inductive ExParamUni1.{v} : {α : Type v} → α → Type v
|
||
number of parameters: 2
|
||
constructors:
|
||
ExParamUni1.mk : {α : Type v} →
|
||
{x : α} → (ys : List.{v} α) → Eq.{v + 1} (List.cons.{v} x List.nil.{v}) ys → ExParamUni1.{v} x
|
||
-/
|
||
#guard_msgs in #print ExParamUni1
|
||
|
||
/-!
|
||
Uses `Type v` for `α` and `β`, since these are the unique non-constant solutions.
|
||
-/
|
||
inductive ExParamUni2 {α β : Type _} (x : α) (y : β) : Type v where
|
||
| mk (fs : List (α → β))
|
||
/--
|
||
info: inductive ExParamUni2.{v} : {α β : Type v} → α → β → Type v
|
||
number of parameters: 4
|
||
constructors:
|
||
ExParamUni2.mk : {α β : Type v} → {x : α} → {y : β} → List.{v} (α → β) → ExParamUni2.{v} x y
|
||
-/
|
||
#guard_msgs in #print ExParamUni2
|
||
|
||
/-!
|
||
The resulting type after resulting type inference is `Type ?u`, with a metavariable.
|
||
Constructor field universe propagation treats this metavariable as a parameter,
|
||
inferring `PUnit : Type ?u`.
|
||
-/
|
||
inductive ExParamUni3 {α : Type _} where
|
||
| mk (x : α) (a : PUnit) -- use Unit if it should be in `Type 0`
|
||
/--
|
||
info: inductive ExParamUni3.{u_1} : {α : Type u_1} → Type u_1
|
||
number of parameters: 1
|
||
constructors:
|
||
ExParamUni3.mk : {α : Type u_1} → α → PUnit.{u_1 + 1} → ExParamUni3.{u_1}
|
||
-/
|
||
#guard_msgs in #print ExParamUni3
|
||
|
||
/-!
|
||
Given the resultant type, infer that the `x` parameter is `Type`.
|
||
-/
|
||
inductive T0 : Type where
|
||
| mk (x : PUnit.{_+1})
|
||
/-- info: T0.mk (x : PUnit.{1}) : T0 -/
|
||
#guard_msgs in #check T0.mk
|
||
|
||
/-!
|
||
Given the resultant type, infer that the `x` parameter is `Type` as well.
|
||
-/
|
||
inductive T1 : Type where
|
||
| mk (x : PUnit.{_+1} × PUnit.{_+1})
|
||
/-- info: T1.mk (x : Prod.{0, 0} PUnit.{1} PUnit.{1}) : T1 -/
|
||
#guard_msgs in #check T1.mk
|
||
|
||
/-!
|
||
Given the resultant type is `Prop`, do not do this inference.
|
||
-/
|
||
/--
|
||
error: Failed to infer universe levels in type of binder `x`
|
||
Prod.{_, _} PUnit.{_ + 1} PUnit.{_ + 1}
|
||
-/
|
||
#guard_msgs in
|
||
inductive T3 : Prop where
|
||
| mk (x : PUnit.{_+1} × PUnit.{_+1})
|
||
|
||
/-!
|
||
Given the resultant type, fail to infer a level for `PUnit` if there's not a unique solution.
|
||
-/
|
||
/--
|
||
error: Failed to infer universe levels in type of binder `x`
|
||
PUnit.{_}
|
||
-/
|
||
#guard_msgs in
|
||
inductive E0 : Type 1 where
|
||
| mk (x : PUnit)
|
||
|
||
/-!
|
||
Inference goes for `Type _` fields, so this succeeds.
|
||
-/
|
||
inductive E0' : Type where
|
||
| mk (x : PUnit)
|
||
|
||
/-!
|
||
Given the resultant type, fail to infer a level for `PUnit` if there's not a unique solution.
|
||
-/
|
||
/--
|
||
error: Failed to infer universe levels in type of binder `x`
|
||
Prod.{_, _} PUnit.{_ + 1} PUnit.{_ + 1}
|
||
-/
|
||
#guard_msgs in
|
||
inductive E1 : Type 1 where
|
||
| mk (x : PUnit × PUnit)
|
||
|
||
/-!
|
||
Even though `α : Prop` is the unique solution, reject it for being unintuitive.
|
||
-/
|
||
/--
|
||
error: Failed to infer universe levels in type of binder `α`
|
||
Sort _
|
||
-/
|
||
#guard_msgs in
|
||
inductive E2 : Type where
|
||
| mk {α} (x : α)
|
||
|
||
/-!
|
||
`Sort` polymorphism is not allowed.
|
||
-/
|
||
/--
|
||
error: Invalid universe polymorphic resulting type: The resulting universe is not `Prop`, but it may be `Prop` for some parameter values:
|
||
Sort u
|
||
|
||
Hint: A possible solution is to use levels of the form `max 1 _` or `_ + 1` to ensure the universe is of the form `Type _`
|
||
-/
|
||
#guard_msgs in
|
||
inductive P (α : Sort u) : Sort u where
|
||
| mk (x : α)
|
||
|
||
/-!
|
||
Errors for `structure` are specialized to talking about fields.
|
||
-/
|
||
/--
|
||
error: Invalid universe level for field `α`: Field has type
|
||
Type
|
||
at universe level
|
||
2
|
||
which is not less than or equal to the structure's resulting universe level
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
structure A : Type where
|
||
α : Type
|
||
|
||
/-!
|
||
Errors for `structure` talk about parent projection fields too.
|
||
(Note: it could easily point to `A'` and say the error is field `α`.)
|
||
-/
|
||
structure A' where
|
||
α : Type
|
||
/--
|
||
error: Invalid universe level for field `α`: Field has type
|
||
Type
|
||
at universe level
|
||
2
|
||
which is not less than or equal to the structure's resulting universe level
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
structure B : Type extends A'
|
||
|
||
/-!
|
||
Basic test of resulting type for recursive type.
|
||
Least universe is `Type`.
|
||
-/
|
||
inductive Bar3
|
||
| foobar {Foo : Prop} : Foo → Bar3
|
||
| somelist : List Bar3 → Bar3
|
||
/-- info: Bar3 : Type -/
|
||
#guard_msgs in #check Bar3
|
||
|
||
/-!
|
||
Test of resulting type for recursive type.
|
||
Least universe here is `Type 1`.
|
||
-/
|
||
inductive Bar4
|
||
| foobar {Foo : Type} : Foo → Bar4
|
||
| somelist : List Bar4 → Bar4
|
||
/-- info: Bar4 : Type 1 -/
|
||
#guard_msgs in #check Bar4
|
||
|
||
/-!
|
||
Like `Bar4`, but this time infers the type of the `Foo` field as `Type`.
|
||
-/
|
||
inductive Bar4' : Type 1
|
||
| foobar {Foo} : Foo → Bar4'
|
||
| somelist : List Bar4' → Bar4'
|
||
/-- info: Bar4' : Type 1 -/
|
||
#guard_msgs in #check Bar4'
|
||
/-- info: Bar4'.foobar {Foo : Type} : Foo → Bar4' -/
|
||
#guard_msgs in #check Bar4'.foobar
|
||
|
||
/-!
|
||
Type error at `List Bar5`, stops elaboration.
|
||
-/
|
||
/--
|
||
error: Application type mismatch: The argument
|
||
Bar5
|
||
has type
|
||
Prop
|
||
of sort `Type` but is expected to have type
|
||
Type _
|
||
of sort `Type (_ + 1)` in the application
|
||
List.{_} Bar5
|
||
-/
|
||
#guard_msgs in
|
||
inductive Bar5 : Prop where
|
||
| foobar {Foo : Prop} : Foo → Bar5
|
||
| somelist : List Bar5 → Bar5
|
||
|
||
/-!
|
||
Type error on `foobar` constructor. Resulting universe is too small.
|
||
-/
|
||
/--
|
||
error: Invalid universe level in constructor `Bar6.foobar`: Parameter `Foo` has type
|
||
Type
|
||
at universe level
|
||
2
|
||
which is not less than or equal to the inductive type's resulting universe level
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
inductive Bar6 : Type where
|
||
| foobar {Foo : Type} : Foo → Bar6
|
||
| somelist : List Bar6 → Bar6
|
||
|
||
/-!
|
||
With `Foo : Prop`, the `Bar6` example would be ok.
|
||
-/
|
||
inductive Bar7 : Type where
|
||
| foobar {Foo : Prop} : Foo → Bar7
|
||
| somelist : List Bar7 → Bar7
|
||
|
||
/-!
|
||
While `Foo : Sort ?u` gives the constraint `?u + 1 ≤ 1`, which has `?u = 0` as the
|
||
unique solution, the `x : Foo : Sort ?u` gives the additional constraint `1 ≤ ?u`,
|
||
so it doesn't assign `?u = 0`.
|
||
-/
|
||
/--
|
||
error: Constructor field `Foo` of `Bar8.foobar` contains universe level metavariables at the expression
|
||
Sort _
|
||
in its type
|
||
Sort _
|
||
-/
|
||
#guard_msgs in
|
||
inductive Bar8 : Type where
|
||
| foobar : (x : Foo) → Bar8
|
||
| somelist : List Bar8 → Bar8
|
||
|
||
/-!
|
||
This gives `Foo : Type u`. This comes from `Foo : Sort ?u : Sort (?u + 1)`, so `?u + 1 ≤ u + 2`
|
||
has two non-constant solutions: `?u = u` and `?u = u + 1`.
|
||
Additionally, `x : Foo : Sort ?u` gives `1 ≤ ?u` since it's a field. This excludes `?u = u` since
|
||
`1 ≤ u` isn't always true.
|
||
Therefore it chooses `?u = u + 1`.
|
||
-/
|
||
inductive Bar9 : Type (u + 1) where
|
||
| foobar : (x : Foo) → Bar9
|
||
| somelist : List Bar9 → Bar9
|
||
/-- info: Bar9.foobar.{u} {Foo : Type u} (x : Foo) : Bar9.{u} -/
|
||
#guard_msgs in #check Bar9.foobar
|
||
|
||
/-!
|
||
Can infer imax field, constant resulting type.
|
||
-/
|
||
inductive Bar10 : Type 1 where
|
||
| mk (f : α → β)
|
||
/-- info: Bar10.mk {α β : Type} (f : α → β) : Bar10 -/
|
||
#guard_msgs in #check Bar10.mk
|
||
|
||
/-!
|
||
Can infer imax field, non-constant resulting type.
|
||
-/
|
||
inductive Bar11 : Type (u + 1) where
|
||
| mk (f : α → β)
|
||
/-- info: Bar11.mk.{u} {α β : Type u} (f : α → β) : Bar11.{u} -/
|
||
#guard_msgs in #check Bar11.mk
|