Coercion elaboration introduces monadic bind into non-monadic code, restricting universes

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

theorem simple {x : Option Int} {y : Option Nat} : x = y := by
  sorry

/-
simple {x : Option Int} {y : Option Nat} :
  x = do
    let a ← y
    pure ↑a
-/
#check simple

instance : Coe β (α ⊕ β) where
  coe x := .inr x

theorem foo (p : Option (α ⊕ Nat)) (q : Option Nat) : p = q := by
  sorry

/-
foo {α : Type} (p : Option (α ⊕ Nat)) (q : Option Nat) :
  p = do
    let a ← q
    pure (Sum.inr a)
-/
#check foo

theorem bar (p : Option (α ⊕ Nat)) (q : Option Nat) : p = q.map .inr := by
  sorry

/-
bar.{u_1} {α : Type u_1} (p : Option (α ⊕ Nat)) (q : Option Nat) : p = Option.map Sum.inr q
-/
#check bar

Here, the RHS of simple unexpectedly elaborates to a do block in the Option monad, which is surprising to users (note: it probably wouldn't be as surprising if instead of Option we were in something like MetaM).

What's problematic about this is that monads are not universe-polymorphic, so the elaborator forcing the bind can restrict universes unexpectedly. This is seen in foo: here, α lives in Type, while inserting the coercion by hand in bar allows for more general universes.

This can lead to theorems which are "silently" less polymorphic than they look, which in turn can lead to failures very far removed from the problematic code (as seen in CertifyingDatalog, where the distance is many hundreds of lines).

Context

This is minimized from a problem observed in CertifyingDatalog (where the problematic monad is List (from mathlib), not Option).

Expected behavior: simple and foo should just fail to elaborate.

Actual behavior: simple and foo elaborate, but with a monadic bind.

Versions

4.21.0-nightly-2025-05-12 on live.lean-lang.org

Additional Information

Lean.Meta.coerceMonadLift? seems to be the spot in the elaborator that is responsible for this behavior.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with Lean.Meta.coerceMonadLift? in the elaborator and reproduce the minimal simple and foo examples against the reported nightly version. Compare their elaborated forms with bar, then verify that the problematic examples fail to elaborate without restricting universes while the explicit map example remains valid.