diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index 80d788bdce..f1e49c6829 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -59,8 +59,8 @@ def isAbortTacticException (ex : Exception) : Bool :=
 def isAbortExceptionId (id : InternalExceptionId) : Bool :=
   id == abortCommandExceptionId || id == abortTermExceptionId || id == abortTacticExceptionId
 
-def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (rawPos : String.Pos) : Message :=
-  let pos := fileMap.toPosition rawPos
-  { fileName := fileName, rawPos := rawPos, pos := pos, data := msgData, severity := severity }
+def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
+  let pos := fileMap.toPosition pos
+  { fileName := fileName, pos := pos, data := msgData, severity := severity }
 
 end Lean.Elab
diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index cbee37a3e3..18cab54e25 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -23,7 +23,7 @@ def processHeader (header : Syntax) (opts : Options) (messages : MessageLog) (in
     let env ← mkEmptyEnvironment
     let spos := header.getPos?.getD 0
     let pos  := inputCtx.fileMap.toPosition spos
-    pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, rawPos := spos, pos := pos })
+    pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
 
 def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
   let fileName := fileName.getD "<input>"
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index 4dc107fbd8..14ff6f7176 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -39,7 +39,7 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
     let endPos := ref.getTailPos?.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage { fileName := (← getFileName), rawPos := pos, pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
+    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
 
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
   logAt ref msgData MessageSeverity.error
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 5245df8149..4698888d79 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -169,7 +169,6 @@ end MessageData
 
 structure Message where
   fileName : String
-  rawPos   : Nat
   pos      : Position
   endPos   : Option Position := none
   severity : MessageSeverity := MessageSeverity.error
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 79e46315f5..9110222bfb 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -826,13 +826,13 @@ def getParamNames (declName : Name) : MetaM (Array Name) := do
 
 -- `kind` specifies the metavariable kind for metavariables not corresponding to instance implicit `[ ... ]` arguments.
 private partial def forallMetaTelescopeReducingAux
-    (e : Expr) (reducing : Bool) (maxMVars? : Option Nat) (kind : MetavarKind) (instsSynthetic : Bool) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+    (e : Expr) (reducing : Bool) (maxMVars? : Option Nat) (kind : MetavarKind) : MetaM (Array Expr × Array BinderInfo × Expr) :=
   let rec process (mvars : Array Expr) (bis : Array BinderInfo) (j : Nat) (type : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) := do
     match type with
     | Expr.forallE n d b c =>
       let cont : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
         let d  := d.instantiateRevRange j mvars.size mvars
-        let k  := if c.binderInfo.isInstImplicit && instsSynthetic then MetavarKind.synthetic else kind
+        let k  := if c.binderInfo.isInstImplicit then  MetavarKind.synthetic else kind
         let mvar ← mkFreshExprMVar d k n
         let mvars := mvars.push mvar
         let bis   := bis.push c.binderInfo
@@ -859,16 +859,15 @@ private partial def forallMetaTelescopeReducingAux
 
 /-- Similar to `forallTelescope`, but creates metavariables instead of free variables. -/
 def forallMetaTelescope (e : Expr) (kind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
-  forallMetaTelescopeReducingAux e (reducing := false) (maxMVars? := none) (instsSynthetic := true) kind
+  forallMetaTelescopeReducingAux e (reducing := false) (maxMVars? := none) kind
 
 /-- Similar to `forallTelescopeReducing`, but creates metavariables instead of free variables. -/
 def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) (kind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
-  forallMetaTelescopeReducingAux e (reducing := true) maxMVars? kind (instsSynthetic := true)
+  forallMetaTelescopeReducingAux e (reducing := true) maxMVars? kind
 
-/-- Similar to `forallMetaTelescopeReducing`, stops constructing the telescope when
-  it reaches size `maxMVars`. -/
-def forallMetaBoundedTelescope (e : Expr) (maxMVars : Nat) (kind : MetavarKind := MetavarKind.natural) (instsSynthetic : Bool := true) : MetaM (Array Expr × Array BinderInfo × Expr) :=
-  forallMetaTelescopeReducingAux e (reducing := true) (maxMVars? := some maxMVars) (kind := kind) (instsSynthetic := instsSynthetic)
+/-- Similar to `forallMetaTelescopeReducing`, stops constructing the telescope when it reaches size `maxMVars`. -/
+def forallMetaBoundedTelescope (e : Expr) (maxMVars : Nat) (kind : MetavarKind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+  forallMetaTelescopeReducingAux e (reducing := true) (maxMVars? := some maxMVars) (kind := kind)
 
 /-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
 partial def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index a59ae1c630..f12cd4929f 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -33,9 +33,9 @@ structure ModuleParserState where
   recovering : Bool       := false
   deriving Inhabited
 
-private def mkErrorMessage (c : ParserContext) (rawPos : String.Pos) (errorMsg : String) : Message :=
-  let pos := c.fileMap.toPosition rawPos
-  { fileName := c.fileName, rawPos := rawPos, pos := pos, data := errorMsg }
+private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message :=
+  let pos := c.fileMap.toPosition pos
+  { fileName := c.fileName, pos := pos, data := errorMsg }
 
 def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do
   let dummyEnv ← mkEmptyEnvironment
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 9cb413f87e..2749d80a4d 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -114,9 +114,16 @@ def replaceLPsWithVars (e : Expr) : MetaM Expr := do
     | Level.param n .. => replaceMap.find! n
     | l => if !l.hasParam then some l else none
 
+def isDefEq (t s : Expr) : MetaM Bool := do
+  withTheReader Meta.Context (fun ctx => { ctx with config := { ctx.config with assignSyntheticOpaque := true }}) $
+    Meta.isDefEq t s
+
+def checkpointDefEq (t s : Expr) : MetaM Bool := do
+  Meta.checkpointDefEq (isDefEq t s) (mayPostpone := false)
+
 def tryUnify (t s : Expr) : MetaM Unit := do
   try
-    let r ← Meta.isExprDefEqAux t s
+    let r ← isDefEq t s
     if !r then
       trace[pp.analyze.tryUnify] "nonDefEq\n\n{fmt t}\n\n=?=\n\n{fmt s}\n"
     pure ()
@@ -168,7 +175,7 @@ partial def okBottomUp? (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
       | Expr.const .. =>
         let args := e.getAppArgs
         let fType ← replaceLPsWithVars (← inferType e.getAppFn)
-        let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType e.getAppArgs.size (instsSynthetic := false)
+        let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType e.getAppArgs.size
         for i in [:mvars.size] do
           if bInfos[i] == BinderInfo.instImplicit then
             inspectOutParams args[i] mvars[i]
@@ -249,7 +256,7 @@ where
 
   analyzeAppStaged (f : Expr) (args : Array Expr) : AnalyzeM Unit := do
     let fType ← replaceLPsWithVars (← inferType f)
-    let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType args.size (instsSynthetic := false)
+    let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType args.size
     let rest := args.extract mvars.size args.size
     let args := args.shrink mvars.size
 
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index fb124d7cbb..a4037fb021 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -164,7 +164,7 @@ section Initialization
         srcSearchPath := srcSearchPath ++ pkgSearchPath
       Elab.processHeader headerStx opts msgLog inputCtx
     catch e =>  -- should be from `leanpkg print-paths`
-      let msgs := MessageLog.empty.add { fileName := "<ignored>", rawPos := 0, pos := ⟨0, 0⟩, data := e.toString }
+      let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
       pure (← mkEmptyEnvironment, msgs)
     publishMessages m msgLog hOut
     let cmdState := Elab.Command.mkState headerEnv msgLog opts
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 049b3b1970..208f650721 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -113,7 +113,6 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
         messages := postCmdState.messages.add {
           fileName := inputCtx.fileName
           severity := MessageSeverity.information
-          rawPos   := snap.endPos
           pos      := inputCtx.fileMap.toPosition snap.endPos
           data     := output
         }