feat: improve argument type mismatch error position, and do not stop …

…at application type mismatch errors
leanprover · Apr 25, 2022 · 40c8db7 · 40c8db7
1 parent 0c8a6d8
commit 40c8db7
Show file tree

Hide file tree

Showing 20 changed files with 71 additions and 26 deletions.
diff --git 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
@@ -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
@@ -1,12 +1,12 @@
-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
 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
@@ -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
@@ -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
@@ -4,15 +4,15 @@ 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
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,11 +1,12 @@
-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
 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
@@ -1,8 +1,9 @@
-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
 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
@@ -1,20 +1,20 @@
-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
 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)
 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
@@ -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
@@ -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
   Γ