`(kernel) deep recursion detected` error with `BitVec.umulOverflow` in an if-then-else

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

The mwe theorem below gives a (kernel) deep recursion error. The MWE has various seemingly unrelated, yet load-bearing elements, e.g. (a) PoisonOr is a wrapper around Option, replacing uses of PoisonOr with Option makes the error disappear, and (b) the example has an if-then-else, removing it makes the error disappear. It's thus hard to point out what exactly triggers the error.

/-! # Preliminary -/

/--
`PoisonOr` is a simple wrapper around `Option`
-/
structure PoisonOr (α : Type) where
  toOption : Option α

namespace PoisonOr

def value : α → PoisonOr α := (⟨some ·⟩)

instance : Bind PoisonOr where
  bind := fun a f => match a with
    | ⟨none⟩    => ⟨none⟩
    | ⟨some a⟩  => f a

theorem bind_assoc (x : PoisonOr α) (f : α → PoisonOr β) (g : β → PoisonOr γ) :
    x >>= f >>= g = x >>= fun x => f x >>= g := by
  rcases x with (_|_) <;> rfl

end PoisonOr

/-! # MWE -/

def BitVec.umulOverflow' {w : Nat} (x y : BitVec w) : Prop :=
  x.toNat * y.toNat ≥ 0
  -- -----^
  -- Making this `+` has no effect, the error remains.
  --
  -- However, replacing `x.toNat` with a constant (even if large), does make the
  --   error disappear
  --
  -- Also note that the rhs was originally `2 ^ w`, but I've replaced it with
  -- `0` to rule out `2 ^ w` being computed. This had no effect on the error.

instance : DecidableRel (@BitVec.umulOverflow' w) := by
  unfold BitVec.umulOverflow';
  -- If we `sorry` out this instance, the error disappears
  -- sorry
  infer_instance


/-
The following gives the error:

  (kernel) deep recursion detected

-/
theorem mwe (x' : BitVec 32) :
    (do
      let _z ←
        (do
          let y' ← PoisonOr.value 0#32
          -- ----- ^^^^^^^^^^^^^^
          -- Replacing the `PoisonOr` wrapper with `Option` (in the whole MWE)
          -- makes the error disappear
          --
          if x'.umulOverflow' (65537#_) then
          -- ----------------- ^^^^^^^
          -- Making this constant smaller, or replacing it with a variable,
          -- makes the error disappear
          --
            PoisonOr.value 0#32
          else
            PoisonOr.value 0#32)
      PoisonOr.value 0) = PoisonOr.value 0 := by
  -- Running `simp only [ite_self]` first makes the error disappear
  --   (but is not applicable in my actual scenario, as the branches of the real
  --    code aren't the same)
  -- Similarly, rewriting the statement to not have the if-then-else also
  -- makes the error disappear, even if the if condition is still present.

  rw [PoisonOr.bind_assoc]
  -- ^^ This rewrite is what seems to trigger the recursion, removing it
  --    makes the error disappear.
  sorry

Context

I've reported on Zulip as well: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Tricky.20.60.28kernel.29.20deep.20recursion.20detected.60.20error/with/525032358

I ran a build through samply as well, which revealed that the offending functions are lean::type_checker::{whnf, reduce_nat} in libleanshared.so, which seems to suggest the core of the problem is the natural number multiplication being reduced.

Suppressing the kernel error using set_option debug.skipKernelTC and then running the generated olean through lean4lean (on previous versions, see the Zulip thread for details), gives no output, which presumably means lean4lean was happy with the generated term.

Steps to Reproduce

1. Open up the MWE
2. Observer the kernel error

Expected behavior: The mwe theorem ought to be accepted

Actual behavior: A (kernel) deep recursion detected error occurs

Versions

Lean 4.22.0-nightly-2025-06-20
Target: x86_64-unknown-linux-gnu

on live.lean-lang.org

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 MWE centered on BitVec.umulOverflow', the PoisonOr wrapper, and the rw [PoisonOr.bind_assoc] step; reproduce it on the specified Lean nightly. Inspect the kernel type checker paths whnf and reduce_nat mentioned in the report, and consider the issue done when the theorem is accepted without a deep-recursion error.