Termination proof failure in the presence of default arguments

[dupuisf]

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

When a termination_by statement depends on parameters with a default value, one can sometimes get the error The termination argument's type must not depend on the function's varying parameters.

The error disappears when the default values are removed.

Context

This error occurred when coding a solution to an Advent of Code problem, and was also brought up on the Lean Zulip

Steps to Reproduce

1. Copy-paste the following code example above into an empty file (no imports required):

def foo (as : Array Nat) (i := 0) (j := as.size - 1) : Array Nat :=
  if j ≤ i then as
  else
    let newas := as.set! 0 0
    foo newas (i+1) (j-1)
termination_by j - i

Expected behavior: The termination_by statement is accepted and no error occurs.
Actual behavior: The termination_by statement produces the error

The termination argument's type must not depend on the function's varying parameters, but pack's termination argument does:
  (disk : Array (Option Nat)) → optParam Nat 0 → optParam Nat (disk.size - 1) → optParam Nat (disk.size - 1)
Try using `sizeOf` explicitly`

Versions

Lean 4.15.0-rc1 (locally, and also on live.lean-lang.org)
Target: x86_64-unknown-linux-gnu
Arch Linux x86_64, kernel 6.6.63-1-lts

Also tried Lean 4.16.0-nightly-2024-12-09 on live.lean-lang.org, the bug is also present there.

Impact

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

[nomeata]

JFTR, another work-around is to write

termination_by @id Nat (j - i)

to infer a type without default arguments.