diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 2d6cfe66d7..79510a8037 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -106,7 +106,8 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe
               Term.synthesizeSyntheticMVarsNoPostponing
               type ← instantiateMVars type
               let pendingMVarIds ← getMVars type
-              discard <| logUnassignedUsingErrorInfos pendingMVarIds
+              discard <| logUnassignedUsingErrorInfos pendingMVarIds <|
+                m!"\nwhen the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed"
             let newHeader := {
               ref           := view.ref,
               modifiers     := view.modifiers,
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 387273e5cb..2bcc423290 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -398,20 +398,24 @@ def throwMVarError {α} (m : MessageData) : TermElabM α := do
   else
     throwError! m
 
-def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := do
+def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option MessageData) : TermElabM Unit := do
   match mvarErrorInfo.kind with
   | MVarErrorKind.implicitArg app => do
     let app ← instantiateMVars app
     let msg : MessageData := m!"don't know how to synthesize implicit argument{indentExpr app.setAppPPExplicit}"
     let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
-    logErrorAt mvarErrorInfo.ref msg
+    logErrorAt mvarErrorInfo.ref (appendExtra msg)
   | 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 msg
-  | MVarErrorKind.custom msgData =>
-    logErrorAt mvarErrorInfo.ref msgData
-
+    logErrorAt mvarErrorInfo.ref (appendExtra msg)
+  | MVarErrorKind.custom msg =>
+    logErrorAt mvarErrorInfo.ref (appendExtra msg)
+where
+  appendExtra (msg : MessageData) : MessageData :=
+    match extraMsg? with
+    | none => msg
+    | some extraMsg => msg ++ extraMsg
 
 /--
   Try to log errors for the unassigned metavariables `pendingMVarIds`.
@@ -420,7 +424,7 @@ def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := d
   TODO: try to fill "all" holes using synthetic "sorry's"
 
   Remark: We only log the "unfilled holes" as new errors if no error has been logged so far. -/
-def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) : TermElabM Bool := do
+def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Option MessageData := none) : TermElabM Bool := do
   let s ← get
   let hasOtherErrors := s.messages.hasErrors
   let mut hasNewErrors := false
@@ -435,7 +439,7 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) : TermElabM Boo
         let mvarDeps ← getMVars (mkMVar mvarId)
         if mvarDeps.any pendingMVarIds.contains then do
           unless hasOtherErrors do
-            mvarErrorInfo.logError
+            mvarErrorInfo.logError extraMsg?
           pure true
         else
           pure false
diff --git a/tests/lean/331.lean b/tests/lean/331.lean
new file mode 100644
index 0000000000..a35c1d53bc
--- /dev/null
+++ b/tests/lean/331.lean
@@ -0,0 +1,6 @@
+structure Foo where
+  foo : Nat
+
+def baz {x : _} := Foo.mk x -- works fine
+
+def qux {x : _} : Foo := Foo.mk x
diff --git a/tests/lean/331.lean.expected.out b/tests/lean/331.lean.expected.out
new file mode 100644
index 0000000000..5728502d1c
--- /dev/null
+++ b/tests/lean/331.lean.expected.out
@@ -0,0 +1,2 @@
+331.lean:6:13-6:14: error: failed to infer binder type
+when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
index a408f2bbdf..381a35b9ef 100644
--- a/tests/lean/holeErrors.lean.expected.out
+++ b/tests/lean/holeErrors.lean.expected.out
@@ -4,6 +4,7 @@ context:
 ⊢ Sort u_1
 holeErrors.lean:3:7-3:12: error: failed to infer definition type
 holeErrors.lean:5:9-5:10: error: failed to infer definition type
+when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
 holeErrors.lean:8:9-8:11: error: don't know how to synthesize implicit argument
   @id ?m
 context:
diff --git a/tests/lean/theoremType.lean.expected.out b/tests/lean/theoremType.lean.expected.out
index 2a843b34ec..6cef68f8cd 100644
--- a/tests/lean/theoremType.lean.expected.out
+++ b/tests/lean/theoremType.lean.expected.out
@@ -1,6 +1,8 @@
 theoremType.lean:1:22-1:23: error: don't know how to synthesize placeholder
 context:
 ⊢ Nat
+when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
 theoremType.lean:4:18-4:19: error: don't know how to synthesize placeholder
 context:
 ⊢ Nat
+when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed