diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 6dac6b6655..cb05a6e7a0 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -314,9 +314,6 @@ end String
 
 namespace Substring
 
-@[inline] def bsize : Substring → Nat
-  | ⟨_, b, e⟩ => e - b
-
 @[inline] def isEmpty (ss : Substring) : Bool :=
   ss.bsize == 0
 
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 6620c850e8..45379961ce 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -148,12 +148,6 @@ partial def getTailInfo : Syntax → Option SourceInfo
   | node _ args   => args.findSomeRev? getTailInfo
   | _             => none
 
-partial def getTailPos : Syntax → Option String.Pos
-  | atom { pos := some pos, .. }  val    => some (pos + val.bsize)
-  | ident { pos := some pos, .. } val .. => some (pos + val.toString.bsize)
-  | node _ args                          => args.findSomeRev? getTailPos
-  | _                                    => none
-
 @[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
   if i == 0 then
     none
@@ -180,8 +174,8 @@ def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
 
 def unsetTrailing (stx : Syntax) : Syntax :=
   match stx.getTailInfo with
-  | none      => stx
-  | some info => stx.setTailInfo { info with trailing := none }
+  | SourceInfo.original lead pos trail => stx.setTailInfo (SourceInfo.original lead pos "".toSubstring)
+  | _                                  => stx
 
 @[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) (i : Nat) : Option (Array α) :=
   if h : i < a.size then
@@ -211,34 +205,10 @@ def setInfo (info : SourceInfo) : Syntax → Syntax
   | ident _ rawVal val pre => ident info rawVal val pre
   | stx                    => stx
 
-/--
-  Copy head and tail position information from `source` to `s`.
-  `leading` and `trailing` information is not preserved. -/
-def copyRangePos (s : Syntax) (source : Syntax) : Syntax :=
-  match source.getPos with
-  | none     => s
-  | some pos =>
-    let s := s.setHeadInfo { pos := pos }
-    match source.getTailInfo with
-    | some { pos := some pos, .. } =>
-      let s := s.setTailInfo { pos := pos }
-      /- The trailing token at `s` may be different from `source`.
-         So, we retrieve the tail positions and adjust `pos` to make sure the `s.getTailPos == source.getTailPos`. -/
-      match source.getTailPos, s.getTailPos with
-      | some pos₁, some pos₂ =>
-        if pos₁ < pos₂ then
-          s.setTailInfo { pos := some ((pos : Nat) - (pos₂ - pos₁) : Nat) }
-        else if pos₁ > pos₂ then
-          s.setTailInfo { pos := some ((pos : Nat) + (pos₁ - pos₂) : Nat) }
-        else
-          s
-      | _, _ => s
-    | _ => s
-
 /-- Return the first atom/identifier that has position information -/
 partial def getHead? : Syntax → Option Syntax
-  | stx@(atom { pos := some _, .. } ..)  => some stx
-  | stx@(ident { pos := some _, .. } ..) => some stx
+  | stx@(atom info ..)  => info.getPos.map fun _ => stx
+  | stx@(ident info ..) => info.getPos.map fun _ => stx
   | node _ args      => args.findSome? getHead?
   | _                => none
 
@@ -251,7 +221,7 @@ end Syntax
   | some ref => withRef ref x
 
 def mkAtom (val : String) : Syntax :=
-  Syntax.atom {} val
+  Syntax.atom SourceInfo.none val
 
 @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
   Syntax.node k args
@@ -277,8 +247,7 @@ partial def expandMacros : Syntax → MacroM Syntax
   Create an identifier copying the position from `src`.
   To refer to a specific constant, use `mkCIdentFrom` instead. -/
 def mkIdentFrom (src : Syntax) (val : Name) : Syntax :=
-  let pos := src.getPos
-  Syntax.ident { pos := pos } (toString val).toSubstring val []
+  Syntax.ident (SourceInfo.fromRef src) (toString val).toSubstring val []
 
 def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m Syntax := do
   return mkIdentFrom (← getRef) val
@@ -288,10 +257,9 @@ def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m Syntax := do
   This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally
   be captured. -/
 def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
-  let pos := src.getPos
   -- 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 { pos := pos } (toString id).toSubstring id [(c, [])]
+  Syntax.ident (SourceInfo.fromRef src) (toString id).toSubstring id [(c, [])]
 
 def mkCIdentFromRef [Monad m] [MonadRef m] (c : Name) : m Syntax := do
   return mkCIdentFrom (← getRef) c
@@ -301,7 +269,7 @@ def mkCIdent (c : Name) : Syntax :=
 
 @[export lean_mk_syntax_ident]
 def mkIdent (val : Name) : Syntax :=
-  Syntax.ident {} (toString val).toSubstring val []
+  Syntax.ident SourceInfo.none (toString val).toSubstring val []
 
 @[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
   Syntax.node nullKind args
@@ -348,17 +316,17 @@ def mkApp (fn : Syntax) : (args : Array Syntax) → Syntax
 def mkCApp (fn : Name) (args : Array Syntax) : Syntax :=
   mkApp (mkCIdent fn) args
 
-def mkLit (kind : SyntaxNodeKind) (val : String) (info : SourceInfo := {}) : Syntax :=
+def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : Syntax :=
   let atom : Syntax := Syntax.atom info val
   Syntax.node kind #[atom]
 
-def mkStrLit (val : String) (info : SourceInfo := {}) : Syntax :=
+def mkStrLit (val : String) (info := SourceInfo.none) : Syntax :=
   mkLit strLitKind (String.quote val) info
 
-def mkNumLit (val : String) (info : SourceInfo := {}) : Syntax :=
+def mkNumLit (val : String) (info := SourceInfo.none) : Syntax :=
   mkLit numLitKind val info
 
-def mkScientificLit (val : String) (info : SourceInfo := {}) : Syntax :=
+def mkScientificLit (val : String) (info := SourceInfo.none) : Syntax :=
   mkLit scientificLitKind val info
 
 /- Recall that we don't have special Syntax constructors for storing numeric and string atoms.
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 76354368af..695cedf122 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1015,6 +1015,9 @@ structure Substring where
   startPos : String.Pos
   stopPos : String.Pos
 
+@[inline] def Substring.bsize : Substring → Nat
+  | ⟨_, b, e⟩ => e.sub b
+
 def String.csize (c : Char) : Nat :=
   c.utf8Size.toNat
 
@@ -1582,19 +1585,31 @@ end Name
 
 /- 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 where
-  /- 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  : Option Substring  := none
-  pos      : Option String.Pos := none
-  trailing : Option Substring  := none
+/-- Source information of tokens. -/
+inductive SourceInfo where
+  /-
+    Token from original input with whitespace and position information.
+    `leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing,
+    it is not at all clear what the preceding token was, especially with backtracking. -/
+  | original (leading : Substring) (pos : String.Pos) (trailing : Substring)
+  /-
+    Synthesized token (e.g. from a quotation) annotated with a span from the original source.
+    In the delaborator, we "misuse" this constructor to store synthetic positions identifying
+    subterms. -/
+  | synthetic (pos : String.Pos) (endPos : String.Pos)
+  /- Synthesized token without position information. -/
+  | protected none
 
-instance : Inhabited SourceInfo := ⟨{}⟩
+instance : Inhabited SourceInfo := ⟨SourceInfo.none⟩
+
+namespace SourceInfo
+
+def getPos : SourceInfo → Option String.Pos
+  | original (pos := pos) ..  => some pos
+  | synthetic (pos := pos) .. => some pos
+  | SourceInfo.none           => none
+
+end SourceInfo
 
 abbrev SyntaxNodeKind := Name
 
@@ -1672,23 +1687,42 @@ def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
   | stx         => stx
 
 /-- Retrieve the left-most leaf's info in the Syntax tree. -/
-partial def getHeadInfo : Syntax → Option SourceInfo
+partial def getHeadInfo? : Syntax → Option SourceInfo
   | atom info _      => some info
   | ident info _ _ _ => some info
   | node _ args      =>
     let rec loop (i : Nat) : Option SourceInfo :=
       match decide (Less i args.size) with
-      | true => match getHeadInfo (args.get! i) with
+      | true => match getHeadInfo? (args.get! i) with
          | some info => some info
          | none      => loop (hAdd i 1)
       | false => none
     loop 0
   | _                => none
 
+/-- Retrieve the left-most leaf's info in the Syntax tree, or `none` if there is no token. -/
+partial def getHeadInfo (stx : Syntax) : SourceInfo :=
+  match stx.getHeadInfo? with
+  | some info => info
+  | none      => SourceInfo.none
+
 def getPos (stx : Syntax) : Option String.Pos :=
-  match stx.getHeadInfo with
-  | some info => info.pos
-  | _         => none
+  stx.getHeadInfo.getPos
+
+partial def getTailPos : Syntax → Option String.Pos
+  | atom (SourceInfo.original (pos := pos) ..) val     => some (pos.add val.bsize)
+  | atom (SourceInfo.synthetic (endPos := pos) ..) _   => some pos
+  | ident (SourceInfo.original (pos := pos) ..) val .. => some (pos.add val.bsize)
+  | ident (SourceInfo.synthetic (endPos := pos) ..) .. => some pos
+  | node _ args                                        =>
+    let rec loop (i : Nat) : Option String.Pos :=
+      match decide (Less i args.size) with
+      | true => match getTailPos (args.get! ((args.size.sub i).sub 1)) with
+         | some info => some info
+         | none      => loop (hAdd i 1)
+      | false => none
+    loop 0
+  | _                                                  => none
 
 /--
   An array of syntax elements interspersed with separators. Can be coerced to/from `Array Syntax` to automatically
@@ -1698,10 +1732,13 @@ structure SepArray (sep : String) where
 
 end Syntax
 
+def SourceInfo.fromRef (ref : Syntax) : SourceInfo :=
+  match ref.getPos, ref.getTailPos with
+  | some pos, some tailPos => SourceInfo.synthetic pos tailPos
+  | _,        _            => SourceInfo.none
+
 def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
-  match src.getHeadInfo with
-  | some info => Syntax.atom info val
-  | none      => Syntax.atom {} val
+  Syntax.atom src.getHeadInfo val
 
 /- Parser descriptions -/
 
@@ -1784,7 +1821,7 @@ class MonadQuotation (m : Type → Type) extends MonadRef m where
 export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 
 def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo := do
-  return { pos := (← getRef).getPos }
+  SourceInfo.fromRef (← getRef)
 
 instance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where
   getCurrMacroScope   := liftM (m := m) getCurrMacroScope
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 3c24d2f173..06d6f4e237 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -54,7 +54,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
           let quotedArg ← quoteAutoTactic arg
           quotedArgs ← `(Array.push $quotedArgs $quotedArg)
       `(Syntax.node $(quote k) $quotedArgs)
-  | Syntax.atom info val => `(Syntax.atom {} $(quote val))
+  | Syntax.atom info val => `(mkAtom $(quote val))
   | Syntax.missing       => unreachable!
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index cbccc354d3..85556c3c41 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -848,7 +848,7 @@ def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := withRef action <| wit
     let cond := action[1]
     `(assert! $cond; $k)
   else
-    let action := Syntax.copyRangePos (← `(($action : $((←read).m) PUnit))) action
+    let action ← withRef action `(($action : $((←read).m) PUnit))
     `(Bind.bind $action (fun (_ : PUnit) => $k))
 
 def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFreshMacroScope do
@@ -870,7 +870,7 @@ def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFr
       -- `doElem` must be a `doExpr action`. See `doLetArrowToCode`
       match isDoExpr? doElem with
       | some action =>
-        let action := Syntax.copyRangePos (← `(($action : $((← read).m) $type))) action
+        let action ← withRef action `(($action : $((← read).m) $type))
         `(Bind.bind $action (fun ($id:ident : $type) => $k))
       | none        => Macro.throwErrorAt decl "unexpected kind of 'do' declaration"
     else
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index c84d5c2ca0..51ef04a717 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1292,21 +1292,21 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
   `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
 def resolveName' (ident : Syntax) (explicitLevels : List Level) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   match ident with
-  | Syntax.ident { pos := pos?, .. } rawStr n preresolved =>
+  | Syntax.ident info rawStr n preresolved =>
     let r ← resolveName n preresolved explicitLevels
     r.mapM fun (c, fields) => do
       let (cSstr, fields) := fields.foldr (init := (rawStr, [])) fun field (restSstr, fs) =>
         let fieldSstr := restSstr.takeRightWhile (· ≠ '.')
         ({ restSstr with stopPos := restSstr.stopPos - (fieldSstr.bsize + 1) }, (field, fieldSstr) :: fs)
       let id := mkIdentFrom ident cSstr.toString
-      match pos? with
+      match info.getPos with
       | none =>
         return (c, id, fields.map fun (field, _) => mkIdentFrom ident (Name.mkSimple field))
       | some pos =>
         let mut pos := pos + cSstr.bsize + 1
         let mut newFields := #[]
         for (field, fieldSstr) in fields do
-          newFields := newFields.push <| Syntax.ident { pos := some pos } fieldSstr (Name.mkSimple field) []
+          newFields := newFields.push <| Syntax.ident (SourceInfo.original "".toSubstring pos "".toSubstring) fieldSstr (Name.mkSimple field) []
           pos := pos + fieldSstr.bsize + 1
         return (c, id, newFields.toList)
   | _ => throwError! "identifier expected"
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index e4cfa0ff1c..5567c5dfa5 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -723,11 +723,11 @@ private def rawAux (startPos : Nat) (trailingWs : Bool) : ParserFn := fun c s =>
     let s        := whitespace c s
     let stopPos' := s.pos
     let trailing := { str := input, startPos := stopPos, stopPos := stopPos' : Substring }
-    let atom     := mkAtom { leading := leading, pos := startPos, trailing := trailing } val
+    let atom     := mkAtom (SourceInfo.original leading startPos trailing) val
     s.pushSyntax atom
   else
     let trailing := mkEmptySubstringAt input stopPos
-    let atom     := mkAtom { leading := leading, pos := startPos, trailing := trailing } val
+    let atom     := mkAtom (SourceInfo.original leading startPos trailing) val
     s.pushSyntax atom
 
 /-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`. -/
@@ -782,7 +782,7 @@ def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : ParserFn := fun c s =>
   let s         := whitespace c s
   let wsStopPos := s.pos
   let trailing  := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }
-  let info      := { leading := leading, pos := startPos, trailing := trailing : SourceInfo }
+  let info      := SourceInfo.original leading startPos trailing
   s.pushSyntax (Syntax.mkLit n val info)
 
 def charLitFnAux (startPos : Nat) : ParserFn := fun c s =>
@@ -924,7 +924,7 @@ def mkTokenAndFixPos (startPos : Nat) (tk : Option Token) : ParserFn := fun c s
       let s         := whitespace c s
       let wsStopPos := s.pos
       let trailing  := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }
-      let atom      := mkAtom { leading := leading, pos := startPos, trailing := trailing } tk
+      let atom      := mkAtom (SourceInfo.original leading startPos trailing) tk
       s.pushSyntax atom
 
 def mkIdResult (startPos : Nat) (tk : Option Token) (val : Name) : ParserFn := fun c s =>
@@ -938,7 +938,7 @@ def mkIdResult (startPos : Nat) (tk : Option Token) (val : Name) : ParserFn := f
     let trailingStopPos := s.pos
     let leading         := mkEmptySubstringAt input startPos
     let trailing        := { str := input, startPos := stopPos, stopPos := trailingStopPos : Substring }
-    let info            := { leading := leading, trailing := trailing, pos := startPos : SourceInfo }
+    let info            := SourceInfo.original leading startPos trailing
     let atom            := mkIdent info rawVal val
     s.pushSyntax atom
 
@@ -1081,8 +1081,8 @@ def symbolInfo (sym : String) : ParserInfo := {
 
 def checkTailNoWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
-  | some { trailing := some trailing, .. } => trailing.stopPos == trailing.startPos
-  | _                                      => false
+  | some (SourceInfo.original _ _ trailing) => trailing.stopPos == trailing.startPos
+  | _                                       => false
 
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
     parsing local tokens that have not been added to the token table (but may have
@@ -1135,8 +1135,8 @@ partial def strAux (sym : String) (errorMsg : String) (j : Nat) :ParserFn :=
 
 def checkTailWs (prev : Syntax) : Bool :=
   match prev.getTailInfo with
-  | some { trailing := some trailing, .. } => trailing.stopPos > trailing.startPos
-  | _                                      => false
+  | some (SourceInfo.original _ _ trailing) => trailing.stopPos > trailing.startPos
+  | _                                       => false
 
 def checkWsBeforeFn (errorMsg : String) : ParserFn := fun c s =>
   let prev := s.stxStack.back
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index bb045607ad..031e14f58a 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -53,7 +53,7 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
     pure (stx, { pos := s.pos }, {})
 
 private def mkEOI (pos : String.Pos) : Syntax :=
-  let atom := mkAtom { pos := pos, trailing := "".toSubstring, leading := "".toSubstring } ""
+  let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring) ""
   Syntax.node `Lean.Parser.Module.eoi #[atom]
 
 def isEOI (s : Syntax) : Bool :=
diff --git a/src/Lean/Parser/Transform.lean b/src/Lean/Parser/Transform.lean
deleted file mode 100644
index ac07659474..0000000000
--- a/src/Lean/Parser/Transform.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
--/
-import Lean.Parser.Basic
-
-namespace Lean
-namespace Syntax
-
-def manyToSepBy (stx : Syntax) (sepTk : String) : Syntax := do
-  match stx with
-  | node k args =>
-    if args.size == 0 then
-      stx
-    else
-      let mut argsNew := #[args[0]]
-      for i in [1:args.size] do
-        let arg  := args[i]
-        let prev := argsNew.back
-        match prev.getTailInfo with
-        | some info =>
-          let prevArg := prev.setTailInfo { trailing := none }
-          argsNew := argsNew.set! (argsNew.size - 1) prev
-          argsNew := argsNew.push (atom info sepTk)
-          argsNew := argsNew.push arg
-        | none =>
-          argsNew := argsNew.push (atom {} sepTk)
-          argsNew := argsNew.push arg
-      node k argsNew
-  | stx => stx
-
-def removeParen (stx : Syntax) : Syntax :=
-  stx.ifNodeKind `Lean.Parser.Term.paren
-    (fun stx =>
-      let body := stx.getArg 1
-      if body.getNumArgs != 2 then stx.val
-      else if (body.getArg 1).isNone then
-        let body := body.getArg 0
-        match stx.getArg 2, body.getTailInfo with
-        | 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 { bodyInfo with trailing := bodyInfoTrail.toSubstring }
-        | _, _ => stx.val
-      else stx.val)
-    (fun _ => stx)
-
-end Syntax
-end Lean
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 706a3a9c9e..79582987a2 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -203,12 +203,12 @@ def withMDataExpr {α} (d : DelabM α) : DelabM α := do
   withReader ({ · with expr := e }) d
 
 partial def annotatePos (pos : Nat) : Syntax → Syntax
-  | stx@(Syntax.ident _ _ _ _)                   => stx.setInfo { pos := pos }
+  | stx@(Syntax.ident _ _ _ _)                   => stx.setInfo (SourceInfo.synthetic pos pos)
   -- app => annotate function
   | stx@(Syntax.node `Lean.Parser.Term.app args) => stx.modifyArg 0 (annotatePos pos)
   -- otherwise, annotate first direct child token if any
   | stx => match stx.getArgs.findIdx? Syntax.isAtom with
-    | some idx => stx.modifyArg idx (Syntax.setInfo { pos := pos })
+    | some idx => stx.modifyArg idx (Syntax.setInfo (SourceInfo.synthetic pos pos))
     | none     => stx
 
 def annotateCurPos (stx : Syntax) : Delab := do
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 5fc7711df0..31ae88dea0 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -260,8 +260,8 @@ def pushTokenCore (tk : String) : FormatterM Unit := do
     push tk.trimRight
 
 def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
-  match info.trailing with
-  | some ss =>
+  match info with
+  | SourceInfo.original _ _ ss =>
     -- preserve non-whitespace content (i.e. comments)
     let ss' := ss.trim
     if !ss'.isEmpty then
@@ -271,7 +271,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
       else
         push s!"  {ss'}"
       modify fun st => { st with leadWord := "" }
-  | none    => pure ()
+  | _ => pure ()
 
   let st ← get
   -- If there is no space between `tk` and the next word, see if we would parse more than `tk` as a single token
@@ -291,8 +291,8 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
     pushTokenCore tk
     modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
 
-  match info.leading with
-  | some ss =>
+  match info with
+  | SourceInfo.original ss _ _ =>
     -- preserve non-whitespace content (i.e. comments)
     let ss' := ss.trim
     if !ss'.isEmpty then
@@ -304,7 +304,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
       else
         push s!"{ss'} "
       modify fun st => { st with leadWord := "" }
-  | none    => pure ()
+  | _ => pure ()
 
 @[combinatorFormatter Lean.Parser.symbolNoAntiquot]
 def symbolNoAntiquot.formatter (sym : String) : Formatter := do
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 35c361b53f..2e295120f1 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -215,16 +215,19 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
       -- the original node, we must first move to the right, except if we already were at the left-most child in the first
       -- place.
       if idx > 0 then goRight
-      let stx ← getCur
-      match stx.getHeadInfo, stx.getTailInfo with
-      | some hi, some ti =>
-        -- Move leading/trailing whitespace of `stx` outside of parentheses
-        let stx := (stx.setHeadInfo { hi with leading := "".toSubstring }).setTailInfo { ti with trailing := "".toSubstring }
-        let stx := mkParen stx
-        let stx := (stx.setHeadInfo { hi with trailing := "".toSubstring }).setTailInfo { ti with leading := "".toSubstring }
-        setCur stx
-      | _, _ => setCur (mkParen stx)
-      let stx ← getCur; trace! `PrettyPrinter.parenthesize m!"parenthesized: {stx.formatStx none}"
+      let mut stx ← getCur
+      -- Move leading/trailing whitespace of `stx` outside of parentheses
+      if let SourceInfo.original _ pos trail := stx.getHeadInfo then
+        stx := stx.setHeadInfo (SourceInfo.original "".toSubstring pos trail)
+      if let SourceInfo.original lead pos _ := stx.getTailInfo then
+        stx := stx.setTailInfo (SourceInfo.original lead pos "".toSubstring)
+      let mut stx' := mkParen stx
+      if let SourceInfo.original lead pos _ := stx.getHeadInfo then
+        stx' := stx'.setHeadInfo (SourceInfo.original lead pos "".toSubstring)
+      if let SourceInfo.original _ pos trail := stx.getTailInfo then
+        stx' := stx'.setTailInfo (SourceInfo.original "".toSubstring pos trail)
+      trace! `PrettyPrinter.parenthesize m!"parenthesized: {stx'.formatStx none}"
+      setCur stx'
       goLeft
       -- after parenthesization, there is no more trailing parser
       modify (fun st => { st with contPrec := Parser.maxPrec, contCat := cat, trailPrec := none })
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 15353bcaa8..7f31153f44 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -431,7 +431,7 @@ section RequestHandling
         return #[]
 
   def rangeOfSyntax (text : FileMap) (stx : Syntax) : Range :=
-    ⟨text.utf8PosToLspPos <| stx.getHeadInfo.get!.pos.get!,
+    ⟨text.utf8PosToLspPos <| stx.getPos.get!,
      text.utf8PosToLspPos <| stx.getTailPos.get!⟩
 
   partial def handleDocumentSymbol (id : RequestID) (p : DocumentSymbolParams) :
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index e039865c62..ce84c2c15a 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -106,7 +106,7 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let (cmdStx, cmdParserState, msgLog) :=
     Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
-  let cmdPos := cmdStx.getHeadInfo.get!.pos.get! -- TODO(WN): always `some`?
+  let cmdPos := cmdStx.getPos.get!
   if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
     Sum.inr msgLog
   else
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 8906a27ac8..13fedc4c91 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -7,12 +7,10 @@ import Lean.Data.Name
 import Lean.Data.Format
 
 namespace Lean
-namespace SourceInfo
 
-def updateTrailing (info : SourceInfo) (trailing : Option Substring) : SourceInfo :=
-  { info with trailing := trailing }
-
-end SourceInfo
+def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
+  | SourceInfo.original leading pos _ => SourceInfo.original leading pos trailing
+  | info                              => info
 
 /- Syntax AST -/
 
@@ -119,8 +117,8 @@ def getIdAt (stx : Syntax) (i : Nat) : Name :=
   Id.run $ stx.rewriteBottomUpM fn
 
 private def updateInfo : SourceInfo → String.Pos → String.Pos → SourceInfo
-  | {leading := some lead, pos := some pos, trailing := some trail}, leadStart, trailStop =>
-    {leading := some { lead with startPos := leadStart }, pos := some pos, trailing := some { trail with stopPos := trailStop }}
+  | SourceInfo.original lead pos trail, leadStart, trailStop =>
+    SourceInfo.original { lead with startPos := leadStart } pos { trail with stopPos := trailStop }
   | info, _, _ => info
 
 private def chooseNiceTrailStop (trail : Substring) : String.Pos :=
@@ -130,12 +128,12 @@ trail.startPos + trail.posOf '\n'
    or the beginning of the String. -/
 @[inline]
 private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
-  | atom info@{trailing := some trail, ..} val => do
+  | atom info@(SourceInfo.original lead pos trail) val => do
     let trailStop := chooseNiceTrailStop trail
     let newInfo := updateInfo info (← get) trailStop
     set trailStop
     pure $ some (atom newInfo val)
-  | ident info@{trailing := some trail, ..} rawVal val pre   => do
+  | ident info@(SourceInfo.original lead pos trail) rawVal val pre => do
     let trailStop := chooseNiceTrailStop trail
     let newInfo := updateInfo info (← get) trailStop
     set trailStop
@@ -160,7 +158,7 @@ private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
 def updateLeading : Syntax → Syntax :=
   fun stx => (replaceM updateLeadingAux stx).run' 0
 
-partial def updateTrailing (trailing : Option Substring) : Syntax → Syntax
+partial def updateTrailing (trailing : 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)             =>
@@ -173,17 +171,19 @@ partial def updateTrailing (trailing : Option Substring) : Syntax → Syntax
   | s => s
 
 partial def getTailWithPos : Syntax → Option Syntax
-  | stx@(atom { pos := some _, .. } _)   => some stx
-  | stx@(ident { pos := some _, .. } ..) => some stx
-  | node _ args                          => args.findSomeRev? getTailWithPos
-  | _                                    => none
+  | stx@(atom info _)   => info.getPos.map fun _ => stx
+  | stx@(ident info ..) => info.getPos.map fun _ => stx
+  | node _ args         => args.findSomeRev? getTailWithPos
+  | _                   => none
 
 private def reprintLeaf (info : SourceInfo) (val : String) : String :=
+  match info with
+  | SourceInfo.original lead _ trail => s!"{lead}{val}{trail}"
   -- 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.
-  (Substring.toString <$> info.leading).getD " " ++ val ++ (Substring.toString <$> info.trailing).getD " "
+  | _                                => s!" {val} "
 
 partial def reprint : Syntax → Option String
   | atom info val           => reprintLeaf info val
@@ -203,13 +203,10 @@ partial def reprint : Syntax → Option String
 open Std.Format
 
 private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Format :=
-  if showInfo then
-    (match info.leading with | some ss => repr ss.toString ++ ":" | _ => "") ++
-    f ++
-    (match info.pos with | some pos => ":" ++ toString info.pos | _ => "") ++
-    (match info.trailing with | some ss => ":" ++ repr ss.toString | _ => "")
-  else
-    f
+  match showInfo, info with
+  | true, SourceInfo.original lead pos trail => f!"{lead}:{f}:{pos}:{trail}"
+  | true, SourceInfo.synthetic pos endPos    => f!"{pos}:{f}:{endPos}"
+  | _,    _                                  => f
 
 partial def formatStxAux (maxDepth : Option Nat) (showInfo : Bool) : Nat → Syntax → Format
   | _,     atom info val     => formatInfo showInfo info $ format (repr val)
@@ -323,9 +320,6 @@ namespace SyntaxNode
 
 end SyntaxNode
 
-def mkSimpleAtom (val : String) : Syntax :=
-  Syntax.atom {} val
-
 def mkListNode (args : Array Syntax) : Syntax :=
   Syntax.node nullKind args
 
diff --git a/stage0/src/library/compiler/ir_interpreter.cpp b/stage0/src/library/compiler/ir_interpreter.cpp
index d3e0c3037c..bf439c53e2 100644
--- a/stage0/src/library/compiler/ir_interpreter.cpp
+++ b/stage0/src/library/compiler/ir_interpreter.cpp
@@ -904,7 +904,7 @@ private:
     }
 public:
     explicit interpreter(environment const & env, options const & opts) : m_env(env), m_opts(opts) {
-        m_prefer_native = opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE);
+        m_prefer_native = true; //opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE);
     }
 
     ~interpreter() {
diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out
index 4ece2a454d..090cae994b 100644
--- a/tests/lean/276.lean.expected.out
+++ b/tests/lean/276.lean.expected.out
@@ -1,2 +1,2 @@
 fun {α} => PEmpty.rec.{v, u_1} fun x => α : {α : Sort v} → PEmpty.{u_1} → α
-276.lean:13:4-13:8: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion
+276.lean:13:4-13:15: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 94676f106f..8840cf8788 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -90,6 +90,6 @@ open Parser.Term
 #check (match · with | `([1, $ys,*, 2, $zs,*, 3]) => _)
 
 #eval run do
-  match Syntax.setHeadInfo (← `(fun x =>%$(Syntax.atom {pos := some 2} "") x)) { pos := some 1 } with
-  | `(fun%$i1 $x =>%$i2 $y) => pure #[i1.getHeadInfo >>= SourceInfo.pos, i2.getHeadInfo >>= SourceInfo.pos]
+  match Syntax.setHeadInfo (← `(fun x =>%$(Syntax.atom (SourceInfo.synthetic 2 2) "") x)) (SourceInfo.synthetic 1 1) with
+  | `(fun%$i1 $x =>%$i2 $y) => pure #[i1.getPos, i2.getPos]
   | _ => unreachable!
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index 1f3b715a16..11082146b6 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/tests/lean/doNotation1.lean.expected.out
@@ -9,11 +9,11 @@ doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type
   Bool
 but is expected to have type
   Nat
-doNotation1.lean:24:0-24:10: error: type mismatch, 'for' has type
+doNotation1.lean:24:0-25:11: error: type mismatch, 'for' has type
   PUnit
 but is expected to have type
   List Bool
-doNotation1.lean:28:0-28:10: error: type mismatch, 'for' has type
+doNotation1.lean:28:0-29:14: error: type mismatch, 'for' has type
   PUnit
 but is expected to have type
   List Nat
@@ -28,7 +28,7 @@ has type
   EIO IO.Error (IO.Ref Bool)
 but is expected to have type
   EIO IO.Error Unit
-doNotation1.lean:58:2-58:3: error: type mismatch, result value has type
+doNotation1.lean:58:2-58:20: error: type mismatch, result value has type
   Unit
 but is expected to have type
   Bool
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 312e927dfb..a4654baf13 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -7,7 +7,7 @@ while expanding
 while expanding
   if h : (x > 0) then 1 else 0
 macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
-macroStack.lean:17:0-17:1: error: failed to synthesize instance
+macroStack.lean:17:0-17:6: error: failed to synthesize instance
   HAdd Nat String ?m
 with resulting expansion
   HAdd.hAdd✝ (x + x✝) x✝¹
diff --git a/tests/lean/patvar.lean.expected.out b/tests/lean/patvar.lean.expected.out
index 488d1ab515..90c7ee6d11 100644
--- a/tests/lean/patvar.lean.expected.out
+++ b/tests/lean/patvar.lean.expected.out
@@ -1,6 +1,6 @@
-patvar.lean:3:0-3:5: error: missing cases:
+patvar.lean:3:0-3:22: error: missing cases:
 (List.cons _ _)
-patvar.lean:10:0-10:5: error: missing cases:
+patvar.lean:10:0-10:16: error: missing cases:
 (List.cons _ _)
 patvar.lean:14:0-14:21: error: invalid pattern variable, must be atomic
 patvar.lean:17:0-17:20: error: invalid pattern variable, must be atomic
diff --git a/tests/lean/run/CommandExtOverlap.lean b/tests/lean/run/CommandExtOverlap.lean
index 312a801efc..ed81eeaecf 100644
--- a/tests/lean/run/CommandExtOverlap.lean
+++ b/tests/lean/run/CommandExtOverlap.lean
@@ -4,7 +4,7 @@ open Lean
 
 macro_rules [mycheck]
 | `(#check $es,*) =>
-  let cmds := es.getElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[Syntax.atom {} "#check", e]
+  let cmds := es.getElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[mkAtom "#check", e]
   pure $ mkNullNode cmds
 
 #check true
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index 18ba96d65e..4f290d9c86 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -6,7 +6,9 @@ open Std.Format open Std
 
 def unparenAux (parens body : Syntax) : Syntax :=
 match parens.getHeadInfo, body.getHeadInfo, body.getTailInfo, parens.getTailInfo with
-| some bi', some bi, some ti, some ti' => (body.setHeadInfo { bi with leading := bi'.leading }).setTailInfo { ti with trailing := ti'.trailing }
+| SourceInfo.original lead _ _, SourceInfo.original _ pos trail,
+  SourceInfo.original endLead endPos _, SourceInfo.original _ _ endTrail =>
+    body.setHeadInfo (SourceInfo.original lead pos trail) |>.setTailInfo (SourceInfo.original endLead endPos endTrail)
 | _, _, _, _ => body
 
 partial def unparen : Syntax → Syntax
diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean
index 3aa2b5e82a..294708797e 100644
--- a/tests/lean/run/autoparam.lean
+++ b/tests/lean/run/autoparam.lean
@@ -1,5 +1,4 @@
 
-
 def f (x y : Nat) (h : x = y := by assumption) : Nat :=
 x + x
 
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index c3608f2d99..e163b8bc72 100644
--- a/tests/lean/run/tacticExtOverlap.lean
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -3,7 +3,7 @@ open Lean
 syntax (name := myintro) "intros" sepBy(ident, ",") : tactic
 
 macro_rules [myintro]
-| `(tactic| intros $x,*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom {} "intros", mkNullNode x]
+| `(tactic| intros $x,*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[mkAtom "intros", mkNullNode x]
 
 theorem tst1 {p q : Prop} : p → q → p :=
 by {
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 8b4f0ca213..c76e811b2a 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -6,7 +6,7 @@ structural recursion cannot be used
 well founded recursion has not been implemented yet
 sanitychecks.lean:4:8-5:9: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
 sanitychecks.lean:7:7-8:9: error: 'unsafe' theorems are not allowed
-sanitychecks.lean:10:0-10:9: error: failed to synthesize instance
+sanitychecks.lean:10:0-10:24: error: failed to synthesize instance
   Inhabited False
 sanitychecks.lean:18:0-18:40: error: failed to compile partial definition 'unsound3', failed to show that type is inhabited
 sanitychecks.lean:20:12-20:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
diff --git a/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out b/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out
index dfa6088833..e57e229688 100644
--- a/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out
+++ b/tests/lean/scopedInstanceOutsideNamespace.lean.expected.out
@@ -1,4 +1,4 @@
 scopedInstanceOutsideNamespace.lean:1:0-2:38: error: scoped attributes must be used inside namespaces
 "true"
-scopedInstanceOutsideNamespace.lean:6:0-6:3: error: scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:6:0-6:30: error: scoped attributes must be used inside namespaces
 scopedInstanceOutsideNamespace.lean:8:0-10:38: error: scoped attributes must be used inside namespaces
diff --git a/tests/lean/scopedMacros.lean.expected.out b/tests/lean/scopedMacros.lean.expected.out
index ea15a2e013..b8871076b2 100644
--- a/tests/lean/scopedMacros.lean.expected.out
+++ b/tests/lean/scopedMacros.lean.expected.out
@@ -2,5 +2,5 @@
 scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!'
 10 + 1 : Nat
 scopedMacros.lean:19:0-19:37: error: scoped attributes must be used inside namespaces
-scopedMacros.lean:19:0-19:7: error: invalid syntax node kind 'termBla!_'
+scopedMacros.lean:19:0-19:50: error: invalid syntax node kind 'termBla!_'
 scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!'