diff --git a/src/Init/Data/Format/Syntax.lean b/src/Init/Data/Format/Syntax.lean
index 14b035f9f2..2dd3ada2cf 100644
--- a/src/Init/Data/Format/Syntax.lean
+++ b/src/Init/Data/Format/Syntax.lean
@@ -23,7 +23,7 @@ partial def formatStxAux (maxDepth : Option Nat) (showInfo : Bool) : Nat → Syn
   | _,     atom info val     => formatInfo showInfo info $ format (repr val)
   | _,     ident info _ val pre => formatInfo showInfo info $ format "`" ++ format val
   | _,     missing           => "<missing>"
-  | depth, node kind args    =>
+  | depth, node _ kind args  =>
     let depth := depth + 1;
     if kind == nullKind then
       sbracket $
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 0f073c8008..29b98bcbbd 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -211,7 +211,7 @@ namespace Syntax
 
 partial def structEq : Syntax → Syntax → Bool
   | Syntax.missing, Syntax.missing => true
-  | Syntax.node k args, Syntax.node k' args' => k == k' && args.isEqv args' structEq
+  | Syntax.node _ k args, Syntax.node _ k' args' => k == k' && args.isEqv args' structEq
   | Syntax.atom _ val, Syntax.atom _ val' => val == val'
   | Syntax.ident _ rawVal val preresolved, Syntax.ident _ rawVal' val' preresolved' => rawVal == rawVal' && val == val' && preresolved == preresolved'
   | _, _ => false
@@ -221,7 +221,9 @@ instance : BEq Lean.Syntax := ⟨structEq⟩
 partial def getTailInfo? : Syntax → Option SourceInfo
   | atom info _   => info
   | ident info .. => info
-  | node _ args   => args.findSomeRev? getTailInfo?
+  | node SourceInfo.none _ args =>
+      args.findSomeRev? getTailInfo?
+  | node info _ args => info
   | _             => none
 
 def getTailInfo (stx : Syntax) : SourceInfo :=
@@ -245,9 +247,9 @@ def getTrailingSize (stx : Syntax) : Nat :=
 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            =>
+  | node info k args       =>
     match updateLast args (setTailInfoAux info) args.size with
-    | some args => some <| node k args
+    | some args => some <| node info k args
     | none      => none
   | stx                    => none
 
@@ -273,9 +275,9 @@ def unsetTrailing (stx : Syntax) : 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            =>
+  | node i k args          =>
     match updateFirst args (setHeadInfoAux info) 0 with
-    | some args => some <| node k args
+    | some args => some <| node i k args
     | noxne     => none
   | stx                    => none
 
@@ -287,13 +289,15 @@ def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
 def setInfo (info : SourceInfo) : Syntax → Syntax
   | atom _ val             => atom info val
   | ident _ rawVal val pre => ident info rawVal val pre
-  | stx                    => stx
+  | node _ kind args       => node info kind args
+  | missing                => missing
 
 /-- Return the first atom/identifier that has position information -/
 partial def getHead? : Syntax → Option Syntax
   | stx@(atom info ..)  => info.getPos?.map fun _ => stx
   | stx@(ident info ..) => info.getPos?.map fun _ => stx
-  | node _ args      => args.findSome? getHead?
+  | node SourceInfo.none _ args => args.findSome? getHead?
+  | stx@(node info _ _) => stx
   | _                => none
 
 def copyHeadTailInfoFrom (target source : Syntax) : Syntax :=
@@ -308,7 +312,7 @@ end Syntax
   | some ref => withRef ref x
 
 @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
-  Syntax.node k args
+  Syntax.node SourceInfo.none k args
 
 /- Syntax objects for a Lean module. -/
 structure Module where
@@ -317,12 +321,12 @@ structure Module where
 
 /-- Expand all macros in the given syntax -/
 partial def expandMacros : Syntax → MacroM Syntax
-  | stx@(Syntax.node k args) => do
+  | stx@(Syntax.node info k args) => do
     match (← expandMacro? stx) with
     | some stxNew => expandMacros stxNew
     | none        => do
       let args ← Macro.withIncRecDepth stx <| args.mapM expandMacros
-      pure <| Syntax.node k args
+      pure <| Syntax.node info k args
   | stx => pure stx
 
 /- Helper functions for processing Syntax programmatically -/
@@ -356,10 +360,10 @@ def mkIdent (val : Name) : Syntax :=
   Syntax.ident SourceInfo.none (toString val).toSubstring val []
 
 @[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
-  Syntax.node nullKind args
+  mkNode nullKind args
 
 @[inline] def mkGroupNode (args : Array Syntax := #[]) : Syntax :=
-  Syntax.node groupKind args
+  mkNode groupKind args
 
 def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := do
   let mut i := 0
@@ -374,11 +378,11 @@ def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := do
 
 def mkOptionalNode (arg : Option Syntax) : Syntax :=
   match arg with
-  | some arg => Syntax.node nullKind #[arg]
-  | none     => Syntax.node nullKind #[]
+  | some arg => mkNullNode #[arg]
+  | none     => mkNullNode #[]
 
 def mkHole (ref : Syntax) : Syntax :=
-  Syntax.node `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]
+  mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]
 
 namespace Syntax
 
@@ -398,14 +402,14 @@ instance (sep) : Coe (Array Syntax) (SepArray sep) where
 /-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
 def mkApp (fn : Syntax) : (args : Array Syntax) → Syntax
   | #[]  => fn
-  | args => Syntax.node `Lean.Parser.Term.app #[fn, mkNullNode args]
+  | args => mkNode `Lean.Parser.Term.app #[fn, mkNullNode args]
 
 def mkCApp (fn : Name) (args : Array Syntax) : Syntax :=
   mkApp (mkCIdent fn) args
 
 def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : Syntax :=
   let atom : Syntax := Syntax.atom info val
-  Syntax.node kind #[atom]
+  mkNode kind #[atom]
 
 def mkStrLit (val : String) (info := SourceInfo.none) : Syntax :=
   mkLit strLitKind (String.quote val) info
@@ -481,7 +485,7 @@ def decodeNatLitVal? (s : String) : Option Nat :=
 
 def isLit? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String :=
   match stx with
-  | Syntax.node k args =>
+  | Syntax.node _ k args =>
     if k == litKind && args.size == 1 then
       match args.get! 0 with
       | (Syntax.atom _ val) => some val
@@ -687,8 +691,8 @@ def isNameLit? (stx : Syntax) : Option Name :=
   | _        => none
 
 def hasArgs : Syntax → Bool
-  | Syntax.node _ args => args.size > 0
-  | _                  => false
+  | Syntax.node _ _ args => args.size > 0
+  | _                    => false
 
 def isAtom : Syntax → Bool
   | atom _ _ => true
@@ -700,15 +704,15 @@ def isToken (token : String) : Syntax → Bool
 
 def isNone (stx : Syntax) : Bool :=
   match stx with
-  | Syntax.node k args => k == nullKind && args.size == 0
+  | Syntax.node _ k args => k == nullKind && args.size == 0
   -- when elaborating partial syntax trees, it's reasonable to interpret missing parts as `none`
   | Syntax.missing     => true
   | _                  => false
 
 def getOptional? (stx : Syntax) : Option Syntax :=
   match stx with
-  | Syntax.node k args => if k == nullKind && args.size == 1 then some (args.get! 0) else none
-  | _                  => none
+  | Syntax.node _ k args => if k == nullKind && args.size == 1 then some (args.get! 0) else none
+  | _                    => none
 
 def getOptionalIdent? (stx : Syntax) : Option Name :=
   match stx.getOptional? with
@@ -716,8 +720,8 @@ def getOptionalIdent? (stx : Syntax) : Option Name :=
   | none     => none
 
 partial def findAux (p : Syntax → Bool) : Syntax → Option Syntax
-  | stx@(Syntax.node _ args) => if p stx then some stx else args.findSome? (findAux p)
-  | stx                      => if p stx then some stx else none
+  | stx@(Syntax.node _ _ args) => if p stx then some stx else args.findSome? (findAux p)
+  | stx                        => if p stx then some stx else none
 
 def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
   findAux p stx
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 173fb080ac..737332a7f5 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1744,9 +1744,31 @@ abbrev SyntaxNodeKind := Name
 
 /- Syntax AST -/
 
+/--
+Syntax objects used by the parser, macro expander, delaborator, etc.
+-/
 inductive Syntax where
   | missing : Syntax
-  | node   (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
+  | /--
+  Node in the syntax tree.
+
+  The `info` field is used by the delaborator
+  to store the position of the subexpression
+  corresponding to this node.
+  The parser sets the `info` field to `none`.
+
+  (Remark: the `node` constructor
+  did not have an `info` field in previous versions.
+  This caused a bug in the interactive widgets,
+  where the popup for `a + b` was the same as for `a`.
+  The delaborator used to associate subexpressions
+  with pretty-printed syntax by setting
+  the (string) position of the first atom/identifier
+  to the (expression) position of the subexpression.
+  For example, both `a` and `a + b`
+  have the same first identifier,
+  and so their infos got mixed up.)
+  -/ node   (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
   | atom   (info : SourceInfo) (val : String) : Syntax
   | ident  (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Prod Name (List String))) : Syntax
 
@@ -1771,7 +1793,7 @@ namespace Syntax
 
 def getKind (stx : Syntax) : SyntaxNodeKind :=
   match stx with
-  | Syntax.node k args => k
+  | Syntax.node _ k args => k
   -- We use these "pseudo kinds" for antiquotation kinds.
   -- For example, an antiquotation `$id:ident` (using Lean.Parser.Term.ident)
   -- is compiled to ``if stx.isOfKind `ident ...``
@@ -1781,16 +1803,16 @@ def getKind (stx : Syntax) : SyntaxNodeKind :=
 
 def setKind (stx : Syntax) (k : SyntaxNodeKind) : Syntax :=
   match stx with
-  | Syntax.node _ args => Syntax.node k args
-  | _                  => stx
+  | Syntax.node info _ args => Syntax.node info k args
+  | _                       => stx
 
 def isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool :=
   beq stx.getKind k
 
 def getArg (stx : Syntax) (i : Nat) : Syntax :=
   match stx with
-  | Syntax.node _ args => args.getD i Syntax.missing
-  | _                  => Syntax.missing
+  | Syntax.node _ _ args => args.getD i Syntax.missing
+  | _                    => Syntax.missing
 
 -- Add `stx[i]` as sugar for `stx.getArg i`
 @[inline] def getOp (self : Syntax) (idx : Nat) : Syntax :=
@@ -1798,13 +1820,13 @@ def getArg (stx : Syntax) (i : Nat) : Syntax :=
 
 def getArgs (stx : Syntax) : Array Syntax :=
   match stx with
-  | Syntax.node _ args => args
-  | _                  => Array.empty
+  | Syntax.node _ _ args => args
+  | _                    => Array.empty
 
 def getNumArgs (stx : Syntax) : Nat :=
   match stx with
-  | Syntax.node _ args => args.size
-  | _                  => 0
+  | Syntax.node _ _ args => args.size
+  | _                    => 0
 
 def isMissing : Syntax → Bool
   | Syntax.missing => true
@@ -1829,19 +1851,19 @@ def matchesIdent (stx : Syntax) (id : Name) : Bool :=
 
 def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
   match stx with
-  | node k _ => node k args
-  | stx      => stx
+  | node info k _ => node info k args
+  | stx           => stx
 
 def setArg (stx : Syntax) (i : Nat) (arg : Syntax) : Syntax :=
   match stx with
-  | node k args => node k (args.setD i arg)
-  | stx         => stx
+  | node info k args => node info k (args.setD i arg)
+  | stx              => stx
 
-/-- Retrieve the left-most leaf's info in the Syntax tree. -/
+/-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
 partial def getHeadInfo? : Syntax → Option SourceInfo
   | atom info _   => some info
   | ident info .. => some info
-  | node _ args   =>
+  | node SourceInfo.none _ args   =>
     let rec loop (i : Nat) : Option SourceInfo :=
       match decide (LT.lt i args.size) with
       | true => match getHeadInfo? (args.get! i) with
@@ -1849,6 +1871,7 @@ partial def getHeadInfo? : Syntax → Option SourceInfo
          | none      => loop (hAdd i 1)
       | false => none
     loop 0
+  | node info _ _ => some info
   | _             => none
 
 /-- Retrieve the left-most leaf's info in the Syntax tree, or `none` if there is no token. -/
@@ -1866,7 +1889,9 @@ partial def getTailPos? (stx : Syntax) (originalOnly := false) : Option String.P
   | atom (SourceInfo.synthetic (endPos := pos) ..) _,  false  => some pos
   | ident (SourceInfo.original (endPos := pos) ..) .., _      => some pos
   | ident (SourceInfo.synthetic (endPos := pos) ..) .., false => some pos
-  | node _ args,                                        _     =>
+  | node (SourceInfo.original (endPos := pos) ..) ..,    _    => some pos
+  | node (SourceInfo.synthetic (endPos := pos) ..) .., false  => some pos
+  | node _ _ args,                                        _     =>
     let rec loop (i : Nat) : Option String.Pos :=
       match decide (LT.lt i args.size) with
       | true => match getTailPos? (args.get! ((args.size.sub i).sub 1)) originalOnly with
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 77bd4346db..f30ee84a86 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -335,7 +335,7 @@ private def hasArgsToProcess : M Bool := do
 /- Return true if the next argument at `args` is of the form `_` -/
 private def isNextArgHole : M Bool := do
   match (← get).args with
-  | Arg.stx (Syntax.node ``Lean.Parser.Term.hole _) :: _ => pure true
+  | Arg.stx (Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure true
   | _ => pure false
 
 
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index dade21c8e3..23535e117a 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -41,7 +41,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
     return AttributeKind.local
 
 def mkAttrKindGlobal : Syntax :=
-  Syntax.node ``Lean.Parser.Term.attrKind #[mkNullNode]
+  mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
 def elabAttr {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (attrInstance : Syntax) : m Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 688bb7aff2..5f1f654c8a 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -44,7 +44,7 @@ structure BinderView where
 
 partial def quoteAutoTactic : Syntax → TermElabM Syntax
   | stx@(Syntax.ident _ _ _ _) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
-  | stx@(Syntax.node k args)   => do
+  | stx@(Syntax.node _ k args)   => do
     if stx.isAntiquot then
       throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
     else
@@ -260,16 +260,16 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
         let newBody ← `(match $major:ident with | $pattern => $newBody)
         pure (binders, newBody, true)
       match binder with
-      | Syntax.node ``Lean.Parser.Term.implicitBinder _       => loop body (i+1) (newBinders.push binder)
-      | Syntax.node ``Lean.Parser.Term.strictImplicitBinder _ => loop body (i+1) (newBinders.push binder)
-      | Syntax.node ``Lean.Parser.Term.instBinder _           => loop body (i+1) (newBinders.push binder)
-      | Syntax.node ``Lean.Parser.Term.explicitBinder _       => loop body (i+1) (newBinders.push binder)
-      | Syntax.node ``Lean.Parser.Term.simpleBinder _         => loop body (i+1) (newBinders.push binder)
-      | Syntax.node ``Lean.Parser.Term.hole _ =>
+      | Syntax.node _ ``Lean.Parser.Term.implicitBinder _       => loop body (i+1) (newBinders.push binder)
+      | Syntax.node _ ``Lean.Parser.Term.strictImplicitBinder _ => loop body (i+1) (newBinders.push binder)
+      | Syntax.node _ ``Lean.Parser.Term.instBinder _           => loop body (i+1) (newBinders.push binder)
+      | Syntax.node _ ``Lean.Parser.Term.explicitBinder _       => loop body (i+1) (newBinders.push binder)
+      | Syntax.node _ ``Lean.Parser.Term.simpleBinder _         => loop body (i+1) (newBinders.push binder)
+      | Syntax.node _ ``Lean.Parser.Term.hole _ =>
         let ident ← mkFreshIdent binder
         let type := binder
         loop body (i+1) (newBinders.push <| mkExplicitBinder ident type)
-      | Syntax.node ``Lean.Parser.Term.paren args =>
+      | Syntax.node _ ``Lean.Parser.Term.paren args =>
         -- `(` (termParser >> parenSpecial)? `)`
         -- parenSpecial := (tupleTail <|> typeAscription)?
         let binderBody := binder[1]
@@ -593,7 +593,7 @@ def expandLetEqnsDecl (letDecl : Syntax) : MacroM Syntax := do
   let ref       := letDecl
   let matchAlts := letDecl[3]
   let val ← expandMatchAltsIntoMatch ref matchAlts
-  return Syntax.node `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val]
+  return mkNode `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val]
 
 def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
   let ref     := stx
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 526925315b..060befbeac 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -153,7 +153,7 @@ partial def mkPairs (elems : Array Syntax) : MacroM Syntax :=
   loop (elems.size - 1) elems.back
 
 private partial def hasCDot : Syntax → Bool
-  | Syntax.node k args =>
+  | Syntax.node _ k args =>
     if k == ``Lean.Parser.Term.paren then false
     else if k == ``Lean.Parser.Term.cdot then true
     else args.any hasCDot
@@ -178,7 +178,7 @@ where
     If `stx` is a `·`, we create a fresh identifier, store in the
     extra state, and return it. Otherwise, we just return `stx`. -/
   go : Syntax → StateT (Array Syntax) MacroM Syntax
-    | stx@(Syntax.node k args) =>
+    | stx@(Syntax.node i k args) =>
       if k == ``Lean.Parser.Term.paren then pure stx
       else if k == ``Lean.Parser.Term.cdot then withFreshMacroScope do
         let id ← `(a)
@@ -186,7 +186,7 @@ where
         pure id
       else do
         let args ← args.mapM go
-        pure $ Syntax.node k args
+        pure $ Syntax.node i k args
     | stx => pure stx
 
 /--
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index df6e42f5b9..a5cee04a64 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -258,7 +258,7 @@ builtin_initialize registerTraceClass `Elab.command
 partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
   withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
     match stx with
-    | Syntax.node k args =>
+    | Syntax.node _ k args =>
       if k == nullKind then
         -- list of commands => elaborate in order
         -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 91d7de14d3..09b804cc16 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -91,7 +91,7 @@ def append (str : String) : M Unit :=
 
 partial def collect (stx : Syntax) : M Unit := do
   match stx with
-  | Syntax.node k args =>
+  | Syntax.node _ k args =>
     unless (← isFirst) do
       match kindReplacements.find? k with
       | some r => append r
@@ -133,7 +133,7 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
     | some val => pure val
     | none     =>
       let val ← `(arbitrary)
-      pure $ Syntax.node ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
+      pure $ mkNode ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
   return {
     ref := stx, kind := DefKind.opaque, modifiers := modifiers,
     declId := stx[1], binders := binders, type? := some type, value := val
@@ -150,7 +150,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
     | some declId => pure declId
     | none        =>
       let id ← MkInstanceName.main type
-      pure <| Syntax.node ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
+      pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
   return {
     ref := stx, kind := DefKind.def, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[5]
@@ -160,7 +160,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "example " >> declSig >> declVal
   let (binders, type) := expandDeclSig stx[1]
   let id              := mkIdentFrom stx `_example
-  let declId          := Syntax.node ``Parser.Command.declId #[id, mkNullNode]
+  let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
   { ref := stx, kind := DefKind.example, modifiers := modifiers,
     declId := declId, binders := binders, type? := some type, value := stx[2] }
 
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index c56b0cb4d3..32a46ecf73 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -76,7 +76,7 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
     false
 
 private partial def hasLiftMethod : Syntax → Bool
-  | Syntax.node k args =>
+  | Syntax.node _ k args =>
     if liftMethodDelimiter k then false
     -- NOTE: We don't check for lifts in quotations here, which doesn't break anything but merely makes this rare case a
     -- bit slower
@@ -1183,7 +1183,7 @@ def ensureEOS (doElems : List Syntax) : M Unit :=
     throwError "must be last element in a 'do' sequence"
 
 private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Syntax → StateT (List Syntax) M Syntax
-  | stx@(Syntax.node k args) =>
+  | stx@(Syntax.node i k args) =>
     if liftMethodDelimiter k then
       return stx
     else if k == ``Lean.Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
@@ -1198,7 +1198,7 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
       let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
       let inBinder   := inBinder || (!inQuot && liftMethodForbiddenBinder stx)
       let args ← args.mapM (expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder)
-      return Syntax.node k args
+      return Syntax.node i k args
   | stx => pure stx
 
 def expandLiftMethod (doElem : Syntax) : M (List Syntax × Syntax) := do
@@ -1612,7 +1612,7 @@ private partial def ensureArrowNotUsed (stx : Syntax) : MacroM Unit := do
 where
   go (stx : Syntax) : MacroM Unit :=
     match stx with
-    | Syntax.node k args => do
+    | Syntax.node i k args => do
       if k == ``Parser.Term.liftMethod || k == ``Parser.Term.doLetArrow || k == ``Parser.Term.doReassignArrow || k == ``Parser.Term.doIfLetBind then
         Macro.throwErrorAt stx "`←` and `<-` are not allowed in pure `do` blocks, i.e., blocks where Lean implicitly used the `Id` monad"
       unless k == ``Parser.Term.do do
diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean
index 751529f87a..4eb04b4870 100644
--- a/src/Lean/Elab/ElabRules.lean
+++ b/src/Lean/Elab/ElabRules.lean
@@ -88,7 +88,7 @@ def expandElab : Macro
     let name ← match name? with
       | some name => pure name.getId
       | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-    let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) patArgs
+    let pat := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs
     `($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat
       $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs)
   | _ => Macro.throwUnsupported
diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean
index c85607869f..708869a655 100644
--- a/src/Lean/Elab/Macro.lean
+++ b/src/Lean/Elab/Macro.lean
@@ -22,7 +22,7 @@ open Lean.Parser.Command
       | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
     /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
       So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
-    let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) patArgs
+    let pat := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs
     let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind
       syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat)
     let macroRulesCmd ←
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 266d5149ae..8f55846f96 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -993,7 +993,7 @@ builtin_initialize
     match (← isLocalIdent? discrExpr) with
     | some _ =>
       let expectedType ← waitExpectedType expectedType?
-      let discr := Syntax.node ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]
+      let discr := mkNode ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]
       elabMatchAux none #[discr] #[] mkNullNode expectedType
     | _ =>
       let stxNew ← `(let _discr := $discrExpr; nomatch _discr)
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index ab72486838..d5079515a4 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -20,16 +20,16 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
     else
       stx
   | _ => match stx with
-    | Syntax.node k args => Syntax.node k (args.map (antiquote vars))
+    | Syntax.node i k args => Syntax.node i k (args.map (antiquote vars))
     | stx => stx
 
 /- Convert `notation` command lhs item into a `syntax` command item -/
 def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
   let k := stx.getKind
   if k == `Lean.Parser.Command.identPrec then
-    pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term,  stx[1]]
+    pure $ mkNode `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term,  stx[1]]
   else if k == strLitKind then
-    pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
+    pure $ mkNode `Lean.Parser.Syntax.atom #[stx]
   else
     Macro.throwUnsupported
 
@@ -88,7 +88,7 @@ private def expandNotationAux (ref : Syntax)
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
   let fullName := currNamespace ++ name
-  let pat := Syntax.node fullName patArgs
+  let pat := mkNode fullName patArgs
   let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):numLit) $[$syntaxParts]* : $cat)
   let mut macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
   if isLocalAttrKind attrKind then
diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean
index 68fbcec777..e91dfead6d 100644
--- a/src/Lean/Elab/PatternVar.lean
+++ b/src/Lean/Elab/PatternVar.lean
@@ -26,7 +26,7 @@ instance : ToString PatternVar := ⟨fun
   The metavariables are created before we elaborate the patterns into `Expr`s. -/
 private def mkMVarSyntax : TermElabM Syntax := do
   let mvarId ← mkFreshId
-  return Syntax.node `MVarWithIdKind #[Syntax.node mvarId #[]]
+  return mkNode `MVarWithIdKind #[mkNode mvarId #[]]
 
 /-- Given a syntax node constructed using `mkMVarSyntax`, return its MVarId -/
 def getMVarSyntaxMVarId (stx : Syntax) : MVarId :=
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 3728d34e95..e12c578e14 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -20,7 +20,7 @@ open Meta
 
 /-- `C[$(e)]` ~> `let a := e; C[$a]`. Used in the implementation of antiquot splices. -/
 private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermElabM Syntax) TermElabM Syntax
-  | stx@(Syntax.node k args) => do
+  | stx@(Syntax.node i k args) => do
     if isAntiquot stx && !isEscapedAntiquot stx then
       let e := getAntiquotTerm stx
       if !e.isIdent || !e.getId.isAtomic then
@@ -28,7 +28,7 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
           let a ← `(a)
           modify (fun cont stx => (`(let $a:ident := $e; $stx) : TermElabM _))
           stx.setArg 2 a
-    Syntax.node k (← args.mapM floatOutAntiquotTerms)
+    Syntax.node i k (← args.mapM floatOutAntiquotTerms)
   | stx => pure stx
 
 private def getSepFromSplice (splice : Syntax) : Syntax := do
@@ -94,7 +94,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
     -- `scp` is bound in stxQuot.expand
     `(Syntax.ident info $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
   -- if antiquotation, insert contents as-is, else recurse
-  | stx@(Syntax.node k _) => do
+  | stx@(Syntax.node _ k _) => do
     if isAntiquot stx && !isEscapedAntiquot stx then
       getAntiquotTerm stx
     else if isTokenAntiquot stx && !isEscapedAntiquot stx then
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 1be8b4141c..d5a74de568 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -182,7 +182,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     let valFirst  := if valFirst.getKind == ``Lean.Parser.Term.structInstArrayRef then valFirst else valFirst[1]
     let restArgs  := rest.getArgs
     let valRest   := mkNullNode restArgs[1:restArgs.size]
-    let valField  := modifyOp.setArg 0 <| Syntax.node ``Parser.Term.structInstLVal #[valFirst, valRest]
+    let valField  := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
     let valSource := mkSourcesWithSyntax #[s]
     let val       := stx.setArg 1 valSource
     let val       := val.setArg 2 <| mkNullNode #[mkNullNode #[valField, mkNullNode]]
@@ -452,7 +452,7 @@ private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName
 def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
   if (← findField? (← getEnv) structName fieldName).isNone then
     return none
-  return some $ Syntax.node ``Lean.Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
+  return some $ mkNode ``Lean.Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
 
 def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
   fields.find? fun field =>
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index cf60a36fa7..50753cebf1 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -155,7 +155,7 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let mut fieldBinder := fieldBinder
     if fieldBinder.getKind == ``Parser.Command.structSimpleBinder then
-      fieldBinder := Syntax.node ``Parser.Command.structExplicitBinder
+      fieldBinder := mkNode ``Parser.Command.structExplicitBinder
         #[ fieldBinder[0], mkAtomFrom fieldBinder "(", mkNullNode #[ fieldBinder[1] ], fieldBinder[2], fieldBinder[3], fieldBinder[4], mkAtomFrom fieldBinder ")" ]
     let k := fieldBinder.getKind
     let binfo ←
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index fc5f914441..843924c043 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -263,7 +263,7 @@ where
     | some val => acc ++ (val.trim.map fun c => if c.isWhitespace then '_' else c).capitalize
     | none =>
       match stx with
-      | Syntax.node k args =>
+      | Syntax.node _ k args =>
         if k == ``Lean.Parser.Syntax.cat then
           acc ++ "_"
         else
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 57e1f046c5..f107e51869 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -176,7 +176,7 @@ mutual
 
   partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
     withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
-      | Syntax.node k args =>
+      | Syntax.node _ k args =>
         if k == nullKind then
           -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
           stx.getArgs.forM evalTactic
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index 00e9e35481..3b66972089 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -99,7 +99,7 @@ private partial def sanitizeSyntaxAux : Syntax → StateM NameSanitizerState Syn
     mkIdentFrom stx <$> match (← get).userName2Sanitized.find? n with
     | some n' => pure n'
     | none    => if n.hasMacroScopes then sanitizeName n else pure n
-  | Syntax.node k args => Syntax.node k <$> args.mapM sanitizeSyntaxAux
+  | Syntax.node info k args => Syntax.node info k <$> args.mapM sanitizeSyntaxAux
   | stx => pure stx
 
 def sanitizeSyntax (stx : Syntax) : StateM NameSanitizerState Syntax := do
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 677ef83e18..7e6bba75b2 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -231,7 +231,7 @@ def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserSta
       let stack   := stack.push Syntax.missing
       ⟨stack, lhsPrec, pos, cache, err⟩
     else
-      let newNode := Syntax.node k (stack.extract iniStackSz stack.size)
+      let newNode := Syntax.node SourceInfo.none k (stack.extract iniStackSz stack.size)
       let stack   := stack.shrink iniStackSz
       let stack   := stack.push newNode
       ⟨stack, lhsPrec, pos, cache, err⟩
@@ -239,7 +239,7 @@ def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserSta
 def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState :=
   match s with
   | ⟨stack, lhsPrec, pos, cache, err⟩ =>
-    let newNode := Syntax.node k (stack.extract (iniStackSz - 1) stack.size)
+    let newNode := Syntax.node SourceInfo.none k (stack.extract (iniStackSz - 1) stack.size)
     let stack   := stack.shrink (iniStackSz - 1)
     let stack   := stack.push newNode
     ⟨stack, lhsPrec, pos, cache, err⟩
@@ -1638,7 +1638,7 @@ def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState
         | some as' => (s, as ++ as')
         | _        => (s, as)
       | none    => find identKind
-  | Except.ok (Syntax.node k _)        => find k
+  | Except.ok (Syntax.node _ k _)      => find k
   | Except.ok _                        => (s, [])
   | Except.error s'                    => (s', [])
 
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index f12cd4929f..fb644a3193 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -54,7 +54,7 @@ def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × M
 
 private def mkEOI (pos : String.Pos) : Syntax :=
   let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""
-  Syntax.node `Lean.Parser.Module.eoi #[atom]
+  mkNode `Lean.Parser.Module.eoi #[atom]
 
 def isEOI (s : Syntax) : Bool :=
   s.isOfKind `Lean.Parser.Module.eoi
@@ -119,7 +119,7 @@ def testParseModule (env : Environment) (fname contents : String) : IO Syntax :=
   let inputCtx := mkInputContext contents fname
   let (header, state, messages) ← parseHeader inputCtx
   let cmds ← testParseModuleAux env inputCtx state messages #[]
-  let stx := Syntax.node `Lean.Parser.Module.module #[header, mkListNode cmds]
+  let stx := mkNode `Lean.Parser.Module.module #[header, mkListNode cmds]
   pure stx.updateLeading
 
 def testParseFile (env : Environment) (fname : System.FilePath) : IO Syntax := do
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 53b09cf806..36c47c460e 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -113,7 +113,7 @@ def compileCategoryParser {α} (ctx : Context α) (declName : Name) (builtin : B
   let attrName := if builtin then ctx.categoryAttr.defn.builtinName else ctx.categoryAttr.defn.name
   -- Create syntax node for a simple attribute of the form
   -- `def simple := leading_parser ident >> optional (ident <|> priorityParser)`
-  let stx := Syntax.node `Lean.Parser.Attr.simple #[
+  let stx := mkNode `Lean.Parser.Attr.simple #[
     mkIdent attrName,
     mkNullNode #[mkIdent kind]
   ]
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index df6d19261a..a11b45f15d 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -158,7 +158,7 @@ def whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab := do
 partial def annotatePos (pos : Nat) : Syntax → Syntax
   | 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)
+  | 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 (SourceInfo.synthetic pos pos))
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 776c9cc7d9..cb39f4c7e4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -444,7 +444,7 @@ but in the delaborator we assume that bindings are never shadowed.
 -/
 partial def hasIdent (id : Name) : Syntax → Bool
   | Syntax.ident _ _ id' _ => id == id'
-  | Syntax.node _ args     => args.any (hasIdent id)
+  | Syntax.node _ _ args   => args.any (hasIdent id)
   | _                      => false
 
 /--
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 7b4822bf92..e1f6c3faea 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -15,7 +15,7 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 /- Syntax AST -/
 
 inductive IsNode : Syntax → Prop where
-  | mk (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node kind args)
+  | mk (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node info kind args)
 
 def SyntaxNode : Type := {s : Syntax // IsNode s }
 
@@ -27,14 +27,14 @@ namespace SyntaxNode
 
 @[inline] def getKind (n : SyntaxNode) : SyntaxNodeKind :=
   match n with
-  | ⟨Syntax.node k args, _⟩ => k
+  | ⟨Syntax.node _ k _, _⟩  => k
   | ⟨Syntax.missing, h⟩     => unreachIsNodeMissing h
   | ⟨Syntax.atom .., h⟩     => unreachIsNodeAtom h
   | ⟨Syntax.ident .., h⟩    => unreachIsNodeIdent h
 
 @[inline] def withArgs {β} (n : SyntaxNode) (fn : Array Syntax → β) : β :=
   match n with
-  | ⟨Syntax.node _ args, _⟩   => fn args
+  | ⟨Syntax.node _ _ args, _⟩   => fn args
   | ⟨Syntax.missing, h⟩       => unreachIsNodeMissing h
   | ⟨Syntax.atom _ _, h⟩      => unreachIsNodeAtom h
   | ⟨Syntax.ident _ _ _ _, h⟩ => unreachIsNodeIdent h
@@ -50,7 +50,7 @@ namespace SyntaxNode
 
 @[inline] def modifyArgs (n : SyntaxNode) (fn : Array Syntax → Array Syntax) : Syntax :=
   match n with
-  | ⟨Syntax.node kind args, _⟩ => Syntax.node kind (fn args)
+  | ⟨Syntax.node i k args, _⟩  => Syntax.node i k (fn args)
   | ⟨Syntax.missing, h⟩        => unreachIsNodeMissing h
   | ⟨Syntax.atom _ _, h⟩       => unreachIsNodeAtom h
   | ⟨Syntax.ident _ _ _ _,  h⟩ => unreachIsNodeIdent h
@@ -69,44 +69,44 @@ def setAtomVal : Syntax → String → Syntax
 
 @[inline] def ifNode {β} (stx : Syntax) (hyes : SyntaxNode → β) (hno : Unit → β) : β :=
   match stx with
-  | Syntax.node k args => hyes ⟨Syntax.node k args, IsNode.mk k args⟩
-  | _                  => hno ()
+  | Syntax.node i k args => hyes ⟨Syntax.node i k args, IsNode.mk i k args⟩
+  | _                    => hno ()
 
 @[inline] def ifNodeKind {β} (stx : Syntax) (kind : SyntaxNodeKind) (hyes : SyntaxNode → β) (hno : Unit → β) : β :=
   match stx with
-  | Syntax.node k args => if k == kind then hyes ⟨Syntax.node k args, IsNode.mk k args⟩ else hno ()
-  | _                  => hno ()
+  | Syntax.node i k args => if k == kind then hyes ⟨Syntax.node i k args, IsNode.mk i k args⟩ else hno ()
+  | _                    => hno ()
 
 def asNode : Syntax → SyntaxNode
-  | Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩
-  | _                     => ⟨Syntax.node nullKind #[], IsNode.mk nullKind #[]⟩
+  | Syntax.node info kind args => ⟨Syntax.node info kind args, IsNode.mk info kind args⟩
+  | _                          => ⟨mkNullNode, IsNode.mk _ _ _⟩
 
 def getIdAt (stx : Syntax) (i : Nat) : Name :=
   (stx.getArg i).getId
 
 @[inline] def modifyArgs (stx : Syntax) (fn : Array Syntax → Array Syntax) : Syntax :=
   match stx with
-  | node k args => node k (fn args)
-  | stx         => stx
+  | node i k args => node i k (fn args)
+  | stx           => stx
 
 @[inline] def modifyArg (stx : Syntax) (i : Nat) (fn : Syntax → Syntax) : Syntax :=
   match stx with
-  | node k args => node k (args.modify i fn)
-  | stx         => stx
+  | node info k args => node info k (args.modify i fn)
+  | stx              => stx
 
 @[specialize] partial def replaceM {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m (Syntax)
-  | stx@(node kind args) => do
+  | stx@(node info kind args) => do
     match (← fn stx) with
     | some stx => return stx
-    | none     => return node kind (← args.mapM (replaceM fn))
+    | none     => return node info kind (← args.mapM (replaceM fn))
   | stx => do
     let o ← fn stx
     return o.getD stx
 
 @[specialize] partial def rewriteBottomUpM {m : Type → Type} [Monad m] (fn : Syntax → m (Syntax)) : Syntax → m (Syntax)
-  | node kind args   => do
+  | node info kind args   => do
     let args ← args.mapM (rewriteBottomUpM fn)
-    fn (node kind args)
+    fn (node info kind args)
   | stx => fn stx
 
 @[inline] def rewriteBottomUp (fn : Syntax → Syntax) (stx : Syntax) : Syntax :=
@@ -157,19 +157,20 @@ def updateLeading : 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)             =>
+  | n@(Syntax.node info k args)        =>
     if args.size == 0 then n
     else
      let i    := args.size - 1
      let last := updateTrailing trailing args[i]
      let args := args.set! i last;
-     Syntax.node k args
+     Syntax.node info k args
   | s => s
 
 partial def getTailWithPos : Syntax → Option Syntax
   | stx@(atom info _)   => info.getPos?.map fun _ => stx
   | stx@(ident info ..) => info.getPos?.map fun _ => stx
-  | node _ args         => args.findSomeRev? getTailWithPos
+  | node SourceInfo.none _ args => args.findSomeRev? getTailWithPos
+  | stx@(node info _ _) => stx
   | _                   => none
 
 open SourceInfo in
@@ -232,7 +233,7 @@ partial instance : ForIn m TopDown Syntax where
       match (← f stx b) with
       | ForInStep.yield b' =>
         let mut b := b'
-        if let Syntax.node k args := stx then
+        if let Syntax.node i k args := stx then
           if firstChoiceOnly && k == choiceKind then
             return ← loop args[0] b
           else
@@ -253,7 +254,7 @@ partial def reprint (stx : Syntax) : Option String :=
       match stx with
       | atom info val           => s := s ++ reprintLeaf info val
       | ident info rawVal _ _   => s := s ++ reprintLeaf info rawVal.toString
-      | node kind args          =>
+      | node info kind args     =>
         if kind == choiceKind then
           -- this visit the first arg twice, but that should hardly be a problem
           -- given that choice nodes are quite rare and small
@@ -358,15 +359,15 @@ namespace SyntaxNode
 end SyntaxNode
 
 def mkListNode (args : Array Syntax) : Syntax :=
-  Syntax.node nullKind args
+  mkNullNode args
 
 namespace Syntax
 
 -- quotation node kinds are formed from a unique quotation name plus "quot"
 def isQuot : Syntax → Bool
-  | Syntax.node (Name.str _ "quot" _)         _  => true
-  | Syntax.node `Lean.Parser.Term.dynamicQuot _ => true
-  | _                                            => false
+  | Syntax.node _ (Name.str _ "quot" _)         _ => true
+  | Syntax.node _ `Lean.Parser.Term.dynamicQuot _ => true
+  | _                                             => false
 
 def getQuotContent (stx : Syntax) : Syntax :=
   if stx.isOfKind `Lean.Parser.Term.dynamicQuot then
@@ -376,8 +377,8 @@ def getQuotContent (stx : Syntax) : Syntax :=
 
 -- antiquotation node kinds are formed from the original node kind (if any) plus "antiquot"
 def isAntiquot : Syntax → Bool
-  | Syntax.node (Name.str _ "antiquot" _) _ => true
-  | _                                       => false
+  | Syntax.node _ (Name.str _ "antiquot" _) _ => true
+  | _                                         => false
 
 def mkAntiquotNode (term : Syntax) (nesting := 0) (name : Option String := none) (kind := Name.anonymous) : Syntax :=
   let nesting := mkNullNode (mkArray nesting (mkAtom "$"))
@@ -409,7 +410,7 @@ def getAntiquotTerm (stx : Syntax) : Syntax :=
     e[1]
 
 def antiquotKind? : Syntax → Option SyntaxNodeKind
-  | Syntax.node (Name.str k "antiquot" _) args =>
+  | Syntax.node _ (Name.str k "antiquot" _) args =>
     if args[3].isOfKind `antiquotName then some k
     else
       -- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`)
@@ -418,8 +419,8 @@ def antiquotKind? : Syntax → Option SyntaxNodeKind
 
 -- An "antiquotation splice" is something like `$[...]?` or `$[...]*`.
 def antiquotSpliceKind? : Syntax → Option SyntaxNodeKind
-  | Syntax.node (Name.str k "antiquot_scope" _) args => some k
-  | _                                                => none
+  | Syntax.node _ (Name.str k "antiquot_scope" _) args => some k
+  | _                                                  => none
 
 def isAntiquotSplice (stx : Syntax) : Bool :=
   antiquotSpliceKind? stx |>.isSome
@@ -440,8 +441,8 @@ def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suff
 
 -- `$x,*` etc.
 def antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind
-  | Syntax.node (Name.str k "antiquot_suffix_splice" _) args => some k
-  | _                                                        => none
+  | Syntax.node _ (Name.str k "antiquot_suffix_splice" _) args => some k
+  | _                                                          => none
 
 def isAntiquotSuffixSplice (stx : Syntax) : Bool :=
   antiquotSuffixSplice? stx |>.isSome
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index 1a31b2e879..26cd16eabd 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -15,10 +15,10 @@ fun x =>
       let scp ← Lean.getCurrMacroScope 
       let mainModule ← Lean.getMainModule 
       pure
-          (Lean.Syntax.node `Lean.Parser.Term.app
+          (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
             #[Lean.Syntax.ident info (String.toSubstring "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp)
                 [(`Nat.add, [])],
-              Lean.Syntax.node `null #[lhs, rhs]])
+              Lean.Syntax.node Lean.SourceInfo.none `null #[lhs, rhs]])
   else
     let discr := x;
     throw Lean.Macro.Exception.unsupportedSyntax
@@ -38,7 +38,7 @@ fun x =>
           let info ← Lean.MonadRef.mkInfoFromRefPos 
           let _ ← Lean.getCurrMacroScope 
           let _ ← Lean.getMainModule 
-          pure (Lean.Syntax.node `«term_+++_» #[lhs, Lean.Syntax.atom info "+++", rhs])
+          pure (Lean.Syntax.node Lean.SourceInfo.none `«term_+++_» #[lhs, Lean.Syntax.atom info "+++", rhs])
       else
         let discr := Lean.Syntax.getArg discr 1;
         throw ())
diff --git a/tests/lean/run/CommandExtOverlap.lean b/tests/lean/run/CommandExtOverlap.lean
index 4c3f604ace..62ffc698db 100644
--- a/tests/lean/run/CommandExtOverlap.lean
+++ b/tests/lean/run/CommandExtOverlap.lean
@@ -4,7 +4,7 @@ open Lean
 
 macro_rules (kind := mycheck)
 | `(#check $es,*) =>
-  let cmds := es.getElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[mkAtom "#check", e]
+  let cmds := es.getElems.map $ fun e => mkNode `Lean.Parser.Command.check #[mkAtom "#check", e]
   pure $ mkNullNode cmds
 
 #check true
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index 41228deb6d..c1070c8991 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -95,11 +95,11 @@ if x > 10 then g x else pure none
 syntax:max (name := doHash) "#" : term
 
 partial def expandHash : Syntax → StateT Bool MacroM Syntax
-| Syntax.node k args =>
+| Syntax.node i k args =>
   if k == `doHash then do set true; `(←MonadState.get)
   else do
     let args ← args.mapM expandHash;
-    pure $ Syntax.node k args;
+    pure $ Syntax.node i k args;
 | stx => pure stx
 
 @[macro Lean.Parser.Term.do] def expandDo : Macro :=
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index 29f968675f..ebee3f77b4 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 (kind := myintro)
-| `(tactic| intros $x,*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[mkAtom "intros", mkNullNode x]
+| `(tactic| intros $x,*) => pure $ mkNode `Lean.Parser.Tactic.intros #[mkAtom "intros", mkNullNode x]
 
 theorem tst1 {p q : Prop} : p → q → p :=
 by {