Better error about uninstantiated universe variables

Stream: lean4

[Jakub Nowak]

The error message is unhelpful. The fix is to explicitly provide universe variable for Ordinal. Either by using Ordinal.{0} in definition of Foo.ordinalLevel, or Foo.ordinalLevel.{0} at call site. Is it possible to have a better error message in this case?

import Mathlib.SetTheory.Ordinal.Basic
import Mathlib.SetTheory.Ordinal.Family

inductive Foo (α : Type) : Type where
| base (k : Nat) : Foo α
| foo (f : α → Foo α) : Foo α

@[simp]
noncomputable def Foo.ordinalLevel : Foo α → Ordinal
| base k => k
| foo f => ⨆ a, (f a).ordinalLevel + 1

/--
error: (kernel) declaration has metavariables 'Foo.sum'
---
error: (kernel) application type mismatch
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
argument has type
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
but function has type
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-/
#guard_msgs in
def Foo.sum [Inhabited α] : Foo α → Nat
| base k => k
| foo f => Foo.sum (f default)
termination_by foo => Foo.ordinalLevel foo
decreasing_by
  simp_wf
  calc (f default).ordinalLevel
    _ < (f default).ordinalLevel + 1 := Order.lt_succ _
    _ ≤ ⨆ a, (f a).ordinalLevel + 1 := Ordinal.le_iSup ..

[Aaron Liu]

does the termination checker not also check for universe mvars

[Jakub Nowak]

Was that a question? I don't know the answer, because I didn't understood the question. In what way universe mvars have to be checked?

[Aaron Liu]

I think this is probably the reason for why you get such an error, is that the termination checker does not process unassigned universe metavariables

[Jakub Nowak]

You think it should automatically default universe mvars that were left unsolved, to lowest possible?

[Jakub Nowak]

Is there an example of Lean doing this in some other context?

[Aaron Liu]

I think it should throw an error actually

[Aaron Liu]

but with a better error message of course

[Jakub Nowak]

Defaulting universe variables to lowest possible makes sense I think? I don't think setting universe variables lower can change solvable goal to unsolvable one? In worst case proof might require some ULift's.

[Aaron Liu]

it's done for definitions, for obvious reasons

[Aaron Liu]

and it's done for proofs because proofs are handled the same as definitions

[Jakub Nowak]

I think for definitions the unsolved universe variables are put as universe variables of the definition?

[Aaron Liu]

...right

[Aaron Liu]

yeah

[Jakub Nowak]

But I don't think it would make sense to put universe variables there are only used in the termination proof as part of the definition.

[Aaron Liu]

how does this work again?

[Aaron Liu]

no wait that's not right

[Aaron Liu]

wait no

[Jakub Nowak]

Jakub Nowak said:

I don't think setting universe variables lower can change solvable goal to unsolvable one?

Hmm, or maybe it actually could make a goal unsolvable? Because there's a significant difference between Sort 0 and Sort 1.

[Aaron Liu]

I remember there was a behavior where if the universe is mentioned but it isn't used anywhere then it throws an error

[Aaron Liu]

but that's not about metavariables

[Aaron Liu]

and there is also the behavior that if in a theorem you leave a universe metavariable then it throws an error

[Aaron Liu]

Jakub Nowak said:

Defaulting universe variables to lowest possible makes sense I think? I don't think setting universe variables lower can change solvable goal to unsolvable one? In worst case proof might require some ULift's.

as an example take docs#UCompactlyGeneratedSpace

[Jakub Nowak]

Jakub Nowak said:

I think for definitions the unsolved universe variables are put as universe variables of the definition?

Like, in the case of Foo.universeLevel Lean made this signature: def Foo.ordinalLevel.{u_1} : {α : Type} → Foo α → Ordinal.{u_1}. So it took the universe mvar that came from Ordinal and put it as a universe variable of the Foo.ordinalLevel.

[Aaron Liu]

but you mentioned it in the statement so that's a bit different

[Aaron Liu]

I think it also lifts it out if you mention it in the body of a definition?

[Aaron Liu]

but not the body of a proof...

[Jakub Nowak]

Jakub Nowak said:

Is there an example of Lean doing this in some other context?

Not exactly the same, but I can write

inductive Foo where
| mk (o : Ordinal.{3})

and Lean will pick Foo : Type 4, even though it could do Foo : Type (max u 4).
So in this case Lean automatically picks the lowest.
And, if I write

inductive Foo where
| nil

then it will pick Foo : Sort 1, not Foo : Sort 0. So, in this case it doesn't pick lowest possible, but it picks lowest possible that doesn't introduce Prop.
Maybe similar behaviour would make sense for automatically instantiating universe variables in proofs?

[Aaron Liu]

that's inductive types

[Aaron Liu]

I feel like that's different

[Jakub Nowak]

That is different.

[Kyle Miller]

inductive has a heuristic that if it's got only one-constructor, and that constructor has at least one field, and all fields are propositions, then it will chose Prop. That's because in this case it's a syntactic subsingleton and the kernel will generate a recursor that can eliminate into any universe. Plus, empirically people want an inductive predicate in this case (at least for structure).

inductive Foo (a : Nat) where
| nil (h : a = 1)
#check Foo -- Foo (a : Nat) : Prop

Otherwise it goes for Type _.

The inductive command doesn't have (good) heuristics for universe level metavariables inside constructors. Currently it does different things depending on whether or not the universe for the inductive was provided. It can also do some crazy things like

inductive Foo : Type where
| nil {α} (x : α)
#check Foo.nil -- Foo.nil {α : Prop} (x : α) : Foo

(It reasons "well, the only level that works here is 0, so go with that". I think this feature is my fault, probably from lean4#6125.)

[Kyle Miller]

I've got your first message starred by the way, since it's a bug if the error is being reported from the kernel. The elaborator is responsible for reporting metavariable errors and localizing them in the source code.

[Kyle Miller]

By the way, the elaborator does assign level metavariables to 0 when it reports errors, as an error-recovery mechanism.

It seems plausible that inside theorems, the elaborator could simply set them to 0 and not report anything — there shouldn't be any Prop/Type _ issues, since the elaborator checks whether levels can/can't be zero as it elaborates. My primary concern is that if a proof has metavariables then it might be brittle.