diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 1f960cd7da..68f83a33f5 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -237,7 +237,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
     if checkTraceOption (← getOptions) `Elab.info then
       logTrace `Elab.info m!"{← tree.format}"
     return tree
-  let initMsgs := (← get).messages
+  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
   withLogging <| withRef stx <| withInfoTreeContext (mkInfoTree := mkInfoTree) <| withIncRecDepth <| withFreshMacroScope do
     runLinters stx
     match stx with
@@ -261,10 +261,13 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
           | some elabFns => elabCommandUsing s stx elabFns
           | none         => throwError "elaboration function for '{k}' has not been implemented"
     | _ => throwError "unexpected command"
+  let mut msgs ← (← get).messages
   -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
   if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
-    -- discard elaboration errors on parse error
-    modify ({ · with messages := initMsgs})
+    -- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error
+    msgs := ⟨msgs.msgs.filter fun msg =>
+      msg.data.hasTag `Elab.synthPlaceholder || msg.data.hasTag `Tactic.unsolvedGoals⟩
+  modify ({ · with messages := initMsgs ++ msgs })
 
 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
 def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab := fun stx => do
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index e05790da44..4da4516018 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -23,7 +23,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
 
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit :=
   withPPInaccessibleNames do
-    throwError "unsolved goals\n{goalsToMessageData goals}"
+    throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{goalsToMessageData goals}"
 
 namespace Tactic
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 8321f112ad..7a37fa96a9 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -439,7 +439,7 @@ def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option M
   | MVarErrorKind.hole => do
     let msg : MessageData := "don't know how to synthesize placeholder"
     let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
-    logErrorAt mvarErrorInfo.ref (appendExtra msg)
+    logErrorAt mvarErrorInfo.ref (MessageData.tagged `Elab.synthPlaceholder <| appendExtra msg)
   | MVarErrorKind.custom msg =>
     logErrorAt mvarErrorInfo.ref (appendExtra msg)
 where
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 1f975cd899..186b9200ae 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -77,6 +77,17 @@ where
     | node msgs                 => node <| msgs.map (visit . mctx)
     | _                         => msg
 
+variable (tag : Name) in
+partial def hasTag : MessageData → Bool
+  | withContext _ msg       => hasTag msg
+  | withNamingContext _ msg => hasTag msg
+  | nest _ msg              => hasTag msg
+  | group msg               => hasTag msg
+  | compose msg₁ msg₂       => hasTag msg₁ || hasTag msg₂
+  | tagged n msg            => tag == n || hasTag msg
+  | node msgs               => msgs.any hasTag
+  | _                       => false
+
 def nil : MessageData :=
   ofFormat Format.nil
 
diff --git a/tests/lean/have.lean b/tests/lean/have.lean
new file mode 100644
index 0000000000..a912c22107
--- /dev/null
+++ b/tests/lean/have.lean
@@ -0,0 +1,2 @@
+example : False :=
+  have False := _
diff --git a/tests/lean/have.lean.expected.out b/tests/lean/have.lean.expected.out
new file mode 100644
index 0000000000..8990ee34bb
--- /dev/null
+++ b/tests/lean/have.lean.expected.out
@@ -0,0 +1,4 @@
+have.lean:3:0: error: unexpected end of input
+have.lean:2:16-2:17: error: don't know how to synthesize placeholder
+context:
+⊢ False
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
index da22471d63..e9e743df06 100644
--- a/tests/lean/unknownTactic.lean.expected.out
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -1,5 +1,15 @@
 unknownTactic.lean:3:3: error: unknown tactic
+unknownTactic.lean:1:41-3:8: error: unsolved goals
+x : Nat
+a✝ : x = x
+⊢ x = x
 ---
 unknownTactic.lean:8:17: error: unknown tactic
+unknownTactic.lean:8:2-8:19: error: unsolved goals
+x : Nat
+⊢ x = x
 ---
 unknownTactic.lean:14:17: error: unknown tactic
+unknownTactic.lean:14:2-14:19: error: unsolved goals
+x : Nat
+⊢ x = x