Lean4’s Nat.succ in kernel is stricter than expected

Nat_succ.lean

import Lean
import Mathlib

elab "#kernel_reduce" t:term : command => Lean.Elab.Command.runTermElabM fun _ => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize t none
  let e' ← Lean.ofExceptKernelException <| Lean.Kernel.whnf (← Lean.getEnv) (← Lean.getLCtx) e
  Lean.logInfo m!"{e'}"

def slow : Bool := Nat.sqrt (1000 * 1000) = 1000 

/-- error: (kernel) deep recursion detected -/
#guard_msgs in
#kernel_reduce slow

/-- error: (kernel) deep recursion detected -/
#guard_msgs in
#kernel_reduce Nat.succ (if slow then 1 else 2)

/-- info: [if slow = true then 1 else 2] -/
#guard_msgs in
#kernel_reduce List.cons (if slow then 1 else 2) []