diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 5cf447b65c..80fa360fb4 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -139,8 +139,7 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
   | none     => s
   | some pos =>
     let pos := if delta then c.input.next pos else pos
-    match s with
-    | ⟨stack, lhsPrec, _, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { unexpected := msg }⟩
+    s.mkUnexpectedErrorAt msg pos
 
 /-- Generate an error at the position saved with the `withPosition` combinator.
    If `delta == true`, then it reports at saved position+1.
diff --git a/src/Lean/Parser/StrInterpolation.lean b/src/Lean/Parser/StrInterpolation.lean
index 2a8ac5815a..421a22341a 100644
--- a/src/Lean/Parser/StrInterpolation.lean
+++ b/src/Lean/Parser/StrInterpolation.lean
@@ -15,9 +15,8 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
   let rec parse (startPos : String.Pos) (c : ParserContext) (s : ParserState) : ParserState :=
     let i     := s.pos
     if input.atEnd i then
-      let s := s.pushSyntax Syntax.missing
-      let s := s.mkNode interpolatedStrKind stackSize
-      s.setError "unterminated string literal"
+      let s := s.mkError "unterminated string literal"
+      s.mkNode interpolatedStrKind stackSize
     else
       let curr := input.get i
       let s    := s.setPos (input.next i)
@@ -37,9 +36,8 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
             let s := s.setPos (input.next i)
             parse i c s
           else
-            let s := s.pushSyntax Syntax.missing
-            let s := s.mkNode interpolatedStrKind stackSize
-            s.setError "'}'"
+            let s := s.mkError "'}'"
+            s.mkNode interpolatedStrKind stackSize
       else
         parse startPos c s
   let startPos := s.pos
diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean
index be0aff2186..a57f42c604 100644
--- a/src/Lean/Parser/Types.lean
+++ b/src/Lean/Parser/Types.lean
@@ -259,34 +259,33 @@ def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : P
     let stack   := stack.push newNode
     ⟨stack, lhsPrec, pos, cache, err⟩
 
-def setError (s : ParserState) (msg : String) : ParserState :=
+@[inline]
+def setError (s : ParserState) (e : Error) : ParserState :=
   match s with
-  | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
+  | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack, lhsPrec, pos, cache, some e⟩
 
 def mkError (s : ParserState) (msg : String) : ParserState :=
-  match s with
-  | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
+  s.setError { expected := [msg] } |>.pushSyntax .missing
 
 def mkUnexpectedError (s : ParserState) (msg : String) (expected : List String := []) (pushMissing := true) : ParserState :=
-  match s with
-  | ⟨stack, lhsPrec, pos, cache, _⟩ => ⟨if pushMissing then stack.push .missing else stack, lhsPrec, pos, cache, some { unexpected := msg, expected := expected }⟩
+  let s := s.setError { unexpected := msg, expected }
+  if pushMissing then s.pushSyntax .missing else s
 
 def mkEOIError (s : ParserState) (expected : List String := []) : ParserState :=
   s.mkUnexpectedError "unexpected end of input" expected
 
-def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState :=
-  match s,  initStackSz? with
-  | ⟨stack, lhsPrec, _, cache, _⟩, none    => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
-  | ⟨stack, lhsPrec, _, cache, _⟩, some sz => ⟨stack.shrink sz |>.push Syntax.missing, lhsPrec, pos, cache, some { expected := [ msg ] }⟩
+def mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState := Id.run do
+  let mut s := s.setPos pos
+  if let some sz := initStackSz? then
+    s := s.shrinkStack sz
+  s := s.setError { expected := ex }
+  s.pushSyntax .missing
 
-def mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState :=
-  match s, initStackSz? with
-  | ⟨stack, lhsPrec, _, cache, _⟩, none    => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { expected := ex }⟩
-  | ⟨stack, lhsPrec, _, cache, _⟩, some sz => ⟨stack.shrink sz |>.push Syntax.missing, lhsPrec, pos, cache, some { expected := ex }⟩
+def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState :=
+  s.mkErrorsAt [msg] pos initStackSz?
 
 def mkUnexpectedErrorAt (s : ParserState) (msg : String) (pos : String.Pos) : ParserState :=
-  match s with
-  | ⟨stack, lhsPrec, _, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { unexpected := msg }⟩
+  s.setPos pos |>.mkUnexpectedError msg
 
 end ParserState