feat: improve error message

closes #331

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,

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

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

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

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:

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