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

@@ -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

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

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