fix: hasBadParamDep? to look at term, not type

fixes #4671

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
 

tests/lean/run/issue4671.lean

@@ -0,0 +1,20 @@
+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 parameter
+    n
+  depends on
+    n
+-/
+#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