Elaboration of multi variable binders

Stream: lean4

[Henrik Böving]

When defining this type:

abbrev Handler (σ m n : Type _ → Type _) := (x : Type _) → σ (m x) → n (σ x)

one might expect sigma m and n to have the same universe levels. However Lean does decide to go maximum polymorphic here:

Handler.{u_1, u_2, u_3} (m : Type u_1 → Type u_1) (n : Type u_2 → Type u_3) (σ : Type u_1 → Type u_2) :
  Type (max (max u_3 u_2) (u_1 + 1))

Now while this is a cool short-hand for spelling out the same Type _ -> Type _ signature thrice I am curious as to whether this is intended behavior or just an accident in the way that multi variable binders are elaborated.

If it is on purpose is there a specific reason apart from is it compact. If it is an accident: Do we consider this a bug given that it produces a slightly unintuitive result?

[Eric Wieser]

I'm pretty sure this is on purpose, and that it works for the same reason as

example (f : α → β → γ) (l1 l2 : List _) := List.zipWith f l1 l2

which fills the (type) metavariable in two different ways