feat: Better error location in structural recursion (#2819)

previously, only the WellFounded code was making use of the error
location in the RecApp-metadata. We can do the same for structural
recursion. This way,
```
def f (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => f (n + 1)
```
will show the error with squiggly lines under `f (n + 1)`, and not at
`def f`.

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -113,12 +113,12 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop below type) (← loop below val) fun x => do
         mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
-    | Expr.mdata d b     =>
-      if let some _ := getRecAppSyntax? e then
-        loop below b
+    | Expr.mdata d b =>
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop below b
       else
         return mkMData d (← loop below b)
-    | Expr.proj n i e    => return mkProj n i (← loop below e)
+    | Expr.proj n i e => return mkProj n i (← loop below e)
     | Expr.app _ _ =>
       let processApp (e : Expr) : StateRefT (HasConstCache recFnName) M Expr :=
         e.withApp fun f args => do

src/Lean/Elab/PreDefinition/Structural/IndPred.lean

@@ -23,7 +23,11 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop type) (← loop val) fun x => do
         mkLetFVars #[x] (← loop (body.instantiate1 x))
-    | Expr.mdata d e     => return mkMData d (← loop e)
+    | Expr.mdata d b => do
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop b
+      else
+        return mkMData d (← loop b)
     | Expr.proj n i e    => return mkProj n i (← loop e)
     | Expr.app _ _ =>
       let processApp (e : Expr) : M Expr := do

tests/lean/terminationFailure.lean.expected.out

@@ -9,7 +9,7 @@ f (x : Nat) : Nat
 f.g (a✝ : Nat) : Nat
 1
 2
-terminationFailure.lean:20:4-20:5: error: fail to show termination for
+terminationFailure.lean:24:9-24:12: error: fail to show termination for
   h
 with errors
 argument #1 was not used for structural recursion

tests/lean/wf1.lean.expected.out

@@ -1,4 +1,4 @@
-wf1.lean:1:4-1:5: error: fail to show termination for
+wf1.lean:3:12-3:19: error: fail to show termination for
   g
 with errors
 argument #1 was not used for structural recursion