chore: fix tests

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Elab/MutualDef.lean

@@ -89,8 +89,15 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl
   else
     pure ()
 
-private def registerFailedToInferDefTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
-  registerCustomErrorIfMVar type ref "failed to infer definition type"
+private def registerFailedToInferDefTypeInfo (type : Expr) (ref : Syntax) (view : DefView) : TermElabM Unit :=
+  let msg := if view.kind.isExample then
+    m!"failed to infer type of example"
+  else if view.kind matches .instance then
+    -- TODO: instances are sometime named. We should probably include the name if available.
+    m!"failed to infer type of instance"
+  else
+    m!"failed to infer type of `{view.declId}`"
+  registerCustomErrorIfMVar type ref msg
 
 /--
   Return `some [b, c]` if the given `views` are representing a declaration of the form
@@ -106,14 +113,17 @@ private def isMultiConstant? (views : Array DefView) : Option (List Name) :=
   else
     none
 
-private def getPendingMVarErrorMessage (views : Array DefView) : String :=
+private def getPendingMVarErrorMessage (views : Array DefView) : MessageData :=
   match isMultiConstant? views with
   | some ids =>
     let idsStr := ", ".intercalate <| ids.map fun id => s!"`{id}`"
     let paramsStr := ", ".intercalate <| ids.map fun id => s!"`({id} : _)`"
-    s!"\nrecall that you cannot declare multiple constants in a single declaration. The identifier(s) {idsStr} are being interpreted as parameters {paramsStr}"
+    MessageData.note m!"Recall that you cannot declare multiple constants in a single declaration. The identifier(s) {idsStr} are being interpreted as parameters {paramsStr}."
   | none =>
-    "\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"
+    if views.all fun view => view.kind.isTheorem then
+      MessageData.note "All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be"
+    else
+      MessageData.note "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"
 
 /--
 Convert terms of the form `OfNat <type> (OfNat.ofNat Nat <num> ..)` into `OfNat <type> <num>`.
@@ -188,13 +198,13 @@ private def elabHeaders (views : Array DefView) (expandedDeclIds : Array ExpandD
             let mut type ← match view.type? with
               | some typeStx =>
                 let type ← elabType typeStx
-                registerFailedToInferDefTypeInfo type typeStx
+                registerFailedToInferDefTypeInfo type typeStx view
                 pure type
               | none =>
                 let hole := mkHole refForElabFunType
                 let type ← elabType hole
                 trace[Elab.definition] ">> type: {type}\n{type.mvarId!}"
-                registerFailedToInferDefTypeInfo type refForElabFunType
+                registerFailedToInferDefTypeInfo type refForElabFunType view
                 pure type
             Term.synthesizeSyntheticMVarsNoPostponing
             if view.isInstance then

tests/lean/331.lean.expected.out

@@ -1,4 +1,6 @@
 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
+
+Note: 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
 331.lean:7:13-7: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
+
+Note: 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

@@ -2,21 +2,22 @@ holeErrors.lean:3:14-3:20: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
-holeErrors.lean:3:11-3:20: 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:3:11-3:20: error: failed to infer type of `f1.{u}`
+holeErrors.lean:5:9-5:10: error: failed to infer type of `f2`
+
+Note: 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:15: error: don't know how to synthesize implicit argument 'α'
   @id ?m
 context:
 ⊢ Sort u
 holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
-holeErrors.lean:7:11-9:1: error: failed to infer definition type
-holeErrors.lean:11:11-11:15: error: failed to infer definition type
+holeErrors.lean:7:11-9:1: error: failed to infer type of `f3.{u}`
+holeErrors.lean:11:11-11:15: error: failed to infer type of `f4`
 holeErrors.lean:11:8-11:9: error: failed to infer binder type
-holeErrors.lean:13:15-13:19: error: failed to infer definition type
+holeErrors.lean:13:15-13:19: error: failed to infer type of `f5`
 holeErrors.lean:13:12-13:13: error: failed to infer binder type
 holeErrors.lean:16:4-16:5: error: failed to infer binder type
-holeErrors.lean:15:7-16:10: error: failed to infer definition type
+holeErrors.lean:15:7-16:10: error: failed to infer type of `f6`
 holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument 'α'
   @id ?m
 context:

tests/lean/holes.lean.expected.out

@@ -29,5 +29,5 @@ a : Nat
 f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a
 ⊢ ?m a
 holes.lean:18:9-18:10: error: failed to infer binder type
-holes.lean:21:25-22:4: error: failed to infer definition type
+holes.lean:21:25-22:4: error: failed to infer type of `f7`
 holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type

tests/lean/multiConstantError.lean.expected.out

@@ -1,6 +1,9 @@
 multiConstantError.lean:1:11-1:12: error: failed to infer binder type
-recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
+
+Note: Recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`.
 multiConstantError.lean:1:9-1:10: error: failed to infer binder type
-recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
+
+Note: Recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`.
 multiConstantError.lean:3:9-3:10: error: failed to infer binder type
-recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`
+
+Note: Recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`.

tests/lean/run/2226.lean

@@ -6,7 +6,7 @@ A : Nat
 #guard_msgs in
 variable (A : Nat) (B : by skip)
 
-/-- error: failed to infer definition type -/
+/-- error: failed to infer type of `foo` -/
 #guard_msgs in
 def foo :=
   A = B

tests/lean/run/5475.lean

@@ -16,7 +16,7 @@ error: don't know how to synthesize implicit argument 'α'
 context:
 ⊢ Type
 ---
-error: failed to infer definition type
+error: failed to infer type of example
 -/
 #guard_msgs in
 example :=

tests/lean/run/type_as_hole.lean

@@ -0,0 +1,38 @@
+/--
+error: failed to infer type of `foo`
+
+Note: All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be
+---
+error: type of theorem 'foo' is not a proposition
+  ?m.2
+-/
+#guard_msgs (error) in
+theorem foo : _ :=
+  sorry
+
+/--
+error: failed to infer type of example
+
+Note: 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
+-/
+#guard_msgs (error) in
+example : _ :=
+  sorry
+
+/--
+error: failed to infer type of `boo`
+
+Note: 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
+-/
+#guard_msgs (error) in
+def boo : _ :=
+  sorry
+
+/--
+error: failed to infer type of instance
+
+Note: 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
+-/
+#guard_msgs (error) in
+instance boo : _ :=
+  sorry

tests/lean/theoremType.lean.expected.out

@@ -1,8 +1,10 @@
 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
+
+Note: All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be
 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
+
+Note: 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