85a9d50 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Update error messages in tests

commit85a9d5063c7aadc8415442ef051b2475884aa2db authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 31 May 2015, 21:22 (11 years ago) parent3ec1122

21 files changed+53−57

compare with master

unifiedsplit

test/basic006/expected+2−2

@@ -1,5 +1,5 @@

1−test020a.idr:16:18:When elaborating right hand side of foo:

2−When elaborating an application of function Prelude.List.reverse:

1+test020a.idr:16:18:When checking right hand side of foo:

2+When checking an application of function Prelude.List.reverse:

33 Type mismatch between

44 Vect n a (Type of xs)

55 and

test/basic009/expected+1−1

@@ -1,4 +1,4 @@

11MAIN-PASS

2−Faulty.idr:6:7:When elaborating type of Faulty.fault:

2+Faulty.idr:6:7:When checking type of Faulty.fault:

33Can't disambiguate name: A.num, B.C.num

44Multiple.idr:3:1:import alias not unique: "X"

test/error003/expected+1−2

@@ -1,3 +1,2 @@

1−ErrorReflection.idr:68:5:

2−When elaborating right hand side of bad:

1+ErrorReflection.idr:68:5:When checking right hand side of bad:

32DSL type error: (t(503) => t'(504)) doesn't match ()

test/error004/expected+4−6

@@ -1,9 +1,7 @@

1−FunErrTest.idr:35:10:

2−When elaborating right hand side of badCadr1:

3−When elaborating argument cons1 to function FunErrTest.cadr:

1+FunErrTest.idr:35:10:When checking right hand side of badCadr1:

2+When checking argument cons1 to function FunErrTest.cadr:

43 Could not prove that [] has at least two elements.

5−FunErrTest.idr:38:10:

6−When elaborating right hand side of badCadr2:

7−When elaborating argument cons2 to function FunErrTest.cadr:

4+FunErrTest.idr:38:10:When checking right hand side of badCadr2:

5+When checking argument cons2 to function FunErrTest.cadr:

86 Could not prove that tail [(fromInteger 1)] has at least two

97 elements.

test/error005/expected+10−10

@@ -1,21 +1,21 @@

1−error005.idr:13:1:When elaborating right hand side of two:

2−When elaborating argument prf to function Data.Fin.fromInteger:

1+error005.idr:13:1:When checking right hand side of two:

2+When checking argument prf to function Data.Fin.fromInteger:

33 When using 2 as a literal for a Fin 2

44 2 is not strictly less than 2

5−error005.idr:16:1:When elaborating right hand side of hahaha:

6−When elaborating argument prf to function Data.Fin.fromInteger:

5+error005.idr:16:1:When checking right hand side of hahaha:

6+When checking argument prf to function Data.Fin.fromInteger:

77 When using 0 as a literal for a Fin n

88 0 is not strictly less than n

9−error005.idr:22:1:When elaborating right hand side of notOk:

10−When elaborating argument prf to function Data.Fin.fromInteger:

9+error005.idr:22:1:When checking right hand side of notOk:

10+When checking argument prf to function Data.Fin.fromInteger:

1111 When using 2 as a literal for a Fin (S (S n))

1212 2 is not strictly less than S (S n)

13−error005.idr:23:24:When elaborating right hand side of b0rken:

14−When elaborating argument prf to function Data.Fin.fromInteger:

13+error005.idr:23:24:When checking right hand side of b0rken:

14+When checking argument prf to function Data.Fin.fromInteger:

1515 When using n as a literal for a Fin 3

1616 Could not show that n is less than 3 because n is a bound

1717 variable instead of a constant Integer

18−error005.idr:28:1:When elaborating right hand side of x:

19−When elaborating argument prf to function Data.Fin.fromInteger:

18+error005.idr:28:1:When checking right hand side of x:

19+When checking argument prf to function Data.Fin.fromInteger:

2020 When using 5 as a literal for a Fin 4

2121 5 is not strictly less than 4

test/meta002/expected+1−1

@@ -1,3 +1,3 @@

11Tacs.idr:247:15:

2−When elaborating right hand side of testElab3:

2+When checking right hand side of testElab3:

33Unifying ty and ARR ty t would lead to infinite value

test/proof002/expected+2−2

@@ -1,6 +1,6 @@

11Reflect.idr:208:38:

2−When elaborating right hand side of testReflect1:

3−When elaborating an application of function Reflect.getJust:

2+When checking right hand side of testReflect1:

3+When checking an application of function Reflect.getJust:

44 Type mismatch between

55 IsJust (Just x1) (Type of ItIsJust)

66 and

test/proof007/expected+2−2

@@ -1,4 +1,4 @@

11DefaultArgUnknownName.idr:9:6:

2−When elaborating right hand side of test:

3−When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:

2+When checking right hand side of test:

3+When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:

44 No such variable sadgjhsag

test/quasiquote003/expected+1−1

@@ -1,2 +1,2 @@

1−NoInfer.idr:11:5:When elaborating right hand side of zzz:

1+NoInfer.idr:11:5:When checking right hand side of zzz:

22No such variable k

test/quasiquote004/expected+1−1

@@ -1,3 +1,3 @@

11Quasiquote004.idr:50:25:

2−When elaborating right hand side of Quasiquote004.getMeNat':

2+When checking right hand side of Quasiquote004.getMeNat':

33Not a Nat goal

test/quasiquote006/expected+3−3

@@ -1,12 +1,12 @@

11quasiquote006.idr:9:3:

2−When elaborating right hand side of b:

2+When checking right hand side of b:

33Can't disambiguate name: ForeignEnv.Nil,

44 Prelude.List.Nil

55quasiquote006.idr:12:3:

6−When elaborating right hand side of c:

6+When checking right hand side of c:

77No such variable alsdkjflkj

88quasiquote006.idr:15:3:

9−When elaborating right hand side of d:

9+When checking right hand side of d:

1010Can't disambiguate name: ForeignEnv.::,

1111 Prelude.List.::,

1212 Prelude.Stream.::

test/reg003/expected+3−3

@@ -1,6 +1,6 @@

1−reg003a.idr:4:11:When elaborating type of Main.ECons:

1+reg003a.idr:4:11:When checking type of Main.ECons:

22No such variable OddList

3−reg003a.idr:7:11:When elaborating type of Main.OCons:

3+reg003a.idr:7:11:When checking type of Main.OCons:

44No such variable EvenList

5−reg003a.idr:9:6:When elaborating type of Main.test:

5+reg003a.idr:9:6:When checking type of Main.test:

66No such variable EvenList

test/reg007/expected+1−1

@@ -1,5 +1,5 @@

11reg007.lidr:8:1:A.n is already defined

2−reg007.lidr:12:11-17:When elaborating right hand side of hurrah:

2+reg007.lidr:12:11-17:When checking right hand side of hurrah:

33Type mismatch between

44 n = lala (Type of isSame)

55and

test/reg010/expected+1−1

@@ -1,3 +1,3 @@

11reg010.idr:5:15:

2−When elaborating left hand side of with block in usubst.unsafeSubst:

2+When checking left hand side of with block in usubst.unsafeSubst:

33Can't match on with block in usubst.unsafeSubst warg a P x x px

test/reg023/expected+1−1

@@ -1,4 +1,4 @@

1−reg023.idr:7:5:When elaborating right hand side of bad:

1+reg023.idr:7:5:When checking right hand side of bad:

22Type mismatch between

33 Nat (Type of 0)

44and

test/reg034/expected+2−2

@@ -1,4 +1,4 @@

1−reg034.idr:6:5:When elaborating left hand side of bar:

1+reg034.idr:6:5:When checking left hand side of bar:

22Can't match on bar xs xs Refl

3−reg034.idr:9:5:When elaborating left hand side of foo:

3+reg034.idr:9:5:When checking left hand side of foo:

44Can't match on foo f x x Refl

test/reg044/expected+1−1

@@ -1,4 +1,4 @@

1−reg044.idr:4:4:When elaborating right hand side of Main.pf:

1+reg044.idr:4:4:When checking right hand side of Main.pf:

22Type mismatch between

33 b = b (Type of Refl)

44and

test/reg049/expected+2−2

@@ -1,4 +1,4 @@

1−reg049.idr:2:9:When elaborating constructor Main.Bogus:

1+reg049.idr:2:9:When checking constructor Main.Bogus:

22Void is not Main.Foo

3−reg049.idr:5:6:When elaborating right hand side of uhOh:

3+reg049.idr:5:6:When checking right hand side of uhOh:

44No such variable Bogus

test/reg054/expected+6−6

@@ -1,11 +1,11 @@

1−reg054.idr:18:5:When elaborating left hand side of inf:

2−When elaborating an application of constructor Main.MkInfer:

1+reg054.idr:18:5:When checking left hand side of inf:

2+When checking an application of constructor Main.MkInfer:

33 Attempting concrete match on polymorphic argument: 0

4−reg054.idr:34:7:When elaborating left hand side of weird:

5−When elaborating argument x to Main.weird:

4+reg054.idr:34:7:When checking left hand side of weird:

5+When checking argument x to Main.weird:

66 No explicit types on left hand side: Char

7−reg054.idr:37:1-8:When elaborating left hand side of tctrick:

8−When elaborating an application of Main.tctrick:

7+reg054.idr:37:1-8:When checking left hand side of tctrick:

8+When checking an application of Main.tctrick:

99 Type mismatch between

1010 Maybe a1 (Type of Just x)

1111 and

test/reg055/expected+5−5

@@ -1,9 +1,9 @@

1−reg055.idr:5:3:When elaborating left hand side of g:

1+reg055.idr:5:3:When checking left hand side of g:

22Can't match on g (f 0)

3−reg055.idr:8:3:When elaborating left hand side of h:

3+reg055.idr:8:3:When checking left hand side of h:

44Can't match on h x x

5−reg055a.idr:8:5:When elaborating left hand side of foo:

6−When elaborating an application of constructor Foo.CAny:

5+reg055a.idr:8:5:When checking left hand side of foo:

6+When checking an application of constructor Foo.CAny:

77 Attempting concrete match on polymorphic argument: Nothing

8−reg055a.idr:13:7:When elaborating left hand side of Foo.apply:

8+reg055a.idr:13:7:When checking left hand side of Foo.apply:

99Can't match on apply (\x => \y => x) a

test/tutorial006/expected+3−4

@@ -1,6 +1,5 @@

1−tutorial006a.idr:5:23-25:

2−When elaborating right hand side of vapp:

3−When elaborating argument xs to constructor Data.VectType.Vect.:::

1+tutorial006a.idr:5:23-25:When checking right hand side of vapp:

2+When checking argument xs to constructor Data.VectType.Vect.:::

43 Type mismatch between

54 Vect (n + n) a (Type of vapp xs xs)

65 and

@@ -12,7 +11,7 @@ When elaborating argument xs to constructor Data.VectType.Vect.:::

1211 and

1312 plus n m

1413tutorial006b.idr:10:10:

15−When elaborating right hand side of with block in Main.parity:

14+When checking right hand side of with block in Main.parity:

1615Type mismatch between

1716 Parity (plus (S j) (S j)) (Type of even)

1817and