The specialization pass does not specialize for oversaturating arguments

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

Specialization does not appear to specialize for oversaturating arguments of a call to a function with a @[specialize] annotation.

Steps to Reproduce

@[specialize]
def foo {α} : Nat → (α → α) → α → α 
  | 0, f, a => f a 
  | n+1, f, a => foo n f a

-- The following example demonstrates that `f` is properly specialized:
set_option trace.Compiler.saveBase true in
/--
trace: [Compiler.saveBase] size: 6
    def foo._at_._example.spec_0 x.1 x.2 : Nat :=
      cases x.1 : Nat
      | Nat.zero =>
        let _x.3 := 1;
        let _x.4 := Nat.add x.2 _x.3;
        return _x.4
      | Nat.succ n.5 =>
        let _x.6 := foo._at_._example.spec_0 n.5 x.2;
        return _x.6
[Compiler.saveBase] size: 2
    def _example n : Nat :=
      let _x.1 := 5;
      let _x.2 := foo._at_._example.spec_0 n _x.1;
      return _x.2
-/
#guard_msgs in
example {n} := foo n (· + 1) 5

-- The following example demonstrates that while `f` is properly specialized, `a` is not:
set_option trace.Compiler.saveBase true in
/--
trace: [Compiler.saveBase] size: 6
    def foo._at_._example.spec_0 x.1 x.2 _y.3 : Nat :=
      cases x.1 : Nat
      | Nat.zero =>
        let _x.4 := x.2 _y.3;
        let _x.5 := x.2 _x.4;
        return _x.5
      | Nat.succ n.6 =>
        let _x.7 := foo._at_._example.spec_0 n.6 x.2 _y.3;
        return _x.7
[Compiler.saveBase] size: 4
    def _example n : Nat :=
      fun _f.1 x.2 : Nat :=
        let _x.3 := 1;
        let _x.4 := Nat.add x.2 _x.3;
        return _x.4;
      let _x.5 := 5;
      let _x.6 := foo._at_._example.spec_0 n _f.1 _x.5;
      return _x.6
-/
#guard_msgs in
example {n} := foo n (fun f a => f (f a)) (· + 1) 5

Expected behavior: foo is specialized not only for (fun f a => f (f a)) but also for (· + 1).

Actual behavior: foo is specialized for (fun f a => f (f a)) but not for (· + 1).

Versions

Lean 4.26.0-nightly-2025-10-22
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.

Start by running the minimal reproducer and examining the specialization pass behavior for the two examples. Done means the second example specializes both the higher-order function and the oversaturating (· + 1) argument, matching the expected trace.