fix: recursive overapplication at WF/Fix.lean

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -50,10 +50,11 @@ private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (d
     | Expr.app _ _ _ =>
       let processApp (e : Expr) : TermElabM Expr :=
         e.withApp fun f args => do
-          if f.isConstOf recFnName && args.size == fixedPrefixSize + 1 then
-            let r := mkApp F (← loop F args.back)
+          if f.isConstOf recFnName && args.size >= fixedPrefixSize + 1 then
+            let r := mkApp F (← loop F args[fixedPrefixSize])
             let decreasingProp := (← whnf (← inferType r)).bindingDomain!
-            return mkApp r (← mkDecreasingProof decreasingProp decrTactic?)
+            let r := mkApp r (← mkDecreasingProof decreasingProp decrTactic?)
+            return mkAppN r (← args[fixedPrefixSize+1:].toArray.mapM (loop F))
           else
             return mkAppN (← loop F f) (← args.mapM (loop F))
       let matcherApp? ← matchMatcherApp? e

tests/lean/run/wfOverapplicationIssue.lean

@@ -0,0 +1,12 @@
+theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
+  simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
+  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
+    unfold anyM.loop
+    intro h
+    split at h
+    . simp [Bind.bind, pure] at h; split at h
+      next he => subst a; apply sizeOf_get_lt
+      next => have ih := aux (j+1) h; assumption
+    . contradiction
+  apply aux 0 h
+termination_by aux j => as.size - j