Overeager default case

Description

Consider the following Lean code:

set_option trace.Compiler.explicitRc true
def escape (s : String) : String := Id.run do
  let mut out := ""
  let mut i := s.startPos
  let mut j := s.startPos
  while h : j ≠ s.endPos do
    let c := j.get h
    if let some esc := subst c then
      out := out ++ s.extract i j ++ esc
      j := j.next h
      i := j
    else
      j := j.next h
  if i = s.startPos then s  -- no escaping needed, return original
  else out ++ s.extract i j
where
  subst : Char → Option String
    | '&' => some "&"
    | '<' => some "&lt;"
    | '>' => some "&gt;"
    | '"' => some "&quot;"
    | _ => none

This produces:

def _private.Init.While.0.Lean.Loop.forIn.loop._at_.escape.spec_0 @&s b : obj :=
      let snd := proj[1] b;
      inc snd;
      let fst := proj[0] b;
      inc fst;
      let _x.1 := reset[2] b;
      let fst := proj[0] snd;
      inc fst;
      let snd := proj[1] snd;
      inc snd;
      let _x.2 := reset[2] snd;
      let _x.3 := String.utf8ByteSize s;
      let _x.4 := Nat.decEq fst _x.3;
      cases _x.4 : obj
      | Bool.false =>
        let c := String.decodeChar s fst ◾;
        let _x.5 := escape.subst c;
        cases _x.5 : obj
        | Option.some =>
          let val.6 := proj[0] _x.5;
          inc val.6;
          dec _x.5;
          let _x.7 := String.extract s fst fst;
          dec fst;
          let _x.8 := String.append snd _x.7;
          dec _x.7;
          let out := String.append _x.8 val.6;
          dec val.6;
          let i := String.Pos.next s fst ◾;
          dec fst;
          let _x.9 := reuse _x.2 in ctor_0[MProd.mk] i out;
          let _x.10 := reuse _x.1 in ctor_0[MProd.mk] i _x.9;
          let _x.11 := _private.Init.While.0.Lean.Loop.forIn.loop._at_.escape.spec_0 s _x.10;
          return _x.11
        | _ =>
          dec _x.5;
          let j := String.Pos.next s fst ◾;
          dec fst;
          let _x.12 := reuse _x.2 in ctor_0[MProd.mk] j snd;
          let _x.13 := reuse _x.1 in ctor_0[MProd.mk] fst _x.12;
          let _x.14 := _private.Init.While.0.Lean.Loop.forIn.loop._at_.escape.spec_0 s _x.13;
          return _x.14
      | Bool.true =>
        let _x.15 := reuse _x.2 in ctor_0[MProd.mk] fst snd;
        let _x.16 := reuse _x.1 in ctor_0[MProd.mk] fst _x.15;
        return _x.16

Observe in particular that the cases _x.5 decides to insert a dec _x.5. However, we can statically know that _x.5 is going to be a none and thus doesn't need to be decremented. The reason that we have a default case here is due to the if let := elaborator. That said the compiler should be able to recover the information about the default branch on its own in order to avoid the reference count.

Steps to Reproduce

Expected behavior: No refcounts on the discriminant in the none branch

Actual behavior: Refcounts on the discriminant in the non branch

Versions

Lean 4.30.0-nightly-2026-02-20
Target: x86_64-unknown-linux-gnu

Impact

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

Reproduce the example with trace.Compiler.explicitRc enabled and inspect the generated loop around the if-let default branch. Focus on the compiler's handling of the Option discriminant and compare the none branch with the shown output. Done means the none branch no longer decrements the statically known none value, while the behavior remains correct.