diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 482a465a12..a7df90b09e 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2042,8 +2042,15 @@ inductive Exception where
   | error             : Syntax → String → Exception
   | unsupportedSyntax : Exception
 
+constant State.ExtraPointed : PointedType.{0}
+
+def State.Extra : Type := State.ExtraPointed.type
+instance : Inhabited State.Extra where
+  default := State.ExtraPointed.val
+
 structure State where
   macroScope : MacroScope
+  extra      : State.Extra
   deriving Inhabited
 
 end Macro
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 49c03988a8..fae2cf8a63 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -161,7 +161,8 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
             currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
             mainModule     := env.mainModule,
             currRecDepth   := ← MonadRecDepth.getRecDepth,
-            maxRecDepth    := ← MonadRecDepth.getMaxRecDepth } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
+            maxRecDepth    := ← MonadRecDepth.getMaxRecDepth }
+          { macroScope := (← MonadMacroAdapter.getNextMacroScope), extra := arbitrary } with
   | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
   | EStateM.Result.error (Macro.Exception.error ref msg) _   => throwErrorAt ref msg
   | EStateM.Result.ok a  s                                   => MonadMacroAdapter.setNextMacroScope s.macroScope; pure a