fix: handle reordered indices in structural recursion (#6116)

This PR fixes a bug where structural recursion did not work when indices
of the recursive argument appeared as function parameters in a different
order than in the argument's type's definition.

Fixes #6015.

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -243,7 +243,7 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first
   recArgInfoss := recArgInfoss.map nonIndicesFirst
-  trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
+  trace[Elab.definition.structural] "recArgInfos:{indentD (.joinSep (recArgInfoss.flatten.toList.map (repr ·)) Format.line)}"
   -- Inductive groups to consider
   let groups ← inductiveGroups recArgInfoss.flatten
   trace[Elab.definition.structural] "inductive groups: {groups}"

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -27,7 +27,7 @@ constituents.
 structure IndGroupInfo where
   all       : Array Name
   numNested : Nat
-deriving BEq, Inhabited
+deriving BEq, Inhabited, Repr
 
 def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
   all       := indInfo.all.toArray
@@ -56,7 +56,7 @@ mutual structural recursion on such incompatible types.
 structure IndGroupInst extends IndGroupInfo where
   levels    : List Level
   params    : Array Expr
-deriving Inhabited
+deriving Inhabited, Repr
 
 def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData :=
   mkAppN (.const igi.all[0]! igi.levels) igi.params

src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -23,9 +23,9 @@ structure RecArgInfo where
   fnName       : Name
   /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
   numFixed     : Nat
-  /-- position of the argument (counted including fixed prefix) we are recursing on -/
+  /-- position (counted including fixed prefix) of the argument we are recursing on -/
   recArgPos    : Nat
-  /-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/
+  /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/
   indicesPos   : Array Nat
   /-- The inductive group (with parameters) of the argument's type -/
   indGroupInst : IndGroupInst
@@ -34,20 +34,23 @@ structure RecArgInfo where
   If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
   -/
   indIdx       : Nat
-deriving Inhabited
+deriving Inhabited, Repr
 
 /--
 If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
 into indices and major arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
+  let indexMajorPos := info.indicesPos.push info.recArgPos
+  for j in indexMajorPos do
+    assert! info.numFixed ≤ j && j - info.numFixed < xs.size
+    indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]!
+  -- Then the other arguments, in the order they appear in `xs`
   let mut otherArgs := #[]
   for h : i in [:xs.size] do
-    let j := i + info.numFixed
-    if j = info.recArgPos || info.indicesPos.contains j then
-      indexMajorArgs := indexMajorArgs.push xs[i]
-    else
+    unless indexMajorPos.contains (i + info.numFixed) do
       otherArgs := otherArgs.push xs[i]
   return (indexMajorArgs, otherArgs)
 

tests/lean/run/issue6015.lean

@@ -0,0 +1,21 @@
+private axiom test_sorry : ∀ {α}, α
+
+inductive Tyₛ (l : List Unit): Type
+| U : Tyₛ l
+open Tyₛ
+
+inductive Varₚ (d : Unit): List Unit → Type
+| vz : Varₚ d [d']
+| vs : Varₚ d l → Varₚ d (Bₛ :: l)
+
+inductive Tmₛ {l : List Unit}: Tyₛ l → Unit → Type 1
+| arr   : (T : Type) → Tmₛ A d → Tmₛ A d
+| param : Varₚ d l → Tmₛ A d → Tmₛ (@U l) d
+
+def TmₛA {l : List Unit} {d : Unit} (nonIndex : Bool) {Aₛ : Tyₛ l} (t : Tmₛ Aₛ d): Type :=
+match t with
+  | .arr dom cd =>
+    let cd := TmₛA nonIndex cd
+    dom → cd
+  | _ => test_sorry
+termination_by structural t