diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 9770fc54f1..bf8137b623 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/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
diff --git a/tests/lean/run/issue4671.lean b/tests/lean/run/issue4671.lean
new file mode 100644
index 0000000000..3c31c94e9c
--- /dev/null
+++ b/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