Proof irrelevance handling in the compiler allows for unconstrained application without `unsafe`

Prerequisites

• 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

The compiler fails to uphold the invariant that proofs are always represented as lean_box(0), allowing unconstrained application of any two runtime values without unsafe.

Context

#general > PSigma' compilation @ 💬

Steps to Reproduce

structure Wrapped (α : Sort u) where
  out : α
  more : Unit := () -- prevent trivial structure

@[noinline]
protected def Wrapped.id : Wrapped (α → α) := { out := id }

@[noinline]
def Wrapped.app (f : Wrapped (α → β)) (a : Wrapped α) : Wrapped β :=
  { out := f.out a.out }

abbrev WrappedProof := Wrapped True

@[noinline]
def WrappedProof.of (x : α) : WrappedProof :=
  have heq : (True → True) = (α → True) := by simp
  (heq ▸ Wrapped.id).app { out := x }

@[noinline]
def WrappedProof.apply (x y : WrappedProof) : WrappedProof :=
  have heq : True = (True → True) := by simp
  .app (heq ▸ x) y

@[noinline]
def WrappedProof.act (x : WrappedProof) : BaseIO Unit :=
  (Wrapped.app { out := fun _ => pure () } x).out

def safeUnsafeCast [Inhabited β] (x : α) : BaseIO β := do
  let ref : IO.Ref β ← IO.mkRef default
  (WrappedProof.of (ref.set : β → BaseIO Unit)).apply (.of x) |>.apply (.of 0) |>.act
  ref.get

/-- info: true -/
#guard_msgs in #eval (safeUnsafeCast (1 : Nat) : BaseIO Bool)

Expected behavior:
The second line of safeUnsafeCast has no effect, resulting in a return value of default : Bool, which is false.

Actual behavior:
The second line of safeUnsafeCast causes a call of ref.set x, even though this call would not be type correct.

Explanation:
Because Wrapped.id always allocates an identity closure regardless of the universe level, you can use Wrapped.id.{0} to create an identity closure in a position of type True → True. This is already bad, since we expect all proofs to be represented as lean_box(0) without any allocation. However, even worse, you can cast this along the equality (True → True) = (α → True) which holds due to propext, giving an identity closure of type α → True.
While the identity closure being typed True → True might have been acceptable, having it of type α → True is certainly not, since both sides don't even have the same type. Now this allows you to take any term of type α and then, through application of the closure, allows you to interpret it as a term of type True! And, since True = (True → True), you can cast any of these back into a function and apply it to another term of type True; both of which may just have been any value. With this idea, WrappedProof.apply (.of f) (.of a) lets you call lean_apply_1(f, a) for any two terms, regardless of type. This can cause all sorts of problems, including calling IO.Ref.set with a value of the wrong type.

Versions

Lean 4.35.0-nightly-2026-08-22

Impact

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

Start with the self-contained reproducer in the issue and run the #eval for safeUnsafeCast on the Lean nightly configuration. Trace compilation of Wrapped.id, WrappedProof.apply, and WrappedProof.act, focusing on the proof-representation invariant. Done means the reproducer returns default : Bool (false) and cannot invoke ref.set with a mismatched value without unsafe.