feat: improve error message position for binders with implicit types

src/Lean/Elab/Binders.lean

@@ -17,9 +17,9 @@ open Meta
     a) (`:` term)?
     b) `:` term
   return `term` if it is present, or a hole if not. -/
-private def expandBinderType (stx : Syntax) : Syntax :=
+private def expandBinderType (ref : Syntax) (stx : Syntax) : Syntax :=
 if stx.getNumArgs == 0 then
-  mkHole stx
+  mkHole ref
 else
   stx.getArg 1
 
@@ -108,14 +108,14 @@ match stx with
   else if k == `Lean.Parser.Term.explicitBinder then do
     -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
     ids ← getBinderIds (args.get! 1);
-    let type        := expandBinderType (args.get! 2);
+    let type        := expandBinderType stx (args.get! 2);
     let optModifier := args.get! 3;
     type ← expandBinderModifier type optModifier;
     ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
   else if k == `Lean.Parser.Term.implicitBinder then do
     -- `{` binderIdent+ binderType `}`
     ids ← getBinderIds (args.get! 1);
-    let type := expandBinderType (args.get! 2);
+    let type := expandBinderType stx (args.get! 2);
     ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.implicit }
   else if k == `Lean.Parser.Term.instBinder then do
     -- `[` optIdent type `]`

tests/lean/holes.lean

@@ -9,3 +9,11 @@ a
 def f3 (x : Nat) : Nat :=
 let y := g x + g x;
 y + _ + ?hole
+
+def f4 {α β} (a : α) := a
+
+def f5 {α} {β : _} (a : α) := a
+
+def f6 (a : Nat) :=
+let f {α β} (a : α) := a;
+f a

tests/lean/holes.lean.expected.out

@@ -24,3 +24,24 @@ context:
 f3 : Nat → Nat
 x : Nat
 ⊢ Type
+holes.lean:13:7: error: don't know how to synthesize placeholder
+context:
+α : Sort u_1
+⊢ Sort ?
+holes.lean:15:16: error: don't know how to synthesize placeholder
+context:
+α : Sort u_1
+⊢ Sort ?
+holes.lean:19:0: error: don't know how to synthesize placeholder
+  @_uniq.114 … ?m.122 …
+context:
+f6 : Nat → Nat
+a : Nat
+f : ∀ {α : Type} {β : ?m.121 a}, α → α := fun {α : Type} {β : ?m.121 a} (a : α) => a
+⊢ ?m.121 a
+holes.lean:18:6: error: don't know how to synthesize placeholder
+context:
+f6 : Nat → Nat
+a : Nat
+α : Type
+⊢ Sort ?