fix: hasBadParamDep? to look at term, not type (#4672)

The previous check, looking only at the type of the parameter, was too
permissive and led to ill-typed terms later on.

This fixes #4671.

In some cases the previous code might have worked by accident, in this
sense this is a breaking change. Affected functions can be fixed by
reordering their parameters to that all the function parameters that
occur in the parameter of the inductive type of the parameter that the
function recurses on come first.

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

@@ -29,9 +29,8 @@ private def hasBadIndexDep? (ys : Array Expr) (indices : Array Expr) : MetaM (Op
 -- Inductive datatype parameters cannot depend on ys
 private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (Option (Expr × Expr)) := do
   for p in indParams do
-    let pType ← inferType p
     for y in ys do
-      if ← dependsOn pType y.fvarId! then
+      if ← dependsOn p y.fvarId! then
         return some (p, y)
   return none
 
@@ -75,7 +74,7 @@ def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo
         | none =>
           match (← hasBadParamDep? ys indParams) with
           | some (indParam, y) =>
-            throwError "its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}"
+            throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich does not come before the varying parameters and before the indices of the recursion parameter."
           | none =>
             let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
             k { fixedParams := fixedParams

tests/lean/run/issue4671.lean

@@ -0,0 +1,21 @@
+set_option linter.constructorNameAsVariable false
+
+inductive  A (n : Nat) : Type
+  | a : A n
+  | b : A n → A n
+
+/--
+error: argument #3 cannot be used for structural recursion
+  its type is an inductive datatype
+    A n
+  and the datatype parameter
+    n
+  depends on the function parameter
+    n
+  which does not come before the varying parameters and before the indices of the recursion parameter.
+-/
+#guard_msgs in
+def A.size (acc n : Nat) : A n → Nat
+  | .a => acc
+  | .b a' => 1 + A.size (acc + 1) n a'
+termination_by structural a => a