From 40c8db7494adccfbc9fb35920b91b65dc1b6df3f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Apr 2022 16:28:46 -0700
Subject: [PATCH] feat: improve argument type mismatch error position, and do
 not stop at application type mismatch errors

---
 src/Lean/Elab/App.lean                        | 16 +++++++++++----
 src/Lean/Elab/Term.lean                       |  2 +-
 tests/lean/243.lean.expected.out              |  4 ++--
 tests/lean/283.lean.expected.out              |  2 +-
 tests/lean/389.lean.expected.out              |  2 +-
 tests/lean/423.lean.expected.out              |  4 ++--
 tests/lean/439.lean.expected.out              |  2 +-
 tests/lean/autoPPExplicit.lean.expected.out   |  2 +-
 tests/lean/doIssue.lean.expected.out          |  2 +-
 tests/lean/elseifDoErrorPos.lean.expected.out |  8 ++++++++
 tests/lean/evalSorry.lean.expected.out        |  2 +-
 tests/lean/modBug.lean.expected.out           |  2 +-
 .../mulcommErrorMessage.lean.expected.out     |  2 +-
 tests/lean/nameArgErrorIssue.lean             |  7 +++++++
 .../lean/nameArgErrorIssue.lean.expected.out  | 20 +++++++++++++++++++
 tests/lean/namedHoles.lean.expected.out       |  3 ++-
 .../phashmap_inst_coherence.lean.expected.out |  3 ++-
 tests/lean/scopedunifhint.lean.expected.out   | 10 +++++-----
 .../simpArgTypeMismatch.lean.expected.out     |  2 +-
 tests/lean/sorryAtError.lean.expected.out     |  2 +-
 20 files changed, 71 insertions(+), 26 deletions(-)
 create mode 100644 tests/lean/nameArgErrorIssue.lean
 create mode 100644 tests/lean/nameArgErrorIssue.lean.expected.out

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 780f0aebbe..e81ea91ebf 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -34,7 +34,15 @@ def throwInvalidNamedArg {α} (namedArg : NamedArg) (fn? : Option Name) : TermEl
 
 private def ensureArgType (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do
   let argType ← inferType arg
-  ensureHasTypeAux expectedType argType arg f
+  try
+    ensureHasTypeAux expectedType argType arg f
+  catch
+    | ex@(Exception.error ..) =>
+      if (← read).errToSorry then
+        exceptionToSorry ex expectedType
+      else
+        throw ex
+    | ex => throw ex
 
 private def mkProjAndCheck (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
   let r := mkProj structName idx e
@@ -168,9 +176,9 @@ private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do
   | Arg.expr val =>
     let arg ← ensureArgType s.f val expectedType
     addNewArg argName arg
-  | Arg.stx val  =>
-    let val ← elabTerm val expectedType
-    let arg ← ensureArgType s.f val expectedType
+  | Arg.stx stx  =>
+    let val ← elabTerm stx expectedType
+    let arg ← withRef stx <| ensureArgType s.f val expectedType
     addNewArg argName arg
 
 /- Return true if the given type contains `OptParam` or `AutoParams` -/
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index ae5bfb63ab..48cedfed52 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -921,7 +921,7 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr :
     | some expectedType => pure expectedType
   mkSyntheticSorry expectedType
 
-private def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
+def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
   let syntheticSorry ← mkSyntheticSorryFor expectedType?
   logException ex
   pure syntheticSorry
diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out
index 43b4d5473d..86368e12cf 100644
--- a/tests/lean/243.lean.expected.out
+++ b/tests/lean/243.lean.expected.out
@@ -1,4 +1,4 @@
-243.lean:2:3-2:14: error: application type mismatch
+243.lean:2:10-2:14: error: application type mismatch
   { fst := Bool, snd := true }
 argument
   true
@@ -6,7 +6,7 @@ has type
   _root_.Bool : Type
 but is expected to have type
   Bool : Type
-243.lean:13:3-13:8: error: application type mismatch
+243.lean:13:7-13:8: error: application type mismatch
   { fst := A, snd := a }
 argument
   a
diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index 2490e69737..7a45c17bbd 100644
--- a/tests/lean/283.lean.expected.out
+++ b/tests/lean/283.lean.expected.out
@@ -1,4 +1,4 @@
-283.lean:1:22-1:25: error: application type mismatch
+283.lean:1:24-1:25: error: application type mismatch
   f (f ?m)
 argument
   f ?m
diff --git a/tests/lean/389.lean.expected.out b/tests/lean/389.lean.expected.out
index ce7f012f50..c8e6f24faf 100644
--- a/tests/lean/389.lean.expected.out
+++ b/tests/lean/389.lean.expected.out
@@ -1,4 +1,4 @@
-389.lean:7:7-7:17: error: application type mismatch
+389.lean:7:14-7:17: error: application type mismatch
   getFoo bar
 argument
   bar
diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out
index cf53fe9a00..b5b3f96970 100644
--- a/tests/lean/423.lean.expected.out
+++ b/tests/lean/423.lean.expected.out
@@ -4,7 +4,7 @@ has type
   Nat : Type
 but is expected to have type
   T : Sort u
-423.lean:5:33-5:38: error: application type mismatch
+423.lean:5:37-5:38: error: application type mismatch
   Add T
 argument
   T
@@ -12,7 +12,7 @@ has type
   Sort u : Type u
 but is expected to have type
   Type ?u : Type (?u + 1)
-423.lean:5:41-5:50: error: application type mismatch
+423.lean:5:47-5:48: error: application type mismatch
   OfNat T
 argument
   T
diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out
index 5bdbaf3fc4..5f8286b80b 100644
--- a/tests/lean/439.lean.expected.out
+++ b/tests/lean/439.lean.expected.out
@@ -9,7 +9,7 @@ term has type
   Bar.fn ?m
 Fn.imp fn : Bar.fn p
 Fn.imp fn' Bp : Bar.fn p
-439.lean:41:7-41:12: error: application type mismatch
+439.lean:41:11-41:12: error: application type mismatch
   Fn.imp fn' p
 argument
   p
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 858b52c943..445a458daa 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -1,4 +1,4 @@
-autoPPExplicit.lean:2:2-2:32: error: application type mismatch
+autoPPExplicit.lean:2:26-2:31: error: application type mismatch
   @Eq.trans α a (b = c)
 argument
   b = c
diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out
index d59f9e7ddb..b7963f5738 100644
--- a/tests/lean/doIssue.lean.expected.out
+++ b/tests/lean/doIssue.lean.expected.out
@@ -10,7 +10,7 @@ has type
   Array Nat : Type
 but is expected to have type
   IO PUnit : Type
-doIssue.lean:18:2-18:20: error: application type mismatch
+doIssue.lean:18:7-18:20: error: application type mismatch
   pure (Array.set! xs 0 1)
 argument
   Array.set! xs 0 1
diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out
index 87c5f1ad9a..178b7d6458 100644
--- a/tests/lean/elseifDoErrorPos.lean.expected.out
+++ b/tests/lean/elseifDoErrorPos.lean.expected.out
@@ -6,3 +6,11 @@ has type
   Nat : Type
 but is expected to have type
   Prop : Type
+elseifDoErrorPos.lean:7:11-7:14: error: application type mismatch
+  pure "a"
+argument
+  "a"
+has type
+  String : Type
+but is expected to have type
+  Nat : Type
diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out
index 984c2973ca..d3e1a027ea 100644
--- a/tests/lean/evalSorry.lean.expected.out
+++ b/tests/lean/evalSorry.lean.expected.out
@@ -1,5 +1,5 @@
 1
-evalSorry.lean:5:31-5:34: error: application type mismatch
+evalSorry.lean:5:33-5:34: error: application type mismatch
   f x
 argument
   x
diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out
index 21c207da61..9bee5bd5bb 100644
--- a/tests/lean/modBug.lean.expected.out
+++ b/tests/lean/modBug.lean.expected.out
@@ -1,4 +1,4 @@
-modBug.lean:1:32-1:64: error: application type mismatch
+modBug.lean:1:48-1:64: error: application type mismatch
   Nat.zero_ne_one (Nat.mod_zero 1)
 argument
   Nat.mod_zero 1
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index 0c9dae32ba..a3e3749dc2 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -24,7 +24,7 @@ the following variables have been introduced by the implicit lamda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
-mulcommErrorMessage.lean:16:12-17:47: error: application type mismatch
+mulcommErrorMessage.lean:17:27-17:47: error: application type mismatch
   Bool.casesOn a ?m (Bool.casesOn b ?m ?m)
 argument
   Bool.casesOn b ?m ?m
diff --git a/tests/lean/nameArgErrorIssue.lean b/tests/lean/nameArgErrorIssue.lean
new file mode 100644
index 0000000000..f33d644abe
--- /dev/null
+++ b/tests/lean/nameArgErrorIssue.lean
@@ -0,0 +1,7 @@
+def boo (x : Nat) (y : Nat) := x + y
+def bla (x : Nat) := boo x
+
+#check bla (y := 2) 5     -- Ok
+#check bla (y := 5) "hi"  -- 1 error at "hi"
+#check bla (z := 5) "hi"  -- 2 errors at `(z := 5)` and "hi"
+#check bla (z := 5) 2     -- 1 errors at `(z := 5)`
diff --git a/tests/lean/nameArgErrorIssue.lean.expected.out b/tests/lean/nameArgErrorIssue.lean.expected.out
new file mode 100644
index 0000000000..13f3fa9776
--- /dev/null
+++ b/tests/lean/nameArgErrorIssue.lean.expected.out
@@ -0,0 +1,20 @@
+bla 5 2 : Nat
+nameArgErrorIssue.lean:5:20-5:24: error: application type mismatch
+  bla "hi"
+argument
+  "hi"
+has type
+  String : Type
+but is expected to have type
+  Nat : Type
+bla (sorryAx Nat) 5 : Nat
+nameArgErrorIssue.lean:6:20-6:24: error: application type mismatch
+  bla "hi"
+argument
+  "hi"
+has type
+  String : Type
+but is expected to have type
+  Nat : Type
+nameArgErrorIssue.lean:6:11-6:19: error: invalid argument name 'z' for function 'bla'
+nameArgErrorIssue.lean:7:11-7:19: error: invalid argument name 'z' for function 'bla'
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index 6fa4e3f9df..911fff47d0 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -1,4 +1,4 @@
-namedHoles.lean:9:7-9:14: error: application type mismatch
+namedHoles.lean:9:12-9:14: error: application type mismatch
   f ?x ?x
 argument
   ?x
@@ -6,6 +6,7 @@ has type
   Nat : Type
 but is expected to have type
   Bool : Type
+f ?x (sorryAx Bool) : Nat
 g ?x ?x : Nat
 20
 foo (fun x => ?m x) ?hole : Nat
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 548fafe221..201a304788 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -1,4 +1,4 @@
-phashmap_inst_coherence.lean:12:6-12:56: error: application type mismatch
+phashmap_inst_coherence.lean:12:53-12:54: error: application type mismatch
   PersistentHashMap.find? m
 argument
   m
@@ -6,3 +6,4 @@ has type
   @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type
 but is expected to have type
   @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type
+phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out
index 5b73b5eb90..ca2f50d4bc 100644
--- a/tests/lean/scopedunifhint.lean.expected.out
+++ b/tests/lean/scopedunifhint.lean.expected.out
@@ -1,4 +1,4 @@
-scopedunifhint.lean:28:7-28:14: error: application type mismatch
+scopedunifhint.lean:28:13-28:14: error: application type mismatch
   mul ?m x
 argument
   x
@@ -6,7 +6,7 @@ has type
   Nat : Type
 but is expected to have type
   ?m.α : Type ?u
-scopedunifhint.lean:29:7-29:24: error: application type mismatch
+scopedunifhint.lean:29:18-29:24: error: application type mismatch
   mul ?m (x, x)
 argument
   (x, x)
@@ -14,7 +14,7 @@ has type
   Nat × Nat : Type
 but is expected to have type
   ?m.α : Type ?u
-scopedunifhint.lean:33:7-33:10: error: application type mismatch
+scopedunifhint.lean:33:9-33:10: error: application type mismatch
   ?m*x
 argument
   x
@@ -24,7 +24,7 @@ but is expected to have type
   ?m.α : Type ?u
 x*x : Nat.Magma.α
 x*x : Nat.Magma.α
-scopedunifhint.lean:39:7-39:24: error: application type mismatch
+scopedunifhint.lean:39:18-39:24: error: application type mismatch
   ?m*(x, x)
 argument
   (x, x)
@@ -33,7 +33,7 @@ has type
 but is expected to have type
   ?m.α : Type ?u
 (x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
-scopedunifhint.lean:56:7-56:22: error: application type mismatch
+scopedunifhint.lean:56:16-56:22: error: application type mismatch
   ?m*(x, x)
 argument
   (x, x)
diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out
index bad66bda4b..1e471a675c 100644
--- a/tests/lean/simpArgTypeMismatch.lean.expected.out
+++ b/tests/lean/simpArgTypeMismatch.lean.expected.out
@@ -1,4 +1,4 @@
-simpArgTypeMismatch.lean:3:13-3:33: error: application type mismatch
+simpArgTypeMismatch.lean:3:29-3:33: error: application type mismatch
   decide_eq_false Unit
 argument
   Unit
diff --git a/tests/lean/sorryAtError.lean.expected.out b/tests/lean/sorryAtError.lean.expected.out
index a0c5b3ded5..b71549c1c6 100644
--- a/tests/lean/sorryAtError.lean.expected.out
+++ b/tests/lean/sorryAtError.lean.expected.out
@@ -1,4 +1,4 @@
-sorryAtError.lean:13:40-13:47: error: application type mismatch
+sorryAtError.lean:13:46-13:47: error: application type mismatch
   Ty.ty ty Γ
 argument
   Γ