fix: deal with params for inductive predicates.

src/Lean/Elab/PreDefinition/Structural.lean

@@ -479,7 +479,6 @@ private def mkIndPredBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value
       let lctx := lctx.erase F.fvarId!
       withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
       let main ← mkFreshExprSyntheticOpaqueMVar FType
-      trace[Elab.definition.structural] "asdf\n{←Meta.ppGoal main.mvarId!}"
       let below := below[0]
       let valueNew     ← replaceIndPredRecApps recFnName recArgInfo motive value
       let Farg         ← mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew

src/Lean/Meta/IndPredBelow.lean

@@ -381,8 +381,9 @@ where
 private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Name × Expr := do
   (←inferType xs[idx]).withApp fun type args => do
   let indName := type.constName!
-  let belowType := mkApp (mkConst (indName ++ `below) type.constLevels!) motive
-  let belowType := mkAppN belowType $ args.push xs[idx]
+  let indInfo ← getConstInfoInduct indName
+  let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]]
+  let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs
   (indName, belowType)
 
 partial def mkBelowMatcher
@@ -393,7 +394,7 @@ partial def mkBelowMatcher
   let mkMatcherInput ← getMkMatcherInputInContext matcherApp
   let (indName, belowType, motive, matchType) ← 
     forallBoundedTelescope mkMatcherInput.matchType mkMatcherInput.numDiscrs fun xs t => do
-    let (indName, belowType) ← IndPredBelow.belowType belowMotive xs idx
+    let (indName, belowType) ← belowType belowMotive xs idx
     let matchType ← 
       withLocalDeclD (←mkFreshUserName `h_below) belowType fun h_below => do
       mkForallFVars (xs.push h_below) t
@@ -417,7 +418,7 @@ partial def mkBelowMatcher
     trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}"
     newAlt
 
-  let matcherName := mkMatcherInput.matcherName ++ s!"below_{idx}"
+  let matcherName ← mkFreshUserName mkMatcherInput.matcherName
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{←lhs.patterns.mapM (·.toMessageData)}"
@@ -483,7 +484,7 @@ where
     | Pattern.var varId => 
       let var := mkFVar varId
       (←inferType var).withApp fun ind args => do
-      let tgtType := mkAppN (mkConst (ind.constName! ++ `below) ind.constLevels!) (#[belowMotive] ++ args ++ #[var])
+      let (_, tgtType) ← belowType belowMotive #[var] 0
       withLocalDeclD (←mkFreshUserName `h) tgtType fun h => do
       let localDecl ← getFVarLocalDecl h
       (#[localDecl], Pattern.var h.fvarId!)

tests/lean/run/structuralRec1.lean

@@ -135,7 +135,7 @@ def paux : PNat → PNat → PNat
  | PNat.succ x, y =>
    match pf x y with
    | PNat.zero => pf x y
-   | v => pf x v + 1
+   | v => PNat.succ (pf x v)
 
 theorem ex (x y : Nat) : f x y = aux x y := by
   cases x
@@ -168,10 +168,12 @@ theorem «nested recursion» : ∀ {n}, is_nat n → P n
 | _, is_nat.S is_nat.Z => F1
 | _, is_nat.S (is_nat.S h) => FS («nested recursion» h)
 
-theorem «nested recursion, inaccessible» : ∀ {n}, is_nat n → P n
-| _, .(is_nat.Z) => F0
-| _, is_nat.S .(is_nat.Z) => F1
-| _, is_nat.S (is_nat.S h) => FS («nested recursion, inaccessible» h)
+/-- forbidding this, because it shouldn't exist in the first place.
+    We don't expect this kind of inconsistent inaccessible patterns. -/
+-- theorem «nested recursion, inaccessible» : ∀ {n}, is_nat n → P n
+-- | _, .(is_nat.Z) => F0
+-- | _, is_nat.S .(is_nat.Z) => F1
+-- | _, is_nat.S (is_nat.S h) => FS («nested recursion, inaccessible» h)
 
 theorem «reordered discriminants, type» : ∀ n, is_nat_T n → Nat → T n := fun n hn m => 
 match n, m, hn with
@@ -185,14 +187,15 @@ match n, m, hn with
 | _, _, is_nat.S is_nat.Z => F1
 | _, m, is_nat.S (is_nat.S h) => FS («reordered discriminants» _ h m)
 
-def «unsupported nesting» (xs : List Nat) : True :=
-  match xs with
-  | List.nil => True.intro
-  | y::ys =>
-    match ys with
-    | List.nil      => True.intro
-    | _::_::zs      => «unsupported nesting» zs 
-    | zs            => «unsupported nesting» ys 
+/-- known unsupported case for types, just here for reference. -/
+-- def «unsupported nesting» (xs : List Nat) : True :=
+--   match xs with
+--   | List.nil => True.intro
+--   | y::ys =>
+--     match ys with
+--     | List.nil      => True.intro
+--     | _::_::zs      => «unsupported nesting» zs 
+--     | zs            => «unsupported nesting» ys 
 
 def «unsupported nesting, predicate» (xs : PList Nat) : True :=
   match xs with