diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index 026b8f2b5b..28d04bb589 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -335,7 +335,7 @@ else
 def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.identPrec then
-  let info := stx.getHeadInfo;
+  let info := stx.getHeadInfo.getD {};
   let id   := (stx.getArg 0).getId;
   pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1]
 else
diff --git a/src/Init/Lean/Elab/SyntheticMVars.lean b/src/Init/Lean/Elab/SyntheticMVars.lean
index 5f0e7f684e..b6892360e9 100644
--- a/src/Init/Lean/Elab/SyntheticMVars.lean
+++ b/src/Init/Lean/Elab/SyntheticMVars.lean
@@ -27,7 +27,7 @@ when val.hasExprMVar $ throwError ref ("tactic failed, result still contain meta
 def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
 modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };
 remainingGoals ← liftTacticElabM ref mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
-let tailRef := ref.getTailWithInfo.getD ref;
+let tailRef := ref.getTailWithPos.getD ref;
 unless remainingGoals.isEmpty (reportUnsolvedGoals tailRef remainingGoals);
 ensureAssignmentHasNoMVars tailRef mvarId
 
diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 4f7b361dbd..5682cc0aea 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -20,7 +20,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
 MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
 
 def Term.reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TermElabM Unit :=
-let tailRef := ref.getTailWithInfo.getD ref;
+let tailRef := ref.getTailWithPos.getD ref;
 Term.throwError tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
 
 namespace Tactic
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 78723126fa..c28371f5f3 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -23,7 +23,7 @@ abbrev mkAtom (info : SourceInfo) (val : String) : Syntax :=
 Syntax.atom info val
 
 abbrev mkIdent (info : SourceInfo) (rawVal : Substring) (val : Name) : Syntax :=
-Syntax.ident (some info) rawVal val []
+Syntax.ident info rawVal val []
 
 /- Return character after position `pos` -/
 def getNext (input : String) (pos : Nat) : Char :=
@@ -639,7 +639,7 @@ let s         := whitespace c s;
 let wsStopPos := s.pos;
 let trailing  := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos };
 let info      := { SourceInfo . leading := leading, pos := startPos, trailing := trailing };
-s.pushSyntax (mkStxLit n val (some info))
+s.pushSyntax (mkStxLit n val info)
 
 def charLitFnAux (startPos : Nat) : ParserFn
 | c, s =>
@@ -973,8 +973,8 @@ partial def strAux (sym : String) (errorMsg : String) : Nat → ParserFn
 
 def checkTailWs (prev : Syntax) : Bool :=
 match prev.getTailInfo with
-| some info => info.trailing.stopPos > info.trailing.startPos
-| none      => false
+| some { trailing := some trailing, .. } => trailing.stopPos > trailing.startPos
+| _                                      => false
 
 def checkWsBeforeFn (errorMsg : String) : ParserFn :=
 fun c s =>
@@ -987,8 +987,8 @@ def checkWsBefore (errorMsg : String) : Parser :=
 
 def checkTailNoWs (prev : Syntax) : Bool :=
 match prev.getTailInfo with
-| some info => info.trailing.stopPos == info.trailing.startPos
-| none      => false
+| some { trailing := some trailing, .. } => trailing.stopPos == trailing.startPos
+| _                                      => false
 
 private def pickNonNone (stack : Array Syntax) : Syntax :=
 match stack.findRev? $ fun stx => !stx.isNone with
diff --git a/src/Init/Lean/Parser/Transform.lean b/src/Init/Lean/Parser/Transform.lean
index d0bf65ae25..275ed1aaa2 100644
--- a/src/Init/Lean/Parser/Transform.lean
+++ b/src/Init/Lean/Parser/Transform.lean
@@ -15,12 +15,12 @@ match stx with
     let prevArg := newArgs.back;
     match prevArg.getTailInfo with
     | some info =>
-      let prevArg := prevArg.setTailInfo info.truncateTrailing;
+      let prevArg := prevArg.setTailInfo { trailing := none };
       let newArgs := newArgs.set! (newArgs.size - 1) prevArg;
       let newArgs := newArgs.push (atom info sepTk);
       newArgs.push arg
     | none =>
-      let newArgs := newArgs.push (atom none sepTk);
+      let newArgs := newArgs.push (atom {} sepTk);
       newArgs.push arg)
     #[args.get! 0]
     1;
@@ -35,10 +35,10 @@ stx.ifNodeKind `Lean.Parser.Term.paren
     else if (body.getArg 1).isNone then
       let body := body.getArg 0;
       match stx.getArg 2, body.getTailInfo with
-      | atom (some info) ")", some bodyInfo =>
-        let bodyInfoTrail := bodyInfo.trailing.toString ++ "  ";      -- add whithespaces for removed parentheses
-        let bodyInfoTrail := bodyInfoTrail ++ info.trailing.toString; -- add close paren trailing spaces
-        body.setTailInfo (some { trailing := bodyInfoTrail.toSubstring, .. bodyInfo })
+      | atom { trailing := some outer } ")", some bodyInfo@{ trailing := some inner } =>
+        let bodyInfoTrail := inner.toString ++ "  ";  -- add whithespaces for removed parentheses
+        let bodyInfoTrail := bodyInfoTrail ++ outer.toString; -- add close paren trailing spaces
+        body.setTailInfo { trailing := bodyInfoTrail.toSubstring, .. bodyInfo }
       | _, _ => stx.val
     else stx.val)
   (fun _ => stx)
diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index a2dd0f8f36..6353100763 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -11,20 +11,9 @@ import Init.Lean.Data.Format
 namespace Lean
 namespace SourceInfo
 
-def updateTrailing (info : SourceInfo) (trailing : Substring) : SourceInfo :=
+def updateTrailing (info : SourceInfo) (trailing : Option Substring) : SourceInfo :=
 { trailing := trailing, .. info }
 
-def truncateTrailing (info : SourceInfo) : SourceInfo :=
-{ trailing := { stopPos := info.trailing.startPos, .. info.trailing }, .. info }
-
-/- Update `info₁.trailing.stopPos` to `info₂.trailing.stopPos` -/
-def appendToTrailing (info₁ info₂ : SourceInfo) : SourceInfo :=
-{ trailing := { stopPos := info₂.trailing.stopPos, .. info₁.trailing }, .. info₁ }
-
-/- Update `info₁.leading.startPos` to `info₂.leading.startPos` -/
-def appendToLeading (info₁ info₂ : SourceInfo) : SourceInfo :=
-{ leading := { startPos := info₂.leading.startPos, .. info₁.leading }, .. info₁ }
-
 end SourceInfo
 
 /- Syntax AST -/
@@ -140,23 +129,24 @@ def getIdAt (stx : Syntax) (i : Nat) : Name :=
 Id.run $ stx.mrewriteBottomUp fn
 
 private def updateInfo : SourceInfo → String.Pos → SourceInfo
-| {leading := {str := s, startPos := _, stopPos := _}, pos := pos, trailing := trailing}, last =>
-  {leading := {str := s, startPos := last, stopPos := pos}, pos := pos, trailing := trailing}
+| {leading := some {str := s, startPos := _, stopPos := _}, pos := some pos, trailing := trailing}, last =>
+  {leading := some {str := s, startPos := last, stopPos := pos}, pos := some pos, trailing := trailing}
+| info, _ => info
 
 /- Remark: the State `String.Pos` is the `SourceInfo.trailing.stopPos` of the previous token,
    or the beginning of the String. -/
 @[inline]
 private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
-| atom (some info) val   => do
+| atom info@{trailing := some trail, ..} val => do
   last ← get;
-  set info.trailing.stopPos;
+  set trail.stopPos;
   let newInfo := updateInfo info last;
-  pure $ some (atom (some newInfo) val)
-| ident (some info) rawVal val pre   => do
+  pure $ some (atom newInfo val)
+| ident info@{trailing := some trail, ..} rawVal val pre   => do
   last ← get;
-  set info.trailing.stopPos;
+  set trail.stopPos;
   let newInfo := updateInfo info last;
-  pure $ some (ident (some newInfo) rawVal val pre)
+  pure $ some (ident newInfo rawVal val pre)
 | _ => pure none
 
 /-- Set `SourceInfo.leading` according to the trailing stop of the preceding token.
@@ -173,9 +163,9 @@ private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
 def updateLeading : Syntax → Syntax :=
 fun stx => (mreplace updateLeadingAux stx).run' 0
 
-partial def updateTrailing (trailing : Substring) : Syntax → Syntax
-| Syntax.atom (some info) val               => Syntax.atom (some (info.updateTrailing trailing)) val
-| Syntax.ident (some info) rawVal val pre   => Syntax.ident (some (info.updateTrailing trailing)) rawVal val pre
+partial def updateTrailing (trailing : Option Substring) : Syntax → Syntax
+| Syntax.atom info val               => Syntax.atom (info.updateTrailing trailing) val
+| Syntax.ident info rawVal val pre   => Syntax.ident (info.updateTrailing trailing) rawVal val pre
 | n@(Syntax.node k args)                    =>
   if args.size == 0 then n
   else
@@ -186,13 +176,13 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
 | s => s
 
 def getPos (stx : Syntax) : Option String.Pos :=
-SourceInfo.pos <$> stx.getHeadInfo
+stx.getHeadInfo >>= SourceInfo.pos
 
-partial def getTailWithInfo : Syntax → Option Syntax
-| stx@(atom (some _) _)      => some stx
-| stx@(ident (some _) _ _ _) => some stx
-| node _ args                => args.findSomeRev? getTailWithInfo
-| _                          => none
+partial def getTailWithPos : Syntax → Option Syntax
+| stx@(atom { pos := some _, .. } _)      => some stx
+| stx@(ident { pos := some _, .. } _ _ _) => some stx
+| node _ args                             => args.findSomeRev? getTailWithPos
+| _                                       => none
 
 partial def getTailInfo : Syntax → Option SourceInfo
 | atom info _      => info
@@ -210,7 +200,7 @@ partial def getTailInfo : Syntax → Option SourceInfo
     | some v => some $ a.set! i v
     | none   => updateLast i
 
-partial def setTailInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
+partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
 | atom _ val             => some $ atom info val
 | ident _ rawVal val pre => some $ ident info rawVal val pre
 | node k args            =>
@@ -219,7 +209,7 @@ partial def setTailInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
   | none      => none
 | stx                    => none
 
-def setTailInfo (stx : Syntax) (info : Option SourceInfo) : Syntax :=
+def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
 match setTailInfoAux info stx with
 | some stx => stx
 | none     => stx
@@ -227,7 +217,7 @@ match setTailInfoAux info stx with
 def truncateTrailing (stx : Syntax) : Syntax :=
 match stx.getTailInfo with
 | none      => stx
-| some info => stx.setTailInfo info.truncateTrailing
+| some info => stx.setTailInfo { info with trailing := none }
 
 @[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) : Nat → Option (Array α)
 | i =>
@@ -239,7 +229,7 @@ match stx.getTailInfo with
   else
     none
 
-partial def setHeadInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
+partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
 | atom _ val             => some $ atom info val
 | ident _ rawVal val pre => some $ ident info rawVal val pre
 | node k args            =>
@@ -248,7 +238,7 @@ partial def setHeadInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
   | noxne      => none
 | stx                    => none
 
-def setHeadInfo (stx : Syntax) (info : Option SourceInfo) : Syntax :=
+def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
 match setHeadInfoAux info stx with
 | some stx => stx
 | none     => stx
@@ -262,13 +252,12 @@ partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
 | node k args => node k $ args.map replaceInfo
 | stx         => setInfo info stx
 
-private def reprintLeaf : Option SourceInfo → String → String
+private def reprintLeaf (info : SourceInfo) (val : String) : String :=
 -- no source info => add gracious amounts of whitespace to definitely separate tokens
 -- Note that the proper pretty printer does not use this function.
 -- The parser as well always produces source info, so round-tripping is still
 -- guaranteed.
-| none,      val => " " ++ val ++ " "
-| some info, val => info.leading.toString ++ val ++ info.trailing.toString
+(Substring.toString <$> info.leading).getD " " ++ val ++ (Substring.toString <$> info.trailing).getD " "
 
 partial def reprint : Syntax → Option String
 | atom info val           => reprintLeaf info val
@@ -327,14 +316,14 @@ end SyntaxNode
 
 @[export lean_mk_syntax_atom]
 def mkSimpleAtom (val : String) : Syntax :=
-Syntax.atom none val
+Syntax.atom {} val
 
 @[export lean_mk_syntax_list]
 def mkListNode (args : Array Syntax) : Syntax :=
 Syntax.node nullKind args
 
 def mkAtom (val : String) : Syntax :=
-Syntax.atom none val
+Syntax.atom {} val
 
 @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
 Syntax.node k args
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 115a600aa8..e28600c9b3 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura and Sebastian Ullrich
 -/
 prelude
+import Init.Data.Option.BasicAux
 import Init.Data.String.Basic
 import Init.Data.Array.Basic
 import Init.Data.UInt
@@ -161,14 +162,19 @@ abbrev TrailingParserDescr := ParserDescr
 
 /- Syntax -/
 
+/--
+  Source information of syntax atoms. All information is generally set for unquoted syntax and unset for syntax in
+  syntax quotations, but syntax transformations might want to invalidate only one side to make the pretty printer
+  reformat it. In the special case of the delaborator, we also use purely synthetic position information without
+  whitespace information. -/
 structure SourceInfo :=
 /- Will be inferred after parsing by `Syntax.updateLeading`. During parsing,
    it is not at all clear what the preceding token was, especially with backtracking. -/
-(leading  : Substring)
-(pos      : String.Pos)
-(trailing : Substring)
+(leading  : Option Substring  := none)
+(pos      : Option String.Pos := none)
+(trailing : Option Substring  := none)
 
-instance SourceInfo.inhabited : Inhabited SourceInfo := ⟨⟨"".toSubstring, arbitrary _, "".toSubstring⟩⟩
+instance SourceInfo.inhabited : Inhabited SourceInfo := ⟨{}⟩
 
 abbrev SyntaxNodeKind := Name
 
@@ -177,8 +183,8 @@ abbrev SyntaxNodeKind := Name
 inductive Syntax
 | missing : Syntax
 | node   (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
-| atom   (info : Option SourceInfo) (val : String) : Syntax
-| ident  (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
+| atom   (info : SourceInfo) (val : String) : Syntax
+| ident  (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
 
 instance Syntax.inhabited : Inhabited Syntax :=
 ⟨Syntax.missing⟩
@@ -412,7 +418,7 @@ abbrev Macro := Syntax → MacroM Syntax
   Create an identifier using `SourceInfo` from `src`.
   To refer to a specific constant, use `mkCIdentFrom` instead. -/
 def mkIdentFrom (src : Syntax) (val : Name) : Syntax :=
-let info := src.getHeadInfo;
+let info := src.getHeadInfo.getD {};
 Syntax.ident info (toString val).toSubstring val []
 
 /--
@@ -420,13 +426,13 @@ Syntax.ident info (toString val).toSubstring val []
   This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally
   be captured. -/
 def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
-let info := src.getHeadInfo;
+let info := src.getHeadInfo.getD {};
 -- Remark: We use the reserved macro scope to make sure there are no accidental collision with our frontend
 let id   := addMacroScope `_internal c reservedMacroScope;
 Syntax.ident info (toString id).toSubstring id [(c, [])]
 
 def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
-let info := src.getHeadInfo;
+let info := src.getHeadInfo.getD {};
 Syntax.atom info val
 
 def Syntax.identToAtom (stx : Syntax) : Syntax :=
@@ -436,7 +442,7 @@ match stx with
 
 @[export lean_mk_syntax_ident]
 def mkIdent (val : Name) : Syntax :=
-Syntax.ident none (toString val).toSubstring val []
+Syntax.ident {} (toString val).toSubstring val []
 
 @[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
 Syntax.node nullKind args
@@ -488,14 +494,14 @@ mkCTermIdFrom Syntax.missing c
 def mkCAppStx (fn : Name) (args : Array Syntax) : Syntax :=
 mkAppStx (mkCTermId fn) args
 
-def mkStxLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
+def mkStxLit (kind : SyntaxNodeKind) (val : String) (info : SourceInfo := {}) : Syntax :=
 let atom : Syntax := Syntax.atom info val;
 Syntax.node kind #[atom]
 
-def mkStxStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+def mkStxStrLit (val : String) (info : SourceInfo := {}) : Syntax :=
 mkStxLit strLitKind (repr val) info
 
-def mkStxNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+def mkStxNumLit (val : String) (info : SourceInfo := {}) : Syntax :=
 mkStxLit numLitKind val info
 
 namespace Syntax
@@ -696,7 +702,7 @@ match stx with
 def strLitToAtom (stx : Syntax) : Syntax :=
 match stx.isStrLit? with
 | none     => stx
-| some val => Syntax.atom stx.getHeadInfo val
+| some val => Syntax.atom stx.getHeadInfo.get! val
 
 def isAtom : Syntax → Bool
 | atom _ _ => true