Stuck at solving universe constraint

Stream: lean4

[Marcus Rossel]

I have a pretty contrived MWE, showing a case where Lean/I can't figure out a universe constraint:

inductive E
  | e₁
  | e₂

variable (α β) [ia : Inhabited α] [ib : Inhabited β]

def E.type : E → Type _
  | e₁ => α
  | e₂ => α × β

variable {α β}

def E.thing : (e : E) → (E.type α β e)
  | e₁ => @Inhabited.default α _
  | e₂ => (@Inhabited.default α _, @Inhabited.default β _)

def f (e : E) : Prop :=
  (@E.thing α β ia ib e) = (@E.thing α β ia ib e)

On the last line, Lean complains:

stuck at solving universe constraint
  max (?u.4095+1) (?u.4106+1) =?= max (?u.4096+1) (?u.4095+1)
while trying to unify
  Type (max ?u.4106 ?u.4095) : Type (max (?u.4106 + 1) (?u.4095 + 1))
with
  Type (max ?u.4096 ?u.4095) : Type (max (?u.4096 + 1) (?u.4095 + 1))

I think the problem arises in some way from the type signature of E.type:

E.type : Type (max u_1 u_2) → Type u_2 → E → Type (max u_1 u_2)

The signature shows that Lean has to assume α to live in a universe at least as big as β's, so we get α : Type (max u_1 u_2).
Changing E.type to the following:

def E.type : E → Type _
  | e₁ => α × β
  | e₂ => α × β

... makes the type signature simpler (Type u_1 → Type u_2 → E → Type (max u_1 u_2)) and fixes the problem.
What is the underlying problem here?

[Marcus Rossel]

Here's a slight simplification of the MWE:

inductive E
  | e₁
  | e₂

def E.type (α β : Type _) : E → Type _
  | e₁ => α
  | e₂ => α × β

def make (α) : α := sorry

def E.thing : (e : E) → (E.type α β e) :=
  make (E.type α β e)

[Reid Barton]

Lean inferred the correct type for E.type, but it's kind of unusable (unless you write explicit universe variable arguments) because there is no way to infer u_1 at a use of it. I imagine you just want to assume that α and β live in the same universe.

[Reid Barton]

Also, I can't tell what you're doing from the MWE obviously, but you could consider forgetting about universes and just using Type everywhere.

[Marcus Rossel]

I'm never sure what I'd be "losing" by constraining type-parameters to certain universes, so I always go for Type _.
But having α and β live in the same universe seems like a good solution.

[Mac]

One thing that surprises me here is thatα and β are in the same binder, but don't they have the same type (and thus the same universe) . Apparently Type _ does some magic that assigns them different types none-the-less (which wouldn't be possible normally). Is that expected? It seems rather odd to me.

[Reid Barton]

I guess it gets syntactically expanded to two binders first, then the metavariables get filled in. Whether this is a good thing is perhaps debatable.

[Marcus Rossel]

FWIW, when I write def foo (α β) : ... I expect the semantics of def foo (α : Type u) (β : Type v) : ..., because it's the most general version.

[Mac]

@Marcus Rossel note that def foo (α β) : ... actually gives def foo (α : Sort u) (β : Sort v) : ... because that it is the most general version. :P

[Marcus Rossel]

Ahh of course :D