Universe Vars

Stream: general

[Marcus Rossel]

It seems I don't understand universe variables (universe parameters?) correctly. In the following example, everything works as expected:

variable (h : ∀ (α : Type _), True)

example : True := h Nat

Here, h has type Type ?u.3477 → True -- that is, the universe level is a level mvar.
Now if I try to replace the _ with a universe variable, things don't work:

universe u
variable (h : ∀ (α : Type u), True)

example : True := h Nat
--                  ^^^
/-
application type mismatch
  h Nat
argument
  Nat
has type
  Type : Type 1
but is expected to have type
  Type u : Type (u + 1)
-/

Here, h has type Type u → True. I don't understand what that's supposed to mean, because I thought universe variables like u only made sense wrt. to a definition.

[Riccardo Brasca]

u is a fixed universe, it can be Type but it can be anything else, while Nat : Type, this is why Lean is complaining.

[Riccardo Brasca]

Note that you cannot quantify over universes, so you cannot say "for all u blah blah"

[Riccardo Brasca]

What probably confuses you is that things like

universe u

axiom h (X : Type u) : True

example : True := h Nat

do work. This is because in this case Lean actually create a family of axioms h.{u}, one for each universe u, giving the impression that h starts with ∀ u, ... , but technically this is not the case.

[Edward van de Meent]

so: universes in the type of arguments are fixed (in the content of your def/theorem, that is), while universes in the type of declarations are variables.

[Riccardo Brasca]

This is my mental model (not sure if it is 100% correct)

[Edward van de Meent]

i'm pretty sure it's correct, that's why i summarised

[Riccardo Brasca]

Also, concerning your first example,

variable (h : ∀ (α : Type _), True)

example : True ∧ True := ⟨h Nat, h Type⟩

does not work, since _ is a metavariable, and Lean waits to give it a value. After the first h Nat, _ is 0 and so you cannot write h Type.

[Riccardo Brasca]

While

universe u

axiom h (X : Type u) : True

example : True ∧ True := ⟨h Nat, h Type⟩

is OK.

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Also, concerning your first example,

variable (h : ∀ (α : Type _), True)

example : True ∧ True := ⟨h Nat, h Type⟩

does not work, since _ is a metavariable, and Lean waits to give it a value. After the first h Nat, _ is 0 and so you cannot write h Type.

I am not 100% sure that this has to do with metavariables, because this works

def h (α : Type _) : True := True.intro

example : True ∧ True := ⟨h Nat, h Type⟩

(and _is also a metavariable); I think this is again related to what @Edward van de Meent was saying about the role of universes in arguments vs. in declarations...

[Edward van de Meent]

variables aren't declarations? they are arguments.

[Riccardo Brasca]

@Filippo A. E. Nuccio I think your example works because Lean creates a family of def, each one with a metavariable

[Riccardo Brasca]

But I can very well be wrong here

[Filippo A. E. Nuccio]

Edward van de Meent said:

variables aren't declarations? they are arguments.

Then I do not understand your answer above

so: universes in the type of arguments are fixed (in the content of your def/theorem, that is), while universes in the type of declarations are variables.

[Edward van de Meent]

what i mean, is that if you have def foo : Type u, you get foo.{u} : Type u for any u, so it is variable. however, in the content of def foo (x:Type u) : _ := bla, at bla you dont get to choose the level u anymore.

[Edward van de Meent]

the argument (x:Type u) has fixed universe u, and so does variable (x:Type u) (since they're both arguments)

[Marcus Rossel]

Riccardo Brasca said:

Filippo A. E. Nuccio I think your example works because Lean creates a family of def, each one with a metavariable

It seems that when you have a level wildcard in a def, then Lean does not create a level mvar for it, but instead creates a universe parameter for it. That is, hovering over the definition of h gives h.{u_1} (α : Type u_1) : True.
I guess that makes sense, because it would feel kind of strange to have a definition with lingering mvars.

[Riccardo Brasca]

Ah yes, sure.

[Kyle Miller]

@Marcus Rossel The rules are basically (1) "each lingering level metavariable at the end of elaborating the "header" of a declaration (the binders and the resulting type) is replaced with a fresh level parameter" and (2) "when a constant is elaborated, its level parameters get instantiated with fresh level metavariables".

Rule 2 should be thought of as being like how implicit arguments work. Implicit parameters get instantiated with fresh expression metavariables when an application is being elaborated.