Skip to content

Commit 7baf698

Browse files
redfish64gallais
redfish64
and
gallais
authored
Made unifying error msg nicer. (#1922)
Co-authored-by: Guillaume ALLAIS <[email protected]>
1 parent 4b44859 commit 7baf698

File tree

15 files changed

+75
-20
lines changed

15 files changed

+75
-20
lines changed

‎src/Idris/Error.idr

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -231,8 +231,9 @@ perror (CyclicMeta fc env n tm)
231231
perror (WhenUnifying _ gam env x y err)
232232
= do defs <- get Ctxt
233233
setCtxt gam
234-
let res = errorDesc (reflow "When unifying" <++> code !(pshow env x) <++> "and"
235-
<++> code !(pshow env y)) <+> dot <+> line <+> !(perror err)
234+
let res = errorDesc (reflow "When unifying:" <+> line
235+
<+> " " <+> code !(pshow env x) <+> line <+> "and:" <+> line
236+
<+> " " <+> code !(pshow env y)) <+> line <+> !(perror err)
236237
put Ctxt defs
237238
pure res
238239
perror (ValidCase fc env (Left tm))

‎tests/idris2/basic001/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
1/1: Building Vect (Vect.idr)
22
Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
3-
Main> Error: When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat.
3+
Main> Error: When unifying:
4+
Vect (S (S Z)) Nat
5+
and:
6+
Vect (S Z) Nat
47
Mismatch between: S Z and Z.
58

69
(Interactive):1:28--1:51

‎tests/idris2/basic016/expected

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
1/1: Building Eta (Eta.idr)
2-
Error: While processing right hand side of etaBad. When unifying \x, y => MkTest x y = \x, y => MkTest x y and MkTest = \x, y => MkTest x y.
2+
Error: While processing right hand side of etaBad. When unifying:
3+
\x, y => MkTest x y = \x, y => MkTest x y
4+
and:
5+
MkTest = \x, y => MkTest x y
36
Mismatch between: Nat and Integer.
47

58
Eta:14:10--14:14
@@ -11,15 +14,21 @@ Eta:14:10--14:14
1114
^^^^
1215

1316
1/1: Building Eta2 (Eta2.idr)
14-
Error: While processing right hand side of test. When unifying \x => S x = \x => S x and S = \x => S x.
17+
Error: While processing right hand side of test. When unifying:
18+
\x => S x = \x => S x
19+
and:
20+
S = \x => S x
1521
Mismatch between: a and Nat.
1622

1723
Eta2:2:8--2:12
1824
1 | test : Builtin.Equal S (\x : a => S ?)
1925
2 | test = Refl
2026
^^^^
2127

22-
Error: While processing right hand side of test2. When unifying \x => S x = \x => S x and S = \x => S x.
28+
Error: While processing right hand side of test2. When unifying:
29+
\x => S x = \x => S x
30+
and:
31+
S = \x => S x
2332
Mismatch between: a and Nat.
2433

2534
Eta2:5:44--5:48

‎tests/idris2/basic030/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
1/1: Building arity (arity.idr)
2-
Error: While processing right hand side of foo. When unifying Nat -> MyN and MyN.
2+
Error: While processing right hand side of foo. When unifying:
3+
Nat -> MyN
4+
and:
5+
MyN
36
Mismatch between: Nat -> MyN and MyN.
47

58
arity:4:16--4:21

‎tests/idris2/basic034/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
1/1: Building lets (lets.idr)
2-
Error: While processing right hand side of dolet2. When unifying Maybe Int and Maybe String.
2+
Error: While processing right hand side of dolet2. When unifying:
3+
Maybe Int
4+
and:
5+
Maybe String
36
Mismatch between: Int and String.
47

58
lets:22:39--22:40

‎tests/idris2/error001/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
1/1: Building Error (Error.idr)
2-
Error: While processing right hand side of wrong. When unifying a and Vect ?k ?a.
2+
Error: While processing right hand side of wrong. When unifying:
3+
a
4+
and:
5+
Vect ?k ?a
36
Mismatch between: a and Vect ?k ?a.
47

58
Error:6:19--6:20

‎tests/idris2/error003/expected

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
1/1: Building Error (Error.idr)
22
Error: While processing right hand side of wrong. Sorry, I can't find any elaboration which works. All errors:
3-
If Main.length: When unifying Nat and Vect ?n ?a.
3+
If Main.length: When unifying:
4+
Nat
5+
and:
6+
Vect ?n ?a
47
Mismatch between: Nat and Vect ?n ?a.
58

69
Error:12:18--12:19
@@ -11,7 +14,10 @@ Error:12:18--12:19
1114
12 | wrong x = length x
1215
^
1316

14-
If Prelude.List.length: When unifying Nat and List ?a.
17+
If Prelude.List.length: When unifying:
18+
Nat
19+
and:
20+
List ?a
1521
Mismatch between: Nat and List ?a.
1622

1723
Error:12:18--12:19
@@ -22,7 +28,10 @@ Error:12:18--12:19
2228
12 | wrong x = length x
2329
^
2430

25-
If Prelude.String.length: When unifying Nat and String.
31+
If Prelude.String.length: When unifying:
32+
Nat
33+
and:
34+
String
2635
Mismatch between: Nat and String.
2736

2837
Error:12:18--12:19

‎tests/idris2/interface027/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
1/1: Building params (params.idr)
22
Main> False
33
Main> True
4-
Main> Error: When unifying X 4 ?t and X 5 ?t.
4+
Main> Error: When unifying:
5+
X 4 ?t
6+
and:
7+
X 5 ?t
58
Mismatch between: 0 and 1.
69

710
(Interactive):1:1--1:12

‎tests/idris2/namespace002/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
1/1: Building Issue1313 (Issue1313.idr)
2-
Error: While processing right hand side of g. When unifying Int -> Int -> Int and Int.
2+
Error: While processing right hand side of g. When unifying:
3+
Int -> Int -> Int
4+
and:
5+
Int
36
Mismatch between: Int -> Int -> Int and Int.
47

58
Issue1313:9:17--9:18

‎tests/idris2/perf005/expected

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
1/2: Building NoRegression (NoRegression.idr)
22
2/2: Building Lambda (Lambda.idr)
3-
Error: While processing right hand side of term. When unifying Term ?g (TyFunc ?tyA (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))) and Term Empty (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat))))))).
3+
Error: While processing right hand side of term. When unifying:
4+
Term ?g (TyFunc ?tyA (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat))))))))
5+
and:
6+
Term Empty (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))
47
Mismatch between: TyFunc TyNat TyNat and TyNat.
58

69
Lambda:62:3--88:9

0 commit comments

Comments
 (0)