feat: improve error location at well-founded recursion

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 :=

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)

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✝