Unwanted universe metavariables

Stream: lean4

[François G. Dorais]

Eric Wieser said:

At least in Lean3 you could write variables {A B C D E : Type*} and have it do the right thing; in lean 4 you have to deal with the fact that two types may accidentally be assigned the same universe

What is "the right thing" for you? Lean 4 variable {α β γ δ ε : Type _} assigns different universes to each type. You have to write variable {α β γ δ ε : Type u} to force them to have the same type.

[Kyle Miller]

You have to be careful with variable {α β γ δ ε : Type _}, since it assign different universe metavariables. Depending on how the types are used, they could be all different, all the same, or even specialized to particular universe levels (like 0). If you want to be sure that they are actually all different (and universe polymorphic), you have to do variable {α : Type s} {β : Type t} {γ : Type u} {δ : Type v} {ε : Type w}.

[Yaël Dillies]

No, that's not what the Lean 4 version does. It assigns different universe metavariables, which Lean can then unify at will. This is what Eric is referring to by "accidentally assigned to the same universe".

[Eric Wieser]

To be clear, Yael is saying that your claim is wrong @François G. Dorais, not Kyle's

[Eric Wieser]

What is "the right thing" for you?

It's to have {A B C D E : Type*} syntax which means universes uA uB uC uD uE and {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} {E : Type uE}

[Kyle Miller]

@Eric Wieser What do you know, it turns out it's really easy to implement:

import Lean

open Lean

elab "Sort*" : term => do
  let u ← Lean.Meta.mkFreshLevelMVar
  Elab.Term.levelMVarToParam (.sort u)

elab "Type*" : term => do
  let u ← Lean.Meta.mkFreshLevelMVar
  Elab.Term.levelMVarToParam (.sort (.succ u))

section
variable (α β γ : Type _)
-- Allowed, metavariables
#check α = β
end

section
variable (α β γ : Type*)
-- Not allowed, distinct level variables
#check α = β
/-
type mismatch
  β
has type
  Type u_2 : Type (u_2 + 1)
but is expected to have type
  Type u_1 : Type (u_1 + 1)
-/
end

[Eric Wieser]

Huh, I was expecting the binder syntax not to re-elaborate each time

[Eric Wieser]

I guess naming the universes to match the type names is a lot more work

[Kyle Miller]

If it didn't, then Type _ wouldn't work the way it does, they'd all get the same metavariable

[François G. Dorais]

I know what Lean 4 does. (I also know I should have said metavariables, my bad.) I still don't know why it's "the wrong thing".

It's been a long while since I've used Lean 3, probably too long to miss its features, but I do remember that Lean 3's universe clashes were much more annoying than in Lean 4. In my mind, it's clear that assigning each variable its own universe metavariable is the right thing to do.

Is there an example where a universe error would be more desirable than unification?

[Kevin Buzzard]

I think the issue was more that lean 3 would sometimes incorrectly over-unify without telling you! In those cases you would rather see the error which you can then try and fix, rather than being oblivious to the problem in your code.

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Subsingleton.2Eelim.20in.20a.20def/near/339122362 has a couple examples where since they're metavariables you can get surprises like Sort _ unifying with Prop.

[Kyle Miller]

@Eric Wieser The situation in Lean 3 is more subtle than you might remember.

It looks like Type* works by giving fresh universe levels:

variables {α β : Type*}
#check α = β
/-
type mismatch at application
  α = β
term
  β
has type
  Type u_2 : Type (u_2+1)
but is expected to have type
  Type u_1 : Type (u_1+1)
-/

But then this is ok:

example {α β : Type*} : α = β := sorry

[Eric Wieser]

Kyle, that's exactly the behavior I remember; variables was the workaround for Type* being annoying in declarations

[Eric Wieser]

We had a bunch of problems that were fixed by hoisting the {Type*} to the top of the file

[Kyle Miller]

Ok, it was unclear whether you were talking about Type* or the variable command, and it didn't occur to me you were talking about the variable command.

[Kyle Miller]

In Lean 3, the variable command itself is responsible for elaborating all the binders and generalizing universe level metavariables to level variables, but in Lean 4 binders are re-elaborated for every declaration.

[Eric Wieser]

I still don't know why it's "the wrong thing".

I guess my claim is the very slightly weaker "it's a footgun that we don't seem to use to shoot anything but our feet with"

[Eric Wieser]

An example of the footgun:

variable {α : Sort _} (a b : α)
example : a = b := by
  let useless := And.intro a b
  rfl  -- succeeds!?

[François G. Dorais]

I see. I guess I've been lucky to avoid that gotcha. I see how it could be a real pain to debug that kind of issue.

[Mario Carneiro]

Eric Wieser said:

An example of the footgun:

variable {α : Sort _} (a b : α)
example : a = b := by
  let useless := And.intro a b
  rfl  -- succeeds!?

Another way to fix this issue would be to convert universe mvars to level params once you get to the type, and then either do it again when you get to the value or give an error if there are any level mvars in the value. (The latter behavior would cause an error if there is a universe in the body that you didn't mention in the type.)

[Eric Wieser]

Eric Wieser said:

I guess naming the universes to match the type names is a lot more work

Do you have any ideas for this?

[Notification Bot]

22 messages were moved here from #lean4 > function.combine by Eric Wieser.