Why doesn't `Bind.bind` allow universe polymorphism?

Stream: lean4

[Gravifer]

I just found out that >>= aka Bind.bind requires all intermediate results to stay in the same sort, while more specific binds like Option.bind allow disuniformity:

section
variable {α : Type u} {β : Type v} {γ : Type w} [Inhabited α] [Inhabited β] [Inhabited γ]
variable (x : α) (f : α -> Option β) (g : β -> Option γ)
/--error: Application type mismatch: The argument
  g
has type
  β → Option.{w} γ
of sort `Type (max v w)` but is expected to have type
  ?m.3 → Option.{w} γ
of sort `Type w` in the application
  @Bind.bind.{w, w} Option.{w} (@Monad.toBind.{w, w} Option.{w} instMonadOption.{w}) ?m.3 γ ?m.5 g
-/
#guard_msgs in
example : Option γ := f x >>= g
example : Option γ := Option.bind (f x) g

/--info: Bind.bind.{u, v} {m : Type u → Type v} [self : Bind.{u, v} m] {α β : Type u} : m α → (α → m β) → m β -/
#guard_msgs in #check Bind.bind
/--info: Option.bind.{u_1, u_2} {α : Type u_1} {β : Type u_2} : Option.{u_1} α → (α → Option.{u_2} β) → Option.{u_2} β -/
#guard_msgs in #check Option.bind
end

I suspect that allowing different sorts may not make sense for a general monad other than Option, but I find it hard for me to pin down exactly why.

[Eric Wieser]

See #lean4 > universe polymorphic IO @ 💬

[Gravifer]

Is it ok if I put similarly novice questions in this thread as well?
Why don't we define PUnit and PEmpty with Typeinstead of Sort?

inductive PUnit : Sort u where
  /-- The only element of the universe-polymorphic unit type. -/
  | unit : PUnit

inductive True : Prop where
  /-- `True` is true, and `True.intro` (or more commonly, `trivial`)
  is the proof. -/
  | intro : True

Since True and False behave like Unit and Empty, I thought the situation would be like that of products

structure Prod (α : Type u) (β : Type v) where
  /--
  Constructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.
  -/
  mk ::
  /-- The first element of a pair. -/
  fst : α
  /-- The second element of a pair. -/
  snd : β

structure And (a b : Prop) : Prop where
  /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
  intro ::
  /-- Extract the left conjunct from a conjunction. `h : a ∧ b` then
  `h.left`, also notated as `h.1`, is a proof of `a`. -/
  left : a
  /-- Extract the right conjunct from a conjunction. `h : a ∧ b` then
  `h.right`, also notated as `h.2`, is a proof of `b`. -/
  right : b

[Gravifer]

I just realize there is such a thing as PProd, just below Prod in the source

structure PProd (α : Sort u) (β : Sort v) where
  /-- The first element of a pair. -/
  fst : α
  /-- The second element of a pair. -/
  snd : β

but now I'm confused how the universe of the output is deduced

#print PProd /--info:
structure PProd.{u, v} (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)
number of parameters: 2
fields:
  PProd.fst.{u, v} : α
  PProd.snd.{u, v} : β
constructor:
  PProd.mk.{u, v} {α : Sort u} {β : Sort v} (fst : α) (snd : β) : PProd.{u, v} α β
-/
#check PProd.{0,0} /--info: PProd.{0, 0} : Prop → Prop → Type -/

[Gravifer]

I also notice that Unit is abbrev for PUnit.{1} while Empty is unrelated to PEmpty; I feel baffled.

---

I tried

example : Empty = PEmpty.{1} := by nofun  --!error: Missing cases:

except there shouldn't be any cases ...?