Generic over universe levels in argument

Stream: lean4

[Tage Johansson]

I have a problem when I want to wrap two different monads (m and n) in the same monad o.
However if m and n have different type levels, this doesn't work:

def foo {m : Type u → Type v} {n : Type u → Type w} {o : Type _ → Type _} (α : Type u) : Type _ :=
  o (m α) → o (n α)

Is there any solution to this? I would like to have o being generic over a type level, something like {o : {w₂} → Type w₂ → Type _}, but that code doesn't seem to work.

[Eric Rodriguez]

If you really care about this, you'll probably have to docs4#ULift to max v w

[Kyle Miller]

Tage Johansson said:

I would like to have o being generic over a type level, something like {o : {w₂} → Type w₂ → Type _}

This is a limitation of Lean's type system: you can't have variables that are polymorphic over universe levels. Only top-level definitions can be universe polymorphic. (What would be the type of {w₂} → Type w₂ → Type _? There's not a big enough universe for it.)

Technically, if you have a monad instantiated twice with different universe variables, then even though the monads are from the same definition, the resulting monads are different and have no relation to each other. (I think of universe levels as giving you a family of definitions rather than a single definition.)

One thing you could do is have foo take two different o arguments. Another is to do something like what Eric is suggesting; one implementation is to make all the monads use the same universe levels and then use ULift when you need types from different universes.