diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 03f42f5f00..cfb880690f 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -40,3 +40,4 @@ import Lean.Elab.Notation
 import Lean.Elab.Mixfix
 import Lean.Elab.MacroRules
 import Lean.Elab.BuiltinCommand
+import Lean.Elab.RecAppSyntax
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index da3744dc18..5b45bdeb1f 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -9,6 +9,7 @@ import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.Arg
+import Lean.Elab.RecAppSyntax
 
 namespace Lean.Elab.Term
 open Meta
@@ -913,7 +914,13 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
 @[builtinTermElab app] def elabApp : TermElab := fun stx expectedType? =>
   withoutPostponingUniverseConstraints do
     let (f, namedArgs, args, ellipsis) ← expandApp stx
-    elabAppAux f namedArgs args (ellipsis := ellipsis) expectedType?
+    let result ← elabAppAux f namedArgs args (ellipsis := ellipsis) expectedType?
+    let resultFn := result.getAppFn
+    if resultFn.isFVar then
+      let localDecl ← getLocalDecl resultFn.fvarId!
+      if localDecl.isAuxDecl then
+        return mkRecAppWithSyntax result stx
+    return result
 
 private def elabAtom : TermElab := fun stx expectedType? =>
   elabAppAux stx #[] #[] (ellipsis := false) expectedType?
diff --git a/src/Lean/Elab/RecAppSyntax.lean b/src/Lean/Elab/RecAppSyntax.lean
new file mode 100644
index 0000000000..ad742168b8
--- /dev/null
+++ b/src/Lean/Elab/RecAppSyntax.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Expr
+
+namespace Lean
+
+private def recAppKey := `_recApp
+
+/--
+  We store the syntax at recursive applications to be able to generate better error messages
+  when performing well-founded and structural recursion.
+-/
+def mkRecAppWithSyntax (e : Expr) (stx : Syntax) : Expr :=
+  mkMData (KVMap.empty.insert recAppKey (DataValue.ofSyntax stx)) e
+
+/--
+  Retrieve (if available) the syntax object attached to a recursive application.
+-/
+def getRecAppSyntax? (e : Expr) : Option Syntax :=
+  match e with
+  | Expr.mdata d b _ =>
+    match d.find recAppKey with
+    | some (DataValue.ofSyntax stx) => some stx
+    | _ => none
+  | _                => none
+
+end Lean
diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out
index 7f3018baed..e9c3090bdf 100644
--- a/tests/lean/interactive/863.lean.expected.out
+++ b/tests/lean/interactive/863.lean.expected.out
@@ -1,7 +1,14 @@
 {"textDocument": {"uri": "file://863.lean"},
  "position": {"line": 3, "character": 12}}
 {"items":
- [{"label": "getReducibilityStatus",
+ [{"label": "getRecAppSyntax?",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "Retrieve (if available) the syntax object attached to a recursive application.\n",
+    "kind": "markdown"},
+   "detail": "Expr → Option Syntax"},
+  {"label": "getReducibilityStatus",
    "kind": 3,
    "detail":
    "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
@@ -19,7 +26,14 @@
 {"textDocument": {"uri": "file://863.lean"},
  "position": {"line": 7, "character": 12}}
 {"items":
- [{"label": "getReducibilityStatus",
+ [{"label": "getRecAppSyntax?",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "Retrieve (if available) the syntax object attached to a recursive application.\n",
+    "kind": "markdown"},
+   "detail": "Expr → Option Syntax"},
+  {"label": "getReducibilityStatus",
    "kind": 3,
    "detail":
    "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},