From efa5db197e19b473b9d681b36eec6aaac964e440 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Aug 2021 08:07:16 -0700
Subject: [PATCH] fix: position information for implicit type

---
 src/Lean/Elab/Binders.lean                   | 17 ++++++++---------
 tests/lean/holes.lean.expected.out           |  4 ++--
 tests/lean/implicitTypePos.lean              |  7 +++++++
 tests/lean/implicitTypePos.lean.expected.out |  5 +++++
 4 files changed, 22 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/implicitTypePos.lean
 create mode 100644 tests/lean/implicitTypePos.lean.expected.out

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 55b8bcedd2..7cbcca7433 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -107,25 +107,24 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
   if k == ``Lean.Parser.Term.simpleBinder then
     -- binderIdent+ >> optType
     let ids ← getBinderIds stx[0]
-    let type := expandOptType (mkNullNode ids) stx[1]
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
+    let optType := stx[1]
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandOptType id optType, bi := BinderInfo.default }
   else if k == ``Lean.Parser.Term.explicitBinder then
     -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
     let ids ← getBinderIds stx[1]
-    let type        := expandBinderType (mkNullNode ids) stx[2]
+    let type        := stx[2]
     let optModifier := stx[3]
-    let type ← expandBinderModifier type optModifier
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := BinderInfo.default }
   else if k == ``Lean.Parser.Term.implicitBinder then
     -- `{` binderIdent+ binderType `}`
     let ids ← getBinderIds stx[1]
-    let type := expandBinderType (mkNullNode ids) stx[2]
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.implicit }
+    let type := stx[2]
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := BinderInfo.implicit }
   else if k == ``Lean.Parser.Term.strictImplicitBinder then
     -- `⦃` binderIdent+ binderType `⦄`
     let ids ← getBinderIds stx[1]
-    let type := expandBinderType (mkNullNode ids) stx[2]
-    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.strictImplicit }
+    let type := stx[2]
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandBinderType id type, bi := BinderInfo.strictImplicit }
   else if k == ``Lean.Parser.Term.instBinder then
     -- `[` optIdent type `]`
     let id ← expandOptIdent stx[1]
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 136db189e8..5db8f6d4ee 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -20,7 +20,7 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
 context:
 x : Nat
 ⊢ Type
-holes.lean:13:8-13:11: error: failed to infer binder 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:19:0-19:3: error: don't know how to synthesize implicit argument
   @f Nat (?m _) a
@@ -28,6 +28,6 @@ context:
 a : Nat
 f : {α : Type} → {β : ?m a (α := α)} → α → α := fun {α} {β} a => a
 ⊢ ?m a (α := Nat)
-holes.lean:18:7-18:10: error: failed to infer binder type
+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:25:8-25:11: error: failed to infer 'let rec' declaration type
diff --git a/tests/lean/implicitTypePos.lean b/tests/lean/implicitTypePos.lean
new file mode 100644
index 0000000000..5e071e238e
--- /dev/null
+++ b/tests/lean/implicitTypePos.lean
@@ -0,0 +1,7 @@
+def f x y := 0
+
+def g (x y z) := 0 + x + z
+
+def h {α β} (a : α) := a
+
+def r {{α β}} (a : α) := a
diff --git a/tests/lean/implicitTypePos.lean.expected.out b/tests/lean/implicitTypePos.lean.expected.out
new file mode 100644
index 0000000000..67464413a8
--- /dev/null
+++ b/tests/lean/implicitTypePos.lean.expected.out
@@ -0,0 +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