From 5bbc54429f15bba66a7447c887a2e2899aba7823 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 22 Feb 2024 17:39:26 +0100
Subject: [PATCH] fix: improve error message when termination argument is too
 dependent (#3414)

this may help users when they face #2260

fixes #2260
---
 src/Lean/Elab/PreDefinition/WF/Rel.lean |  7 ++++++
 tests/lean/issue2260.lean               | 32 +++++++++++++++++++++++++
 tests/lean/issue2260.lean.expected.out  | 15 ++++++++++++
 3 files changed, 54 insertions(+)
 create mode 100644 tests/lean/issue2260.lean
 create mode 100644 tests/lean/issue2260.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 37bd29d768..8427d3efb0 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -68,7 +68,14 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
     for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
       let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
       mvarId.withContext do
+        let errorMsgHeader? := if preDefs.size > 1 then
+          "The termination argument types differ for the different functions, or depend on the " ++
+          "function's varying parameters. Try using `sizeOf` explicitly:\nThe termination argument"
+        else
+          "The termination argument depends on the function's varying parameters. Try using " ++
+          "`sizeOf` explicitly:\nThe termination argument"
         let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
+            (errorMsgHeader? := errorMsgHeader?)
         mvarId.assign value
     let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
     wfRelMVarId.assign wfRelVal
diff --git a/tests/lean/issue2260.lean b/tests/lean/issue2260.lean
new file mode 100644
index 0000000000..5e7b4c732e
--- /dev/null
+++ b/tests/lean/issue2260.lean
@@ -0,0 +1,32 @@
+inductive DNat : Nat → Type
+  | zero : DNat 0
+  | succ : DNat n → DNat (n+1)
+
+def foo : DNat i → Nat
+  | .zero => 0
+  | .succ n => foo n
+termination_by n => n
+
+
+mutual
+def bar1 : DNat i → Nat
+  | .zero => 0
+  | .succ n => bar2 n
+termination_by n => n
+def bar2 : DNat i → Nat
+  | .zero => 0
+  | .succ n => bar1 n
+termination_by n => n
+end
+
+
+mutual
+def baz1 : DNat i → Nat
+  | .zero => 0
+  | .succ n => baz2 n
+termination_by n => sizeOf n
+def baz2 : DNat i → Nat
+  | .zero => 0
+  | .succ n => baz1 n
+termination_by n => n
+end
diff --git a/tests/lean/issue2260.lean.expected.out b/tests/lean/issue2260.lean.expected.out
new file mode 100644
index 0000000000..66e493b51c
--- /dev/null
+++ b/tests/lean/issue2260.lean.expected.out
@@ -0,0 +1,15 @@
+issue2260.lean:8:20-8:21: error: The termination argument depends on the function's varying parameters. Try using `sizeOf` explicitly:
+The termination argument has type
+  DNat i : Type
+but is expected to have type
+  ?β : Sort ?u
+issue2260.lean:15:20-15:21: error: The termination argument types differ for the different functions, or depend on the function's varying parameters. Try using `sizeOf` explicitly:
+The termination argument has type
+  DNat i : Type
+but is expected to have type
+  ?β : Sort ?u
+issue2260.lean:31:20-31:21: error: The termination argument types differ for the different functions, or depend on the function's varying parameters. Try using `sizeOf` explicitly:
+The termination argument has type
+  DNat i : Type
+but is expected to have type
+  Nat : Type