Kernel reduction of Nat.succ is more strict that expected

Stream: lean4

[Joachim Breitner]

I noticed this behavior which surprised me: The kernel reduction of Nat.succ e will try to reduce e even if it’s not actually required by its context, this sets its behavior apart from other constructors like List.cons:

import Lean

def foo : Nat → Nat
  | 0 => 0
  | n+1 => foo n/2
termination_by n => n

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 := foo 1000000 = 0

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

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

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

This is not really an issue, but part of how the kernel efficiently works with natural numbers, so I’ll just record this fact here for posterity.