fix: FunInd with nested well-founded recurison and late fixed parameters (#8094)

This PR fixes the generation of functional induction principles for
functions with nested nested well-founded recursion and late fixed
parameters. This is a follow-up for #7166. Fixes #8093.

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

@@ -20,17 +20,14 @@ open Eqns
 structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
-  fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
   fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
-
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
     (argsPacker : ArgsPacker) : MetaM Unit := do
-  let fixedPrefixSize := fixedParamPerms.numFixed
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -43,7 +40,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker, fixedParamPerms }
+            declNames, declNameNonRec, argsPacker, fixedParamPerms }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Meta/Tactic/FunInd.lean

@@ -875,15 +875,17 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
     -- Look for _unary redexes
     if e.isAppOf eqnInfo.declNameNonRec then
       let args := e.getAppArgs
-      if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
-        let packedArg := args.back!
-          let some (i, unpackedArgs) := eqnInfo.argsPacker.unpack packedArg
-            | throwError "Unexpected packedArg:{indentExpr packedArg}"
-          let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
-          let e' := mkAppN e' args.pop
-          let e' := mkAppN e' unpackedArgs
-          let e' := mkAppN e' args[eqnInfo.fixedPrefixSize+1:]
-          return .continue e'
+      if h : args.size ≥ eqnInfo.fixedParamPerms.numFixed + 1 then
+        let xs := args[:eqnInfo.fixedParamPerms.numFixed]
+        let packedArg := args[eqnInfo.fixedParamPerms.numFixed]
+        let extraArgs := args[eqnInfo.fixedParamPerms.numFixed+1:]
+        let some (funIdx, ys) := eqnInfo.argsPacker.unpack packedArg
+          | throwError "Unexpected packedArg:{indentExpr packedArg}"
+        let args' := eqnInfo.fixedParamPerms.perms[funIdx]!.buildArgs xs ys
+        let e' := .const eqnInfo.declNames[funIdx]! e.getAppFn.constLevels!
+        let e' := mkAppN e' args'
+        let e' := mkAppN e' extraArgs
+        return .continue e'
 
     return .continue e)
   mkExpectedTypeHint value cleanType
@@ -902,6 +904,7 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) : MetaM Name := do
   return inductName
 where doRealize inductName := do
   let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
+  mapError (f := (m!"Cannot unpack functional cases principle {.ofConstName unaryInductName} (please report this issue)\n{indentD ·}")) do
   let ci ← getConstInfo unaryInductName
   let us := ci.levelParams
   let value := .const ci.name (us.map mkLevelParam)
@@ -930,7 +933,7 @@ where doRealize inductName := do
         return value
 
   unless ← isTypeCorrect value do
-    logError m!"failed to unpack induction principle:{indentExpr value}"
+    logError m!"final term is type incorrect:{indentExpr value}"
     check value
   let type ← inferType value
   let type ← elimOptParam type

tests/lean/run/issue8093.lean

@@ -0,0 +1,13 @@
+axiom testSorry : α
+
+def foo (n : Nat) (p : Nat) : Nat :=
+  foo (foo (n - 1) p) p
+termination_by n
+decreasing_by all_goals exact testSorry
+
+/--
+info: foo.induct (p : Nat) (motive : Nat → Prop) (case1 : ∀ (x : Nat), motive (x - 1) → motive (foo (x - 1) p) → motive x)
+  (n : Nat) : motive n
+-/
+#guard_msgs in
+#check foo.induct