From 8b7411bdd83efe456d4158e8265e66699ebc33af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Dec 2021 06:50:20 -0800
Subject: [PATCH] feat: improve error location at well-founded recursion

---
 src/Lean/Elab/PreDefinition/WF/Fix.lean | 7 ++++++-
 tests/lean/wf2.lean                     | 6 ++++++
 tests/lean/wf2.lean.expected.out        | 3 +++
 3 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/wf2.lean
 create mode 100644 tests/lean/wf2.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 6cc1f7220c..f2c2e3bcf2 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Meta.Match.Match
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Cleanup
+import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 
@@ -44,7 +45,11 @@ private partial def replaceRecApps (recFnName : Name) (decrTactic? : Option Synt
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop F type) (← loop F val) fun x => do
         mkLetFVars #[x] (← loop F (body.instantiate1 x)) (usedLetOnly := false)
-    | Expr.mdata d e _   => return mkMData d (← loop F e)
+    | Expr.mdata d b _   =>
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop F b
+      else
+        return mkMData d (← loop F b)
     | Expr.proj n i e _  => return mkProj n i (← loop F e)
     | Expr.app _ _ _ =>
       let processApp (e : Expr) : TermElabM Expr :=
diff --git a/tests/lean/wf2.lean b/tests/lean/wf2.lean
new file mode 100644
index 0000000000..5aa8d18cad
--- /dev/null
+++ b/tests/lean/wf2.lean
@@ -0,0 +1,6 @@
+def g (x : Nat) (y : Nat) : Nat :=
+  if x < y then
+    2 * g (x-1) y -- Error here
+  else
+    0
+termination_by measure (·.1)
diff --git a/tests/lean/wf2.lean.expected.out b/tests/lean/wf2.lean.expected.out
new file mode 100644
index 0000000000..dcfdc188cb
--- /dev/null
+++ b/tests/lean/wf2.lean.expected.out
@@ -0,0 +1,3 @@
+wf2.lean:3:8-3:17: error: unsolved goals
+fst✝ snd✝ : Nat
+⊢ fst✝ - 1 < fst✝