fix: strip optional parameters when elaborating the termination hints (#7335)

This PR modifies `elabTerminationByHints` in a way that the type of the
recursive function used for elaboration of the termination measure is
striped of from optional parameters. It prevents introducing
dependencies between the default values for arguments, that can cause
the termination checker to fail.

Closes https://github.com/leanprover/lean4/issues/6351.

src/Lean/Elab/PreDefinition/TerminationMeasure.lean

@@ -52,7 +52,6 @@ Elaborates a `TerminationBy` to an `TerminationMeasure`.
 def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
     (hint : TerminationBy) : TermElabM TerminationMeasure := withDeclName funName do
   assert! extraParams ≤ arity
-
   if h : hint.vars.size > extraParams then
     let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
       m!"{funName} only binds {parameters extraParams}."
@@ -64,7 +63,7 @@ def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams :
 
   -- Bring parameters before the colon into scope
   let r ← withoutErrToSorry <|
-    forallBoundedTelescope type (arity - extraParams) fun ys type' => do
+    forallBoundedTelescope (cleanupAnnotations := true) type (arity - extraParams) fun ys type' => do
       -- Bring the variables bound by `termination_by` into scope.
       elabFunBinders hint.vars (some type') fun xs type' => do
         -- Elaborate the body in this local environment

tests/lean/run/issue6531.lean

@@ -0,0 +1,9 @@
+-- This used to cause
+-- error: The termination argument's type must not depend on the function's varying parameters
+
+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