From f36bbc8d56cf96d9137d8676d2899b91b4fe0992 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 7 Jul 2024 18:00:00 +0200
Subject: [PATCH] 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.
---
 .../PreDefinition/Structural/FindRecArg.lean  |  5 ++---
 tests/lean/run/issue4671.lean                 | 21 +++++++++++++++++++
 2 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/issue4671.lean

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