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

test/basic006/expected+2−2

compare with master

unifiedsplit

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

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

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

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

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

3 Type mismatch between

4 Vect n a (Type of xs)

5 and

test/basic009/expected+1−1

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

1MAIN-PASS

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

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

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

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

test/error003/expected+1−2

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

1−ErrorReflection.idr:68:5:

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

2−When elaborating right hand side of bad:

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

2DSL 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:

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

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

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

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

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

5−FunErrTest.idr:38:10:

6−When elaborating right hand side of badCadr2:

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

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

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

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

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

9 elements.

7 elements.

test/error005/expected+10−10

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

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

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

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

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

3 When using 2 as a literal for a Fin 2

4 2 is not strictly less than 2

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

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

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

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

7 When using 0 as a literal for a Fin n

8 0 is not strictly less than n

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

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

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

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

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

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

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

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

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

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

15 When using n as a literal for a Fin 3

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

17 variable instead of a constant Integer

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

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

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

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

20 When using 5 as a literal for a Fin 4

21 5 is not strictly less than 4

test/meta002/expected+1−1

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

1Tacs.idr:247:15:

2−When elaborating right hand side of testElab3:

2+When checking right hand side of testElab3:

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

test/proof002/expected+2−2

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

1Reflect.idr:208:38:

2−When elaborating right hand side of testReflect1:

2+When checking right hand side of testReflect1:

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

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

4 Type mismatch between

5 IsJust (Just x1) (Type of ItIsJust)

6 and

test/proof007/expected+2−2

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

1DefaultArgUnknownName.idr:9:6:

2−When elaborating right hand side of test:

2+When checking right hand side of test:

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

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

4 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:

2No such variable k

test/quasiquote004/expected+1−1

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

1Quasiquote004.idr:50:25:

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

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

3Not a Nat goal

test/quasiquote006/expected+3−3

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

1quasiquote006.idr:9:3:

2−When elaborating right hand side of b:

2+When checking right hand side of b:

3Can't disambiguate name: ForeignEnv.Nil,

4 Prelude.List.Nil

5quasiquote006.idr:12:3:

6−When elaborating right hand side of c:

6+When checking right hand side of c:

7No such variable alsdkjflkj

8quasiquote006.idr:15:3:

9−When elaborating right hand side of d:

9+When checking right hand side of d:

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

11 Prelude.List.::,

12 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:

2No 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:

4No 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:

6No such variable EvenList

test/reg007/expected+1−1

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

1reg007.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:

3Type mismatch between

4 n = lala (Type of isSame)

5and

test/reg010/expected+1−1

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

1reg010.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:

3Can'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:

2Type mismatch between

3 Nat (Type of 0)

4and

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:

2Can'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:

4Can'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:

2Type mismatch between

3 b = b (Type of Refl)

4and

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:

2Void 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:

4No such variable Bogus

test/reg054/expected+6−6

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

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

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

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

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

3 Attempting concrete match on polymorphic argument: 0

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

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

5−When elaborating argument x to Main.weird:

5+When checking argument x to Main.weird:

6 No explicit types on left hand side: Char

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

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

8−When elaborating an application of Main.tctrick:

8+When checking an application of Main.tctrick:

9 Type mismatch between

10 Maybe a1 (Type of Just x)

11 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:

2Can'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:

4Can't match on h x x

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

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

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

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

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

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

test/tutorial006/expected+3−4

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

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

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

2−When elaborating right hand side of vapp:

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

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

4 Type mismatch between

3 Type mismatch between

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

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

6 and

5 and

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

12 and

11 and

13 plus n m

12 plus n m

14tutorial006b.idr:10:10:

13tutorial006b.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:

16Type mismatch between

15Type mismatch between

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

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

18and

17and