diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index d30b40a304..872fd10620 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -89,8 +89,8 @@ def mkFreshUserName {m} [MonadLiftT CoreM m] (n : Name) : m Name :=
 
 @[inline] def CoreM.toIO {α} (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run ctx s).toIO') with
-  | Except.error (Exception.error _ msg) => do let e ← msg.toString; throw $ IO.userError e
-  | Except.error (Exception.internal id) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
+  | Except.error (Exception.error _ msg)   => do let e ← msg.toString; throw $ IO.userError e
+  | Except.error (Exception.internal id _) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
   | Except.ok a => pure a
 
 instance {α} [MetaEval α] : MetaEval (CoreM α) := {
@@ -112,14 +112,14 @@ export Core (CoreM mkFreshUserName)
   try
     x
   catch ex => match ex with
-    | Exception.error _ _    => throw ex
-    | Exception.internal id' => if id == id' then h ex else throw ex
+    | Exception.error _ _      => throw ex
+    | Exception.internal id' _ => if id == id' then h ex else throw ex
 
 @[inline] def catchInternalIds {α} {m : Type → Type} [Monad m] [MonadExcept Exception m] (ids : List InternalExceptionId) (x : m α) (h : Exception → m α) : m α := do
   try
     x
   catch ex => match ex with
-    | Exception.error _ _   => throw ex
-    | Exception.internal id => if ids.contains id then h ex else throw ex
+    | Exception.error _ _     => throw ex
+    | Exception.internal id _ => if ids.contains id then h ex else throw ex
 
 end Lean
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 915dbd2f27..457040d41d 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -561,7 +561,7 @@ private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExce
       | none       =>
         previousExceptions.forM fun ex => logException ex
         throw ex
-    | ex@(Exception.internal _) => throw ex
+    | ex@(Exception.internal _ _) => throw ex
 
 private def resolveLVal (e : Expr) (lval : LVal) : TermElabM (Expr × LValResolution) := do
   let eType ← inferType e
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 64079a535c..100b8347ab 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -205,8 +205,8 @@ instance : MonadRecDepth CommandElabM := {
   try
     x
   catch ex => match ex with
-    | Exception.error _ _   => logException ex
-    | Exception.internal id =>
+    | Exception.error _ _     => logException ex
+    | Exception.internal id _ =>
       if id == abortExceptionId then
         pure ()
       else
@@ -542,7 +542,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
       hasNoErrorMessages
     catch
       | ex@(Exception.error _ _) => do logException ex; pure false
-      | Exception.internal id    => do logError "internal"; pure false -- TODO: improve `logError "internal"`
+      | Exception.internal id _  => do logError "internal"; pure false -- TODO: improve `logError "internal"`
     finally
       restoreMessages prevMessages
   if succeeded then
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index 3f7e3a607b..592d97722c 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -65,7 +65,7 @@ def logInfo (msgData : MessageData) : m Unit :=
 def logException [MonadLiftT IO m] (ex : Exception) : m Unit := do
   match ex with
   | Exception.error ref msg => logErrorAt ref msg
-  | Exception.internal id   =>
+  | Exception.internal id _ =>
     unless id == abortExceptionId do
       let name ← id.getName
       logError ("internal exception: " ++ name)
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 157620f057..48f026366d 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -53,7 +53,7 @@ private def resumePostponed (macroStack : MacroStack) (declName? : Option Name)
         assignExprMVar mvarId result
         pure true
     catch
-     | ex@(Exception.internal id) =>
+     | ex@(Exception.internal id _) =>
        if id == postponeExceptionId then
          set s
          pure false
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 2695cc30fa..88f00ad68f 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -105,7 +105,7 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact
         match evalFns with
         | []      => throw ex
         | evalFns => s.restore; loop evalFns
-      | ex@(Exception.internal id) =>
+      | ex@(Exception.internal id _) =>
         if id == unsupportedSyntaxExceptionId then
           s.restore; loop evalFns
         else
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index bb6fe14269..6ba5a6eeb2 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -189,7 +189,7 @@ def getMessageLog : TermElabM MessageLog :=
       let sNew ← saveAllState
       s.restore
       pure (EStateM.Result.error ex sNew)
-    | ex@(Exception.internal id) =>
+    | ex@(Exception.internal id _) =>
       if id == postponeExceptionId then s.restore
       throw ex
 
@@ -844,7 +844,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
           exceptionToSorry ex expectedType?
         else
           throw ex
-      | Exception.internal id =>
+      | Exception.internal id _ =>
         if id == unsupportedSyntaxExceptionId then
           s.restore
           elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 42f027d1ff..988459a132 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -13,15 +13,15 @@ namespace Lean
 /- Exception type used in most Lean monads -/
 inductive Exception :=
   | error (ref : Syntax) (msg : MessageData)
-  | internal (id : InternalExceptionId)
+  | internal (id : InternalExceptionId) (extra : KVMap := {})
 
 def Exception.toMessageData : Exception → MessageData
-  | Exception.error _ msg => msg
-  | Exception.internal id => id.toString
+  | Exception.error _ msg   => msg
+  | Exception.internal id _ => id.toString
 
 def Exception.getRef : Exception → Syntax
-  | Exception.error ref _ => ref
-  | Exception.internal _  => Syntax.missing
+  | Exception.error ref _   => ref
+  | Exception.internal _  _ => Syntax.missing
 
 instance : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩