diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index cc28a5b85b..b4db28b40f 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -168,7 +168,12 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
             maxRecDepth    := ← MonadRecDepth.getMaxRecDepth
           } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
   | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
-  | EStateM.Result.error (Macro.Exception.error ref msg) _   => throwErrorAt ref msg
+  | EStateM.Result.error (Macro.Exception.error ref msg) _   =>
+    if msg == maxRecDepthErrorMessage then
+      -- Make sure we can detect exception using `Exception.isMaxRecDepth`
+      throwMaxRecDepthAt ref
+    else
+      throwErrorAt ref msg
   | EStateM.Result.ok a  s                                   =>
     MonadMacroAdapter.setNextMacroScope s.macroScope
     s.traceMsgs.reverse.forM fun (clsName, msg) => trace clsName fun _ => msg
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index ee1d815b6b..0013edaa44 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -81,11 +81,26 @@ instance [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
 instance [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
   inferInstanceAs (MonadRecDepth (StateRefT' _ _ _))
 
+def throwMaxRecDepthAt [MonadError m] (ref : Syntax) : m α :=
+  throw <| Exception.error ref (MessageData.ofFormat (Std.Format.text maxRecDepthErrorMessage))
+
+/--
+  Return true if `ex` was generated by `throwMaxRecDepthAt`.
+  This function is a bit hackish. The max rec depth exception should probably be an internal exception,
+  but it is also produced by `MacroM` which implemented in the prelude, and internal exceptions have not
+  been defined yet. -/
+def Exception.isMaxRecDepth (ex : Exception) : Bool :=
+  match ex with
+  | error _ (MessageData.ofFormat (Std.Format.text msg)) => msg == maxRecDepthErrorMessage
+  | _ => false
+
 @[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if curr == max then Lean.throwError maxRecDepthErrorMessage
-  MonadRecDepth.withRecDepth (curr+1) x
+  if curr == max then
+    throwMaxRecDepthAt (← getRef)
+  else
+    MonadRecDepth.withRecDepth (curr+1) x
 
 syntax "throwError " (interpolatedStr(term) <|> term) : term
 syntax "throwErrorAt " term:max (interpolatedStr(term) <|> term) : term