Crash on overapplication of Quot.mk or trivial structures

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 crashes when the program contains an overapplication of an unsafeCast from Quot α _ to α or from a trivial wrapper to its sole parameter (both of which are documented as safe uses of unsafeCast).

Steps to Reproduce

Both of these crash:

unsafe def five : Nat := (unsafeCast (Quot.mk (fun _ _ => True) (· + 1)) : Nat → Nat) 4
#eval five

inductive Wrap where | mk (run : Nat → Nat)
unsafe def five : Nat := (unsafeCast (Wrap.mk (· + 1)) : Nat → Nat) 4
#eval five

Versions

Lean 4.34.0-nightly-2026-08-08
Target: x86_64-unknown-linux-gnu Linux

Additional Information

The root cause appears to be in LetValue.toMono where the overapplied arguments are dropped:

https://github.com/leanprover/lean4/blob/f29e9e488ea8242c875806e4b0564820c2d553b2/src/Lean/Compiler/LCNF/ToMono.lean#L94

It looks like this issue was found before for Quot.lift and fixed in https://github.com/leanprover/lean4/pull/9827, but not for these other two cases, perhaps because they can only occur if combined with unsafeCast.

Impact

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

Start in src/Lean/Compiler/LCNF/ToMono.lean at LetValue.toMono around line 94, then run the two minimal unsafeCast examples from the issue. Compare the handling of overapplied arguments with the earlier Quot.lift fix in PR #9827; done means both examples compile and evaluate without crashing.