max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve argument type mismatch error position, and do not stop at application type mismatch errors

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-25 16:28:46 -07:00
parent 0c8a6d8977
commit 40c8db7494
20 changed files with 71 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Elab/App.lean
View file

@ -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` -/

2
src/Lean/Elab/Term.lean
View file

@ -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

4
tests/lean/243.lean.expected.out
View file

@ -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

2
tests/lean/283.lean.expected.out
View file

@ -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

2
tests/lean/389.lean.expected.out
View file

@ -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

4
tests/lean/423.lean.expected.out
View file

@ -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

2
tests/lean/439.lean.expected.out
View file

@ -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

2
tests/lean/autoPPExplicit.lean.expected.out
View file

@ -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

2
tests/lean/doIssue.lean.expected.out
View file

@ -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

8
tests/lean/elseifDoErrorPos.lean.expected.out
View file

@ -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

2
tests/lean/evalSorry.lean.expected.out
View file

@ -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

2
tests/lean/modBug.lean.expected.out
View file

@ -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

2
tests/lean/mulcommErrorMessage.lean.expected.out
View file

@ -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

7
tests/lean/nameArgErrorIssue.lean Normal file
View file

@ -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)`

20
tests/lean/nameArgErrorIssue.lean.expected.out Normal file
View file

@ -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'

3
tests/lean/namedHoles.lean.expected.out
View file

@ -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

3
tests/lean/phashmap_inst_coherence.lean.expected.out
View file

@ -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

10
tests/lean/scopedunifhint.lean.expected.out
View file

@ -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)

2
tests/lean/simpArgTypeMismatch.lean.expected.out
View file

@ -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

2
tests/lean/sorryAtError.lean.expected.out
View file

@ -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
Γ