feat: improve infer binder type failure message and range

Author: Kha

src/Lean/Elab/Binders.lean

@@ -175,9 +175,13 @@ private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
   else
     throwUnsupportedSyntax
 
-private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit := do
-  registerCustomErrorIfMVar type ref "failed to infer binder type"
-  registerLevelMVarErrorExprInfo type ref m!"failed to infer universe levels in binder type"
+private def registerFailedToInferBinderTypeInfo (type : Expr) (view : BinderView) : TermElabM Unit := do
+  let msg := if view.id.getId.hasMacroScopes then
+    m!"binder type"
+  else
+    m!"type of binder '{view.id.getId}'"
+  registerCustomErrorIfMVar type view.ref m!"Failed to infer {msg}"
+  registerLevelMVarErrorExprInfo type view.ref m!"Failed to infer universe levels in {msg}"
 
 def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit :=
   addTermInfo' (isBinder := true) stx fvar
@@ -209,7 +213,7 @@ private partial def elabBinderViews (binderViews : Array BinderView) (fvars : Ar
       let binderView := binderViews[i]
       ensureAtomicBinderName binderView
       let type ← elabType binderView.type
-      registerFailedToInferBinderTypeInfo type binderView.type
+      registerFailedToInferBinderTypeInfo type binderView
       if binderView.bi.isInstImplicit && checkBinderAnnotations.get (← getOptions) then
         unless (← isClass? type).isSome do
           throwErrorAt binderView.type "invalid binder annotation, type is not a class instance{indentExpr type}\nuse the command `set_option checkBinderAnnotations false` to disable the check"
@@ -420,7 +424,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
     ensureAtomicBinderName binderView
     withRef binderView.type <| withLCtx s.lctx s.localInsts do
       let type ← elabType binderView.type
-      registerFailedToInferBinderTypeInfo type binderView.type
+      registerFailedToInferBinderTypeInfo type binderView
       let fvarId ← mkFreshFVarId
       let fvar  := mkFVar fvarId
       let s     := { s with fvars := s.fvars.push fvar }

src/Lean/Elab/MutualDef.lean

@@ -89,8 +89,18 @@ 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) (view : DefView) :
+    TermElabM Unit :=
+  let ref := match view.kind with
+    | .example  => view.ref[0]
+    | .instance => view.ref[1]
+    | _         => view.declId
+  let msg := match view.kind with
+    | .example  => m!"example"
+    | .instance => m!"instance"
+    | .theorem  => m!"theorem '{view.declId}'"
+    | _         => m!"definition '{view.declId}'"
+  registerCustomErrorIfMVar type ref m!"Failed to infer type of {msg}"
 
 /--
   Return `some [b, c]` if the given `views` are representing a declaration of the form
@@ -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 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 view
                 pure type
             Term.synthesizeSyntheticMVarsNoPostponing
             if view.isInstance then

tests/lean/331.lean.expected.out

@@ -1,4 +1,4 @@
-331.lean:6:13-6:14: error: failed to infer binder type
+331.lean:6:9-6:10: error: Failed to infer type of binder 'x'
 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
+331.lean:7:9-7:10: error: Failed to infer type of binder 'x'
 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/autoImplicitCtorParamIssue.lean.expected.out

@@ -1,3 +1,3 @@
-autoImplicitCtorParamIssue.lean:1:9-1:10: error: failed to infer binder type
-autoImplicitCtorParamIssue.lean:4:9-4:10: error: failed to infer binder type
-autoImplicitCtorParamIssue.lean:7:7-7:8: error: failed to infer binder type
+autoImplicitCtorParamIssue.lean:1:9-1:10: error: Failed to infer type of binder 'x'
+autoImplicitCtorParamIssue.lean:4:9-4:10: error: Failed to infer type of binder 'x'
+autoImplicitCtorParamIssue.lean:7:7-7:8: error: Failed to infer type of binder 'x'

tests/lean/holeErrors.lean.expected.out

@@ -2,21 +2,21 @@ 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
+holeErrors.lean:3:4-3:10: error: Failed to infer type of definition 'f1.{u}'
+holeErrors.lean:5:4-5:6: error: Failed to infer type of definition 'f2'
 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: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: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:7:4-7:10: error: Failed to infer type of definition 'f3.{u}'
+holeErrors.lean:11:4-11:6: error: Failed to infer type of definition 'f4'
+holeErrors.lean:11:8-11:9: error: Failed to infer type of binder 'x'
+holeErrors.lean:13:4-13:6: error: Failed to infer type of definition 'f5'
+holeErrors.lean:13:8-13:9: error: Failed to infer type of binder 'x'
+holeErrors.lean:16:4-16:5: error: Failed to infer type of binder 'x'
+holeErrors.lean:15:4-15:6: error: Failed to infer type of definition '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

@@ -20,14 +20,14 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument 'β
 context:
 x : Nat
 ⊢ Type
-holes.lean:13:10-13:11: error: failed to infer binder type
-holes.lean:15:16-15:17: error: failed to infer binder type
+holes.lean:13:10-13:11: error: Failed to infer type of binder 'β'
+holes.lean:15:12-15:13: error: Failed to infer type of binder 'β'
 holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument 'β'
   @f Nat (?m a) a
 context:
 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:18:9-18:10: error: Failed to infer type of binder 'β'
+holes.lean:21:12-21:14: error: Failed to infer type of definition 'f7'
 holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type

tests/lean/implicitTypePos.lean.expected.out

@@ -1,5 +1,5 @@
-implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
-implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
-implicitTypePos.lean:3:9-3:10: error: failed to infer binder type
-implicitTypePos.lean:5:9-5:10: error: failed to infer binder type
-implicitTypePos.lean:7:10-7:11: error: failed to infer binder type
+implicitTypePos.lean:1:8-1:9: error: Failed to infer type of binder 'y'
+implicitTypePos.lean:1:6-1:7: error: Failed to infer type of binder 'x'
+implicitTypePos.lean:3:9-3:10: error: Failed to infer type of binder 'y'
+implicitTypePos.lean:5:9-5:10: error: Failed to infer type of binder 'β'
+implicitTypePos.lean:7:10-7:11: error: Failed to infer type of binder 'β'

tests/lean/interactive/2058.lean.expected.out

@@ -14,12 +14,13 @@
   {"source": "Lean 4",
    "severity": 1,
    "range":
-   {"start": {"line": 21, "character": 26},
-    "end": {"line": 21, "character": 31}},
-   "message": "failed to infer universe levels in binder type\n  PUnit.{_}",
+   {"start": {"line": 21, "character": 22},
+    "end": {"line": 21, "character": 23}},
+   "message":
+   "Failed to infer universe levels in type of binder 'x'\n  PUnit.{_}",
    "fullRange":
-   {"start": {"line": 21, "character": 26},
-    "end": {"line": 21, "character": 31}}},
+   {"start": {"line": 21, "character": 22},
+    "end": {"line": 21, "character": 23}}},
   {"source": "Lean 4",
    "severity": 1,
    "range":

tests/lean/multiConstantError.lean.expected.out

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

tests/lean/run/2058.lean

@@ -64,7 +64,7 @@ Test: Works for `fun` binders.
 -/
 
 /--
-error: failed to infer universe levels in binder type
+error: Failed to infer universe levels in type of binder 'x'
   PUnit.{_}
 -/
 #guard_msgs in

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 definition '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/forInColErr.lean

@@ -21,7 +21,7 @@ error: don't know how to synthesize implicit argument 'ρ'
 context:
 ⊢ Type _
 ---
-error: failed to infer binder type
+error: Failed to infer type of binder 'x'
 ---
 error: don't know how to synthesize implicit argument 'α'
   @List.nil ?_
@@ -63,9 +63,9 @@ error: don't know how to synthesize implicit argument 'ρ'
 context:
 ⊢ Type _
 ---
-error: failed to infer binder type
+error: Failed to infer type of binder 'h'
 ---
-error: failed to infer binder type
+error: Failed to infer type of binder 'x'
 ---
 error: don't know how to synthesize implicit argument 'α'
   @List.nil ?_

tests/lean/run/inferTypeFailure.lean

@@ -0,0 +1,36 @@
+/-! Check messages of binder type inference failures. -/
+
+/--
+error: Failed to infer type of binder 'y'
+---
+error: Failed to infer type of binder 'x'
+---
+error: Failed to infer type of definition 'l1'
+-/
+#guard_msgs in
+def l1 := fun x y => x
+
+/--
+error: Failed to infer binder type
+---
+error: Failed to infer type of definition 'l2'
+-/
+#guard_msgs in
+def l2 := fun _ => 0
+
+/--
+error: Failed to infer type of theorem 't'
+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
+---
+error: type of theorem 't' is not a proposition
+  ?m.65
+-/
+#guard_msgs in
+theorem t : _ := _
+
+/--
+error: Failed to infer type of example
+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 in
+example : _ := _

tests/lean/run/structBinderUpdates.lean

@@ -118,7 +118,7 @@ end Ex4
 Here, `(α β)` is not an override since `β` is not an existing parameter, so `α` is treated as a binder.
 -/
 namespace Ex5
-/-- error: failed to infer binder type -/
+/-- error: Failed to infer type of binder 'α' -/
 #guard_msgs in
 class C (α : Type) where
   f (α β) : β
@@ -128,7 +128,7 @@ end Ex5
 Here, `(α β)` is not an override since `β` is a field.
 -/
 namespace Ex6
-/-- error: failed to infer binder type -/
+/-- error: Failed to infer type of binder 'α' -/
 #guard_msgs in
 class C (α : Type) where
   β : Type