diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 18df55ec78..7278b7ccfb 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -124,13 +124,6 @@ instance monadNameGeneratorLift (m n : Type → Type) [MonadNameGenerator m] [Mo
 
 namespace Syntax
 
-/-- Retrieve the left-most leaf's info in the Syntax tree. -/
-partial def getHeadInfo : Syntax → Option SourceInfo
-  | atom info _      => info
-  | ident info _ _ _ => info
-  | node _ args      => args.findSome? getHeadInfo
-  | _                => none
-
 partial def getTailInfo : Syntax → Option SourceInfo
   | atom info _   => info
   | ident info .. => info
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ad76425e8b..1a51faf29d 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1463,8 +1463,29 @@ def getArgs (stx : Syntax) : Array Syntax :=
   | Syntax.node _ args => args
   | _                  => Array.empty
 
+/-- Retrieve the left-most leaf's info in the Syntax tree. -/
+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
+         | some info => some info
+         | none      => loop (add i 1)
+      | false => none
+    loop 0
+  | _                => none
+
+def getPos (stx : Syntax) : Option String.Pos :=
+  match stx.getHeadInfo with
+  | some info => info.pos
+  | _         => none
+
 end Syntax
 
+/- Parser descriptions -/
+
 inductive ParserDescr
   | const  (name : Name)
   | unary  (name : Name) (p : ParserDescr)
@@ -1649,6 +1670,27 @@ def defaultMaxRecDepth := 512
 def maxRecDepthErrorMessage : String :=
   "maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
 
+class MonadRef (m : Type → Type) :=
+  (getRef      : m Syntax)
+  (withRef {α} : Syntax → m α → m α)
+
+export MonadRef (getRef)
+
+instance (m n : Type → Type) [MonadRef m] [MonadFunctor m n] [MonadLift m n] : MonadRef n := {
+  getRef  := liftM (getRef : m _),
+  withRef := fun ref x => monadMap (m := m) (MonadRef.withRef ref) x
+}
+
+def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
+  match ref.getPos with
+  | some _ => ref
+  | _      => oldRef
+
+@[inline] def withRef {m : Type → Type} [Monad m] [MonadRef m] {α} (ref : Syntax) (x : m α) : m α :=
+  bind getRef fun oldRef =>
+  let ref := replaceRef ref oldRef
+  MonadRef.withRef ref x
+
 namespace Macro
 
 /- References -/
diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index 43a4eb81be..4b2376b90a 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -31,7 +31,7 @@ def setImplementedBy (env : Environment) (declName : Name) (impName : Name) : Ex
 
 end Compiler
 
-def setImplementedBy {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+def setImplementedBy {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
     (declName : Name) (impName : Name) : m Unit := do
   let env ← getEnv
   match Compiler.setImplementedBy env declName impName with
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index d20c6bec64..63cd88ab1f 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -32,7 +32,7 @@ abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception)
 
 instance {α} : Inhabited (CoreM α) := ⟨fun _ _ => throw $ arbitrary _⟩
 
-instance : Ref CoreM := {
+instance : MonadRef CoreM := {
   getRef  := do let ctx ← read; pure ctx.ref,
   withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
 }
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 12436ba273..4626f4d51d 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -16,7 +16,7 @@ instance : ToFormat Attribute := ⟨fun attr =>
 
 instance : Inhabited Attribute := ⟨{ name := arbitrary _ }⟩
 
-def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m Attribute := do
+def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (stx : Syntax) : m Attribute := do
   -- rawIdent >> many attrArg
   let nameStx := stx[0]
   let attrName ← match nameStx.isIdOrAtom? with
@@ -31,14 +31,14 @@ def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [Add
   pure { name := attrName, args := args }
 
 -- sepBy1 attrInstance ", "
-def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) := do
+def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in stx.getSepArgs do
     attrs := attrs.push (← elabAttr attr)
   return attrs
 
 -- parser! "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1]
 
 end Lean.Elab
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index d5ac9eca82..46542a97b0 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -79,7 +79,7 @@ instance : AddMessageContext CommandElabM := {
   addMessageContext := addMessageContextPartial
 }
 
-instance : Ref CommandElabM := {
+instance : MonadRef CommandElabM := {
   getRef     := Command.getRef,
   withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
 }
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index d4b65b984c..9392c2e53e 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -10,7 +10,7 @@ import Lean.Elab.DeclUtil
 
 namespace Lean.Elab
 
-def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (declName : Name) : m Unit := do
+def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (declName : Name) : m Unit := do
   let env ← getEnv
   if env.contains declName then
     match privateToUserName? declName with
@@ -70,7 +70,7 @@ instance : ToString Modifiers := ⟨toString ∘ format⟩
 
 section Methods
 
-variables {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+variables {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
 
 def elabModifiers (stx : Syntax) : m Modifiers := do
   let docCommentStx := stx[0]
diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index 5cb9d1fc24..8eb88e5fb6 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -18,10 +18,10 @@ def throwPostpone {α m} [MonadExceptOf Exception m] : m α :=
 def throwUnsupportedSyntax {α m} [MonadExceptOf Exception m] : m α :=
   throw $ Exception.internal unsupportedSyntaxExceptionId
 
-def throwIllFormedSyntax {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] : m α :=
+def throwIllFormedSyntax {α m} [Monad m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] : m α :=
   throwError "ill-formed syntax"
 
-def throwAlreadyDeclaredUniverseLevel {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (u : Name) : m α :=
+def throwAlreadyDeclaredUniverseLevel {α m} [Monad m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (u : Name) : m α :=
   throwError! "a universe level named '{u}' has already been declared"
 
 -- Throw exception to abort elaboration without producing any error message
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index 5c9cb61aaf..e5e399ecb4 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -19,7 +19,7 @@ structure State :=
 
 abbrev LevelElabM := ReaderT Context (EStateM Exception State)
 
-instance : Ref LevelElabM := {
+instance : MonadRef LevelElabM := {
   getRef      := return (← read).ref,
   withRef     := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
 }
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 409d4a0496..48bef47c9d 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -142,7 +142,7 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
     | ex                                => throw ex
 
 @[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
-    [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : MacroM α) : m α := do
+    [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (x : MacroM α) : m α := do
   let env  ← getEnv
   match x { macroEnv       := Macro.mkMacroEnv (expandMacro? env),
             currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
@@ -154,7 +154,7 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
   | EStateM.Result.ok a nextMacroScope                       => MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
 
 @[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
-    [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
+    [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
   liftMacroM (x stx)
 
 builtin_initialize
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 06f39496c3..5e146b4915 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -24,27 +24,6 @@ def Exception.getRef : Exception → Syntax
 
 instance : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
 
-class Ref (m : Type → Type) :=
-  (getRef      : m Syntax)
-  (withRef {α} : Syntax → m α → m α)
-
-export Ref (getRef)
-
-instance (m n : Type → Type) [Ref m] [MonadFunctor m n] [MonadLift m n] : Ref n := {
-  getRef  := liftM (getRef : m _),
-  withRef := fun ref x => monadMap (m := m) (Ref.withRef ref) x
-}
-
-def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
-  match ref.getPos with
-  | some _ => ref
-  | _      => oldRef
-
-@[inline] def withRef {m : Type → Type} [Monad m] [Ref m] {α} (ref : Syntax) (x : m α) : m α := do
-  let oldRef ← getRef
-  let ref := replaceRef ref oldRef
-  Ref.withRef ref x
-
 /- Similar to `AddMessageContext`, but for error messages.
    The default instance just uses `AddMessageContext`.
    In error messages, we may want to provide additional information (e.g., macro expansion stack),
@@ -60,7 +39,7 @@ instance (m : Type → Type) [AddMessageContext m] [Monad m] : AddErrorMessageCo
 
 section Methods
 
-variables {m : Type → Type} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+variables {m : Type → Type} [Monad m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
 
 def throwError {α} (msg : MessageData) : m α := do
   let ref ← getRef
@@ -97,7 +76,7 @@ instance {ρ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) := {
 instance {ω σ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
   inferInstanceAs (MonadRecDepth (ReaderT _ _))
 
-@[inline] def withIncRecDepth {α m} [Monad m] [MonadRecDepth m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+@[inline] def withIncRecDepth {α m} [Monad m] [MonadRecDepth m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
     (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 101c499c0e..ef1224953b 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -66,7 +66,7 @@ private def getFunctionDomain (f : Expr) : MetaM Expr := do
   | Expr.forallE _ d _ _ => pure d
   | _                    => throwFunctionExpected f
 
-def throwAppTypeMismatch {α} {m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadLiftT MetaM m]
+def throwAppTypeMismatch {α} {m} [Monad m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] [MonadLiftT MetaM m]
     (f a : Expr) (extraMsg : MessageData := Format.nil) : m α := do
   let e := mkApp f a
   let aType ← inferType a
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 0ee19466e3..4a012bd851 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -61,7 +61,7 @@ private partial def mkAuxNameAux (env : Environment) (base : Name) (i : Nat) : N
 def mkAuxName (baseName : Name) (idx : Nat) : m Name := do
   return mkAuxNameAux (← getEnv) baseName idx
 
-variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+variables [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
 
 def getConstInfo (constName : Name) : m ConstantInfo := do
   match (← getEnv).find? constName with
@@ -107,7 +107,7 @@ def addAndCompile [MonadOptions m] (decl : Declaration) : m Unit := do
   addDecl decl;
   compileDecl decl
 
-variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadOptions m]
+variables [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] [MonadOptions m]
 
 unsafe def evalConst (α) (constName : Name) : m α := do
   ofExcept $ (← getEnv).evalConst α (← getOptions) constName
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index c46bd3a9a5..44920a05f7 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -184,7 +184,7 @@ variables {m : Type → Type} [Monad m] [MonadResolveName m] [MonadEnv m]
 def resolveGlobalName  (id : Name) : m (List (Name × List String)) := do
   return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
 
-variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+variables [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
 
 def resolveNamespace (id : Name) : m Name := do
   match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index d49b81095c..6629235510 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -188,9 +188,6 @@ partial def updateTrailing (trailing : Option Substring) : Syntax → Syntax
      Syntax.node k args
   | s => s
 
-def getPos (stx : Syntax) : Option String.Pos :=
-  stx.getHeadInfo >>= SourceInfo.pos
-
 partial def getTailWithPos : Syntax → Option Syntax
   | stx@(atom { pos := some _, .. } _)   => some stx
   | stx@(ident { pos := some _, .. } ..) => some stx
diff --git a/src/Lean/Util/Constructions.lean b/src/Lean/Util/Constructions.lean
index d0a16d7e98..c11f00d965 100644
--- a/src/Lean/Util/Constructions.lean
+++ b/src/Lean/Util/Constructions.lean
@@ -16,7 +16,7 @@ namespace Lean
 @[extern "lean_mk_brec_on"] constant mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
 @[extern "lean_mk_binduction_on"] constant mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
 
-variables {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadOptions m]
+variables {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] [MonadOptions m]
 
 @[inline] private def adaptFn (f : Environment → Name → Except KernelException Environment) (declName : Name) : m Unit := do
   match f (← getEnv) declName with
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index a18459a511..4556b5e6a9 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -103,7 +103,7 @@ private def getResetTraces : m (PersistentArray TraceElem) := do
   pure oldTraces
 
 section
-variables [Ref m] [AddMessageContext m] [MonadOptions m]
+variables [MonadRef m] [AddMessageContext m] [MonadOptions m]
 
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
   let ref ← getRef
@@ -150,7 +150,7 @@ macro_rules
     else
       `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
 
-variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [Ref m]
+variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [MonadRef m]
 
 def withNestedTraces [MonadFinally m] (x : m α) : m α := do
   let s ← getTraceState