fix: structural nested recursion confused when nested type appears fi…

…rst (#5766)

this fixes #5726

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

@@ -212,21 +212,21 @@ def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
 /--
 Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
 The `value` is the function with (only) the fixed parameters moved into the context,
-The `type` is the expected type of the argument.
+The `FType` is the expected type of the argument.
 The `recArgInfos` is used to transform the body of the function to replace recursive calls with
 uses of the `below` induction hypothesis.
 -/
 def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
     (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
   lambdaTelescope value fun xs value => do
-    let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
-    let FType ← instantiateForall FType indexMajorArgs
+    let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
+    let FType ← instantiateForall FType indicesMajorArgs
     forallBoundedTelescope FType (some 1) fun below _ => do
       -- TODO: `below` user name is `f`, and it will make a global `f` to be pretty printed as `_root_.f` in error messages.
       -- We should add an option to `forallBoundedTelescope` to ensure fresh names are used.
       let below := below[0]!
-      let valueNew   ← replaceRecApps recArgInfos positions below value
-      mkLambdaFVars (indexMajorArgs ++ #[below] ++ otherArgs) valueNew
+      let valueNew ← replaceRecApps recArgInfos positions below value
+      mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
 
 /--
 Given the `motives`, figures out whether to use `.brecOn` or `.binductionOn`, pass
@@ -264,7 +264,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
     (brecOnConst : Nat → Expr) : MetaM (Array Expr) := do
   let numTypeFormers := positions.size
   let recArgInfo := recArgInfos[0]! -- pick an arbitrary one
-  let brecOn := brecOnConst 0
+  let brecOn := brecOnConst recArgInfo.indIdx
   check brecOn
   let brecOnType ← inferType brecOn
   -- Skip the indices and major argument

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

@@ -77,7 +77,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       if !indIndices.all Expr.isFVar then
         throwError "its type {indInfo.name} is an inductive family and indices are not variables{indentExpr xType}"
       else if !indIndices.allDiff then
-        throwError " its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+        throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}"
       else
         let indexMinPos := getIndexMinPos xs indIndices
         let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed

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

@@ -107,17 +107,17 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
     check valueNew
     return #[{ preDef with value := valueNew }]
 
-  -- Sort the (indices of the) definitions by their position in indInfo.all
+  -- Groups the (indices of the) definitions by their position in indInfo.all
   let positions : Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers)
-  trace[Elab.definition.structural] "positions: {positions}"
+  trace[Elab.definition.structural] "assignments of type formers of {indInfo.name} to functions: {positions}"
 
   -- Construct the common `.brecOn` arguments
   let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
   trace[Elab.definition.structural] "motives: {motives}"
   let brecOnConst ← mkBRecOnConst recArgInfos positions motives
   let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
   trace[Elab.definition.structural] "FTypes: {FTypes}"
-  let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
+  let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
     mkBRecOnF recArgInfos positions r v t
   trace[Elab.definition.structural] "FArgs: {FArgs}"
   -- Assemble the individual `.brecOn` applications

src/Lean/Meta/InferType.lean

@@ -441,6 +441,8 @@ This can be used to infer the expected type of the alternatives when constructin
 -/
 def arrowDomainsN (n : Nat) (type : Expr) : MetaM (Array Expr) := do
   forallBoundedTelescope type n fun xs _ => do
+    unless xs.size = n do
+      throwError "type {type} does not have {n} parameters"
     let types ← xs.mapM (inferType ·)
     for t in types do
       if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then

tests/lean/run/issue5726.lean

@@ -0,0 +1,14 @@
+inductive Vec (α : Type) : Nat → Type where
+  | nil : Vec α 0
+  | cons : ∀ {n}, α → Vec α n → Vec α (n + 1)
+
+inductive Tree : Type where
+  | branch : ∀ {n}, Vec (Option Tree) n → Tree
+
+theorem die : Tree → True
+  | .branch v =>
+    let rec loop {n} : Vec (Option Tree) n → True
+    | .nil => ⟨⟩
+    | .cons none _ => ⟨⟩
+    | .cons (some t) _ => die t
+    loop v