idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-20 09:48:38 +03:00
Code Issues Projects Releases Wiki Activity

Show more codes in error report

Browse Source
This commit is contained in:
Andy Lok 2021-02-12 01:24:26 +08:00 committed by G. Allais
parent 4baacc322b
commit bb1edab3aa
61 changed files with 437 additions and 218 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Idris/Error.idr
View File

@ -66,10 +66,9 @@ ploc fc@(MkFC fn s e) = do
source <- lines <$> getCurrentElabSource
if sr == er
then do
let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
let line = (annotate FileCtxt pipe) <++> maybe emptyDoc pretty (elemAt source sr)
let emph = (annotate FileCtxt pipe) <++> spaces (cast sc) <+> annotate Error (pretty (Extra.replicate (ec `minus` sc) '^'))
pure $ vsep [emptyDoc, head, firstRow, annotate FileCtxt (space <+> pretty (sr + 1)) <++> align (vsep [line, emph]), emptyDoc]
let emph = spaces (cast $ nsize + sc + 4) <+> annotate Error (pretty (Extra.replicate (ec `minus` sc) '^'))
let firstr = er `minus` 4
pure $ vsep ([emptyDoc, head] ++ (addLineNumbers nsize firstr (pretty <$> extractRange firstr er source)) ++ [emph]) <+> line
else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line
where
extractRange : Nat -> Nat -> List String -> List String

14
tests/chez/chez006/expected
View File

@ -17,14 +17,20 @@ Main> Bye for now!
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).
TypeCase2.idr:5:14--5:17
|
1 | data Bar = MkBar
2 | data Baz = MkBaz
3 |
4 | strangeId : a -> a
5 | strangeId {a=Nat} x = x+1
| ^^^
^^^
Error: While processing left hand side of foo. Can't match on Nat (Erased argument).
TypeCase2.idr:9:5--9:8
|
5 | strangeId {a=Nat} x = x+1
6 | strangeId x = x
7 |
8 | foo : (0 x : Type) -> String
9 | foo Nat = "Nat"
| ^^^
^^^

3
tests/idris2/basic001/expected
View File

@ -4,8 +4,7 @@ Main> Error: When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat.
Mismatch between: S Z and Z.
(interactive):1:28--1:51
|
1 | zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
| ^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^
Main> Bye for now!

7
tests/idris2/basic003/expected
View File

@ -6,8 +6,11 @@ Error: While processing right hand side of keepUnique. Ambiguous elaboration. Po
Main.Vect.toList ?arg
Ambig2.idr:26:21--26:27
|
22 | export
23 | fromList : List a -> Set a
24 |
25 | keepUnique : List b -> List b
26 | keepUnique {b} xs = toList (fromList xs)
| ^^^^^^
^^^^^^
Main> Bye for now!

3
tests/idris2/basic005/expected
View File

@ -2,8 +2,7 @@
Error: Unsolved holes:
Main.{_:1} introduced at:
NoInfer.idr:1:7--1:8
|
1 | foo : ? -> Int
| ^
^
Main> Bye for now!

4
tests/idris2/basic011/expected
View File

@ -3,9 +3,9 @@
Error: While processing left hand side of foo. Can't match on ?x [no locals in scope] (Non linear pattern variable).
Dots2.idr:2:7--2:8
|
1 | foo : Int -> Int -> Int
2 | foo x x = x + x
| ^
^
1/1: Building Dots3 (Dots3.idr)
Error: While processing left hand side of addBaz. Pattern variable z unifies with: ?y [no locals in scope].

14
tests/idris2/basic014/expected
View File

@ -2,14 +2,20 @@
Error: While processing right hand side of wrongCommutes. Rewriting by m + k = k + m did not change type S k + m = m + S k.
Rewrite.idr:15:25--15:57
|
11 | plusCommutes (S k) m = rewrite plusCommutes k m in sym (plusnSm m k)
12 |
13 | wrongCommutes : (n, m : Nat) -> n + m = m + n
14 | wrongCommutes Z m = sym (plusnZ m)
15 | wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: While processing right hand side of wrongCommutes2. Nat is not a rewrite rule type.
Rewrite.idr:19:26--19:43
|
15 | wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar
16 |
17 | wrongCommutes2 : (n, m : Nat) -> n + m = m + n
18 | wrongCommutes2 Z m = sym (plusnZ m)
19 | wrongCommutes2 (S k) m = rewrite m in ?bar
| ^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^

18
tests/idris2/basic016/expected
View File

@ -3,24 +3,30 @@ Error: While processing right hand side of etaBad. When unifying \x, y => MkTest
Mismatch between: Nat and Integer.
Eta.idr:14:10--14:14
|
10 | etaGood3: (f : a -> b) -> f = (\x => f x)
11 | etaGood3 f = Refl
12 |
13 | etaBad : MkTest = (\x : Nat => \y => MkTest ? ?)
14 | etaBad = Refl
| ^^^^
^^^^
1/1: Building Eta2 (Eta2.idr)
Error: While processing right hand side of test. When unifying \x => S ?_ = \x => S ?_ and S = \x => S ?_.
Mismatch between: a and Nat.
Eta2.idr:2:8--2:12
|
1 | test : Builtin.Equal S (\x : a => S ?)
2 | test = Refl
| ^^^^
^^^^
Error: While processing right hand side of test2. When unifying \x => S ?_ = \x => S ?_ and S = \x => S ?_.
Mismatch between: a and Nat.
Eta2.idr:5:44--5:48
|
1 | test : Builtin.Equal S (\x : a => S ?)
2 | test = Refl
3 |
4 | test2 : ?
5 | test2 = {a : _} -> the (S = \x : a => S _) Refl
| ^^^^
^^^^

7
tests/idris2/basic018/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of bar. Can't find an implementation for IsJust (integerToFin 8 5).
Fin.idr:34:7--34:8
|
30 | foo : Fin 5
31 | foo = 3
32 |
33 | bar : Fin 5
34 | bar = 8
| ^
^

14
tests/idris2/basic022/expected
View File

@ -2,16 +2,22 @@
Error: While processing left hand side of bad. Can't match on False (Erased argument).
Erase.idr:5:5--5:10
|
1 | myReplace : forall p . (0 rule : x = y) -> (1 val : p y) -> p x
2 | myReplace Refl prf = prf
3 |
4 | bad : (0 x : Bool) -> Bool
5 | bad False = True
| ^^^^^
^^^^^
Error: While processing left hand side of minusBad. Can't match on LeZ (Erased argument).
Erase.idr:19:18--19:21
|
15 | minus (S k) (S j) (LeS p) = minus k j p
16 |
17 | -- y is used in the run time case tree, so erasure not okay
18 | minusBad : (x : Nat) -> (0 y : Nat) -> (0 prf : LT y x) -> Nat
19 | minusBad (S k) Z LeZ = S k
| ^^^
^^^
Main> \m => minus (S (S m)) m prf
Main> Bye for now!

6
tests/idris2/basic030/expected
View File

@ -3,7 +3,9 @@ Error: While processing right hand side of foo. When unifying Nat -> MyN and MyN
Mismatch between: Nat -> MyN and MyN.
arity.idr:4:16--4:21
|
1 | data MyN = MkN Nat Nat
2 |
3 | foo : Nat -> Nat -> Nat
4 | foo x y = case MkN x of
| ^^^^^
^^^^^

7
tests/idris2/basic031/expected
View File

@ -2,7 +2,10 @@
Error: While processing left hand side of nameOf. Can't match on Bool (Erased argument).
erased.idr:7:17--7:21
|
3 | MyJust : a -> MyMaybe a
4 |
5 | -- Should fail since type argument is deleted
6 | nameOf : Type -> String
7 | nameOf (MyMaybe Bool) = "MyMaybe Bool"
| ^^^^
^^^^

14
tests/idris2/basic033/expected
View File

@ -2,14 +2,20 @@
Error: While processing type of len'. Undefined name xs.
unboundimps.idr:18:11--18:13
|
14 | -- xs and its indices
15 | len : forall xs . Env xs -> Nat
16 |
17 | -- neither of these are fine
18 | len': Env xs -> Nat
| ^^
^^
Error: While processing type of append'. Undefined name n.
unboundimps.idr:19:16--19:17
|
15 | len : forall xs . Env xs -> Nat
16 |
17 | -- neither of these are fine
18 | len': Env xs -> Nat
19 | append' : Vect n a -> Vect m a -> Vect (n + m) a
| ^
^

7
tests/idris2/basic034/expected
View File

@ -3,7 +3,10 @@ Error: While processing right hand side of dolet2. When unifying Maybe Int and M
Mismatch between: Int and String.
lets.idr:22:39--22:40
|
18 | pure (x' + y')
19 |
20 | dolet2 : Maybe Int -> Maybe Int -> Maybe Int
21 | dolet2 x y
22 | = do let Just x' : Maybe String = x
| ^
^

7
tests/idris2/basic041/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of test. Undefined name B.A.>>=.
QDo.idr:19:10--19:11
|
15 | (>>=) x fy = x + (fy ())
16 |
17 | test : Nat
18 | test = B.A.do
19 | 5
| ^
^

6
tests/idris2/basic042/expected
View File

@ -6,9 +6,8 @@ Main> False
Main> Error: Can't find an implementation for IsJust Nothing.
(interactive):1:10--1:14
|
1 | the Bool "42"
| ^^^^
^^^^
Main> Bye for now!
1/1: Building LiteralsInteger (LiteralsInteger.idr)
@ -19,8 +18,7 @@ Main> FS (FS FZ)
Main> Error: Can't find an implementation for IsJust (integerToFin 6 3).
(interactive):1:13--1:14
|
1 | the (Fin 3) 6
| ^
^
Main> Bye for now!

7
tests/idris2/basic049/expected
View File

@ -4,9 +4,12 @@ Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous ela
Main.R1.MkR Type
Fld.idr:72:26--72:29
|
68 | r1 : R1 -- explicit fields access
69 | r1 = MkR {field = "string"}
70 |
71 | r2_shouldNotTypecheck1 : ?
72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
| ^^^
^^^
Main> Main.myDog : OrdinaryDog
Main> Main.mySuperDog : SuperDog

7
tests/idris2/coverage003/expected
View File

@ -2,9 +2,12 @@
Error: While processing left hand side of badBar. Can't match on 0 as it has a polymorphic type.
Cover.idr:16:1--16:7
|
12 | cty Nat (S _) = S Z
13 | cty _ x = S (S Z)
14 |
15 | badBar : a -> Nat
16 | badBar Z = Z
| ^^^^^^
^^^^^^
Main> Main.foo: foo (0, S _)
foo (S _, _)

7
tests/idris2/coverage004/expected
View File

@ -2,9 +2,12 @@
Error: While processing left hand side of bad. Can't match on Just (fromInteger 0) as it has a polymorphic type.
Cover.idr:14:1--14:4
|
10 |
11 | bad : a -> Foo a -> Bool
12 | bad Z IsNat = False
13 | bad True IsBool = True
14 | bad (Just 0) _ = False
| ^^^
^^^
Main> Main.okay: okay (S _) IsNat
okay False IsBool

14
tests/idris2/coverage007/expected
View File

@ -2,14 +2,20 @@
Error: badeq x y p is not a valid impossible case.
eq.idr:27:1--27:23
|
23 | eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat
24 | eqL2 xs p impossible
25 |
26 | badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
27 | badeq x y p impossible
| ^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^
Error: badeqL xs ys p is not a valid impossible case.
eq.idr:30:1--30:26
|
26 | badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
27 | badeq x y p impossible
28 |
29 | badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat
30 | badeqL xs ys p impossible
| ^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^

12
tests/idris2/coverage009/expected
View File

@ -2,14 +2,18 @@
Warning: Unreachable clause: foo Nothing True
unreachable.idr:3:1--3:17
|
1 | foo : Maybe Int -> Bool -> Int
2 | foo Nothing _ = 42
3 | foo Nothing True = 94
| ^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^
Warning: Unreachable clause: foo Nothing False
unreachable.idr:5:1--5:18
|
1 | foo : Maybe Int -> Bool -> Int
2 | foo Nothing _ = 42
3 | foo Nothing True = 94
4 | foo (Just x) _ = x
5 | foo Nothing False = 42
| ^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^

7
tests/idris2/coverage010/expected
View File

@ -2,8 +2,11 @@
Error: main is not covering.
casetot.idr:12:1--12:13
|
08 |
09 | ints : Vect 4 Int
10 | ints = [1, 2, 3, 4]
11 |
12 | main : IO ()
| ^^^^^^^^^^^^
^^^^^^^^^^^^
Calls non covering function Main.case block in case block in main

7
tests/idris2/error001/expected
View File

@ -3,7 +3,10 @@ Error: While processing right hand side of wrong. When unifying a and Vect ?k ?a
Mismatch between: a and Vect ?k ?a.
Error.idr:6:19--6:20
|
2 | Nil : Vect Z a
3 | (::) : a -> Vect k a -> Vect (S k) a
4 |
5 | wrong : a -> Vect (S n) a -> Vect (S n) a
6 | wrong x xs = x :: x
| ^
^

7
tests/idris2/error002/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of wrong. Undefined name ys.
Error.idr:6:17--6:19
|
2 | Nil : Vect Z a
3 | (::) : a -> Vect k a -> Vect (S k) a
4 |
5 | wrong : a -> Vect (S n) a -> Vect (S n) a
6 | wrong xs = x :: ys
| ^^
^^

21
tests/idris2/error003/expected
View File

@ -4,23 +4,32 @@ If Main.length: When unifying Nat and Vect ?n ?a.
Mismatch between: Nat and Vect ?n ?a.
Error.idr:12:18--12:19
|
08 | length [] = Z
09 | length (x :: xs) = S (length xs)
10 |
11 | wrong : Nat -> Nat
12 | wrong x = length x
| ^
^
If Prelude.List.length: When unifying Nat and List ?a.
Mismatch between: Nat and List ?a.
Error.idr:12:18--12:19
|
08 | length [] = Z
09 | length (x :: xs) = S (length xs)
10 |
11 | wrong : Nat -> Nat
12 | wrong x = length x
| ^
^
If Prelude.String.length: When unifying Nat and String.
Mismatch between: Nat and String.
Error.idr:12:18--12:19
|
08 | length [] = Z
09 | length (x :: xs) = S (length xs)
10 |
11 | wrong : Nat -> Nat
12 | wrong x = length x
| ^
^

21
tests/idris2/error004/expected
View File

@ -2,18 +2,24 @@
Error: While processing right hand side of wrong. Can't find an implementation for Show (Vect 4 Integer).
Error1.idr:8:9--8:40
|
4 | Nil : Vect Z a
5 | (::) : a -> Vect k a -> Vect (S k) a
6 |
7 | wrong : String
8 | wrong = show (the (Vect _ _) [1,2,3,4])
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1/1: Building Error2 (Error2.idr)
Error: While processing right hand side of show. Multiple solutions found in search of:
Show (Vect k Integer)
Error2.idr:13:38--13:45
|
09 | show (x :: xs) = show x ++ ", " ++ show xs
10 |
11 | Show (Vect n Integer) where
12 | show [] = "END"
13 | show (x :: xs) = show x ++ ", " ++ show xs
| ^^^^^^^
^^^^^^^
Possible correct results:
Show implementation at Error2.idr:11:1--13:45
@ -22,9 +28,12 @@ Error: While processing right hand side of wrong. Multiple solutions found in se
Show (Vect 1 Integer)
Error2.idr:16:9--16:34
|
12 | show [] = "END"
13 | show (x :: xs) = show x ++ ", " ++ show xs
14 |
15 | wrong : String
16 | wrong = show (the (Vect _ _) [1])
| ^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^
Possible correct results:
Show implementation at Error2.idr:11:1--13:45

13
tests/idris2/error005/expected
View File

@ -2,14 +2,19 @@
Error: While processing right hand side of foo. Can't find an implementation for Eq a.
IfErr.idr:4:11--4:17
|
1 | data Wibble = Wobble
2 |
3 | foo : a -> a -> Bool
4 | foo x y = x == y
| ^^^^^^
^^^^^^
Error: While processing right hand side of bar. Can't find an implementation for Eq Wibble.
IfErr.idr:7:11--7:17
|
3 | foo : a -> a -> Bool
4 | foo x y = x == y
5 |
6 | bar : Wibble -> Wibble -> Bool
7 | bar x y = x == y
| ^^^^^^
^^^^^^

14
tests/idris2/error006/expected
View File

@ -2,14 +2,20 @@
Error: While processing right hand side of test. Can't find an implementation for Eq Foo.
IfErr.idr:15:10--15:30
|
11 | -- hard to achieve and this way is better than displaying the whole
12 | -- top level search when only part of it is relevant)
13 |
14 | test : Int -> String
15 | test x = showIfEq MkFoo MkBar
| ^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^
Error: While processing right hand side of test2. Can't find an implementation for Show Foo.
IfErr.idr:23:9--23:29
|
19 | MkBar == MkBar = True
20 | _ == _ = False
21 |
22 | test2 : String
23 | test2 = showIfEq MkFoo MkBar
| ^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^

6
tests/idris2/error007/expected
View File

@ -2,7 +2,9 @@
Error: While processing right hand side of fsprf. Can't solve constraint between: ?_ x and FS x.
CongErr.idr:4:11--4:19
|
1 | import Data.Fin
2 |
3 | fsprf : x === y -> FS x = FS y
4 | fsprf p = cong _ p
| ^^^^^^^^
^^^^^^^^

3
tests/idris2/error009/expected
View File

@ -1,8 +1,7 @@
Error: Module DoesntExist not found
Exists.idr:1:1--1:19
|
1 | import DoesntExist
| ^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^
Main> Bye for now!

4
tests/idris2/error010/expected
View File

@ -2,7 +2,7 @@
Error: While processing right hand side of example. Main.example is already defined.
Loop.idr:2:11--2:19
|
1 | example : String
2 | example = ?example
| ^^^^^^^^
^^^^^^^^

10
tests/idris2/error011/expected
View File

@ -2,14 +2,16 @@
Error: Main.B is already defined.
ConstructorDuplicate.idr:1:14--1:15
|
1 | data A = B | B
| ^
^
Error: Main.D is already defined.
ConstructorDuplicate.idr:5:3--5:15
|
1 | data A = B | B
2 |
3 | data C : Type -> Type where
4 | D : C Int
5 | D : C String
| ^^^^^^^^^^^^
^^^^^^^^^^^^

21
tests/idris2/error013/expected
View File

@ -2,21 +2,30 @@
Error: main is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--5:11 -> Main.== -> Main./= -> Main.==
Issue361.idr:7:1--7:13
|
3 | data S = T | F
4 |
5 | Eq S where
6 |
7 | main : IO ()
| ^^^^^^^^^^^^
^^^^^^^^^^^^
Error: /= is not total, possibly not terminating due to recursive path Main./= -> Main.== -> Main./= -> Main.==
Issue361.idr:5:1--5:11
|
1 | %default total
2 |
3 | data S = T | F
4 |
5 | Eq S where
| ^^^^^^^^^^
^^^^^^^^^^
Error: == is not total, possibly not terminating due to call to Main./=
Issue361.idr:5:1--5:11
|
1 | %default total
2 |
3 | data S = T | F
4 |
5 | Eq S where
| ^^^^^^^^^^
^^^^^^^^^^

14
tests/idris2/error014/expected
View File

@ -2,14 +2,20 @@
Error: Constructor Prelude.Types.:: is not fully applied.
Issue735.idr:5:8--5:12
|
1 | module Issue735
2 |
3 | -- Not allowed to pattern-match on under-applied constructors
4 | isCons : (a -> List a -> List a) -> Bool
5 | isCons (::) = True
| ^^^^
^^^^
Error: Constructor Issue735.A is not fully applied.
Issue735.idr:12:6--12:7
|
08 | interface A a where
09 |
10 | -- Not allowed to pattern-match on under-applied type constructors
11 | test : (kind : Type -> Type) -> Maybe Nat
12 | test A = Just 1
| ^
^

14
tests/idris2/import002/expected
View File

@ -4,15 +4,21 @@
Error: While processing type of thing. Undefined name Nat.
Test.idr:5:9--5:12
|
1 | module Test
2 |
3 | import Mult
4 |
5 | thing : Nat -> Nat
| ^^^
^^^
Error: No type declaration for Test.thing.
Test.idr:6:1--6:28
|
2 |
3 | import Mult
4 |
5 | thing : Nat -> Nat
6 | thing x = mult x (plus x x)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^
Test> Bye for now!

7
tests/idris2/interface008/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of badcard. k is not accessible in this context.
Deps.idr:18:13--18:14
|
14 | badcard : Nat
15 | badto : t -> Fin card
16 |
17 | implementation BadFinite (Fin k) where
18 | badcard = k
| ^
^

7
tests/idris2/interface013/expected
View File

@ -2,7 +2,10 @@
Error: While processing constructor MkRecord. Can't find an implementation for Interface ?s.
TypeInt.idr:14:25--14:49
|
10 | 0 DependentValue : Interface s => Value s -> Type
11 | DependentValue v = concrete (specifier v)
12 |
13 | data Record : s -> Type where
14 | MkRecord : Value s -> DependentValue {s} value -> Record s
| ^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^

21
tests/idris2/interface015/expected
View File

@ -3,9 +3,12 @@ Error: While processing right hand side of TestSurprise1. Multiple solutions fou
Gnu
gnu.idr:47:27--47:32
|
43 |
44 | ||| This is the meat. I'd expect this function to raise an error
45 | ||| because it is ambiguous which local/local function to use.
46 | TestSurprise1 : (gnu1, gnu2 : Gnu) -> String
47 | TestSurprise1 gnu1 gnu2 = Guess
| ^^^^^
^^^^^
Possible correct results:
gnu1
@ -14,9 +17,12 @@ Error: While processing right hand side of TestSurprise2. Multiple solutions fou
Gnu
gnu.idr:50:21--50:26
|
46 | TestSurprise1 : (gnu1, gnu2 : Gnu) -> String
47 | TestSurprise1 gnu1 gnu2 = Guess
48 |
49 | TestSurprise2 : (f,g : Unit -> Gnu) -> String
50 | TestSurprise2 f g = Guess
| ^^^^^
^^^^^
Possible correct results:
f ()
@ -24,7 +30,10 @@ Possible correct results:
Error: While processing right hand side of TestSurprise3. Can't find an implementation for Gnu.
gnu.idr:53:19--53:24
|
49 | TestSurprise2 : (f,g : Unit -> Gnu) -> String
50 | TestSurprise2 f g = Guess
51 |
52 | TestSurprise3 : (Unit -> Gnu, Unit -> Gnu) -> String
53 | TestSurprise3 f = Guess
| ^^^^^
^^^^^

6
tests/idris2/interface016/expected
View File

@ -3,9 +3,11 @@ Error: While processing right hand side of f. While processing right hand side o
Num a
TwoNum.idr:4:7--4:8
|
1 | f : Num a => a
2 | f = g where
3 | g : Num a => a
4 | g = 0
| ^
^
Possible correct results:
conArg (implicitly bound at TwoNum.idr:4:3--4:8)

7
tests/idris2/interface019/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of bug. Can't find an implementation for Gnu.
LocalHints.idr:48:17--48:22
|
44 | bug {a} x = let M : More
45 | M = MkMore a
46 | %hint arg : Gnat (Ty M)
47 | arg = MkGnat (const B)
48 | in (findB ** Refl)
| ^^^^^
^^^^^

3
tests/idris2/interpreter003/expected
View File

@ -1,9 +1,8 @@
Main> Error: Undefined name fromMaybe.
(interactive):1:1--1:10
|
1 | fromMaybe "test" Nothing
| ^^^^^^^^^
^^^^^^^^^
Main> Imported module Data.Maybe
Main> "test"

7
tests/idris2/linear006/expected
View File

@ -2,9 +2,12 @@
Error: While processing right hand side of bar. Main.test is not accessible in this context.
ZFun.idr:13:7--13:11
|
09 | 0 baz : Nat
10 | baz = test foo -- fine!
11 |
12 | bar : Nat
13 | bar = test foo -- bad!
| ^^^^
^^^^
Main> [tc] Main> 10
[tc] Main> Bye for now!

7
tests/idris2/params001/expected
View File

@ -3,8 +3,11 @@
Error: While processing right hand side of U. Name Main.X.foo is private.
parambad.idr:7:7--7:10
|
3 | foo : Bool
4 | foo = True
5 |
6 | U : Bool
7 | U = foo
| ^^^
^^^
Suggestion: add an explicit export or public export modifier. By default, all names are private in namespace blocks.

3
tests/idris2/pkg004/expected
View File

@ -2,9 +2,8 @@
Dummy> Error: Undefined name undefined.
(interactive):1:4--1:13
|
1 | :t undefined
| ^^^^^^^^^
^^^^^^^^^
Dummy> Dummy.something : String
Dummy> "Something something"

3
tests/idris2/record004/expected
View File

@ -10,9 +10,8 @@ Main> Error: When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
(interactive):1:1--1:4
|
1 | map .x [MkPoint 1 2, MkPoint 3 4]
| ^^^
^^^
Main> [2.5, 2.5]
Main> 7.4

21
tests/idris2/reflection001/expected
View File

@ -3,23 +3,32 @@ Error: While processing right hand side of bad. When unifying Int and TTImp.
Mismatch between: Int and TTImp.
quote.idr:25:19--25:22
|
21 | bad : Int -> TTImp
22 | bad val
23 | = `(let xfn : Int -> Int
24 | xfn var = var * 2 in
25 | xfn ~(val))
| ^^^
^^^
Error: %language ElabReflection not enabled
quote.idr:33:1--33:21
|
29 |
30 | noExtension : Elab ()
31 | noExtension = fail "Should not print this message"
32 |
33 | %runElab noExtension
| ^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^
Error: Error during reflection: Should not print this message
quote.idr:37:1--37:21
|
33 | %runElab noExtension
34 |
35 | %language ElabReflection
36 |
37 | %runElab noExtension
| ^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4)))
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False"))

28
tests/idris2/reflection003/expected
View File

@ -8,28 +8,40 @@ LOG 0: Constructors: [Prelude.Types.Z, Prelude.Types.S]
Error: While processing right hand side of dummy1. Error during reflection: Not really trying
refprims.idr:43:10--43:27
|
39 | ns <- inCurrentNS n
40 | fail $ "failed after generating " ++ censorDigits (show ns)
41 |
42 | dummy1 : a
43 | dummy1 = %runElab logPrims
| ^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^
Error: While processing right hand side of dummy2. Error during reflection: Still not trying
refprims.idr:46:10--46:30
|
42 | dummy1 : a
43 | dummy1 = %runElab logPrims
44 |
45 | dummy2 : a
46 | dummy2 = %runElab logDataCons
| ^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^
Error: While processing right hand side of dummy3. Error during reflection: Undefined name
refprims.idr:49:10--49:25
|
45 | dummy2 : a
46 | dummy2 = %runElab logDataCons
47 |
48 | dummy3 : a
49 | dummy3 = %runElab logBad
| ^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^
Error: While processing right hand side of dummy4. Error during reflection: failed after generating Main.{plus:XXXX}
refprims.idr:52:10--52:28
|
48 | dummy3 : a
49 | dummy3 = %runElab logBad
50 |
51 | dummy4 : a
52 | dummy4 = %runElab tryGenSym
| ^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^

7
tests/idris2/reflection005/expected
View File

@ -3,9 +3,12 @@ Error: While processing right hand side of bad. When unifying Elab () and Elab a
Mismatch between: () and a.
refdecl.idr:13:16--13:29
|
09 |
10 | %runElab mkDecls `(94)
11 |
12 | bad : a
13 | bad = %runElab mkDecls `(94)
| ^^^^^^^^^^^^^
^^^^^^^^^^^^^
Main> 9400
Main> Bye for now!

7
tests/idris2/reflection006/expected
View File

@ -5,7 +5,10 @@ LOG 0: Right: ((Prelude.Types.plus y) x)
Error: While processing right hand side of commutes. Error during reflection: Not done
refleq.idr:24:16--24:21
|
20 | logMsg "" 0 (show env)
21 | solveReflected g
22 |
23 | commutes : (x, y : Nat) -> plus x y = plus y x
24 | commutes x y = prove
| ^^^^^
^^^^^

43
tests/idris2/reg003/expected
View File

@ -2,58 +2,69 @@
Error: While processing type of Vect_ext. Undefined name ~=~.
Holes.idr:4:64--4:85
|
1 | import Data.Vect
2 | import Data.Fin
3 |
4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
| ^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^
Error: While processing type of Weird. Undefined name ~=~.
Holes.idr:7:26--7:31
|
3 |
4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
5 | -> v = w
6 |
7 | Weird : (v: Vect n a) -> v = v
| ^^^^^
^^^^^
Error: No type declaration for Main.Weird.
Holes.idr:8:1--8:41
|
4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
5 | -> v = w
6 |
7 | Weird : (v: Vect n a) -> v = v
8 | Weird v = Vect_ext ?hole0 ?hole1 ?hole2
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: While processing type of f. Undefined name Bool.
Holes.idr:10:5--10:9
|
06 |
07 | Weird : (v: Vect n a) -> v = v
08 | Weird v = Vect_ext ?hole0 ?hole1 ?hole2
09 |
10 | f : Bool -> Nat
| ^^^^
^^^^
Error: No type declaration for Main.f.
Holes.idr:11:1--11:11
|
07 | Weird : (v: Vect n a) -> v = v
08 | Weird v = Vect_ext ?hole0 ?hole1 ?hole2
09 |
10 | f : Bool -> Nat
11 | f True = 0
| ^^^^^^^^^^
^^^^^^^^^^
Main> Error: Undefined name help.
(interactive):1:4--1:8
|
1 | :t help
| ^^^^
^^^^
Main> Error: Undefined name hole0.
(interactive):1:4--1:9
|
1 | :t hole0
| ^^^^^
^^^^^
Main> Error: Undefined name hole1.
(interactive):1:4--1:9
|
1 | :t hole1
| ^^^^^
^^^^^
Main> Unknown name hole1
Main> Bye for now!

7
tests/idris2/reg005/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of isInListBad. Can't solve constraint between: if c then "Foo" else "Baz" and if c then "Foo" else "Bar".
iftype.idr:15:15--15:19
|
11 | isInList = Here
12 |
13 | isInListBad : Elem (ABC Bool String (\c => if c then "Foo" else "Bar"))
14 | [(ABC Bool String (\c => if c then "Foo" else "Baz"))]
15 | isInListBad = Here
| ^^^^
^^^^

7
tests/idris2/reg007/expected
View File

@ -3,7 +3,10 @@ Error: While processing right hand side of dpairWithExtraInfoBad. When unifying
Mismatch between: [MN 0] and [].
Main.idr:27:26--27:73
|
23 | dpairWithExtraInfoWorks : List (vars : List Name ** Expr vars)
24 | dpairWithExtraInfoWorks = [([MN 0] ** CLocal {x=MN 0} (First {ns=[]}))]
25 |
26 | dpairWithExtraInfoBad : List (vars : List Name ** Expr vars)
27 | dpairWithExtraInfoBad = [([MN 0] ** CLocal {x=MN 0} (First {ns=[MN 0]}))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

28
tests/idris2/reg013/expected
View File

@ -2,28 +2,40 @@
Error: While processing constructor Foo. Undefined name n.
UnboundImplicits.idr:6:22--6:23
|
2 | import Data.Vect
3 |
4 | %unbound_implicits off
5 |
6 | record Foo (x : Vect n Nat) where
| ^
^
Error: Undefined name n.
UnboundImplicits.idr:9:24--9:25
|
5 |
6 | record Foo (x : Vect n Nat) where
7 | constructor MkFoo
8 |
9 | parameters (Foo : Vect n Nat)
| ^
^
Error: While processing constructor Foo. Undefined name n.
UnboundImplicits.idr:14:25--14:26
|
10 | bar : Nat
11 | bar = 0
12 |
13 |
14 | interface Foo (a : Vect n Nat) where
| ^
^
Error: While processing type of Functor implementation at UnboundImplicits.idr:17:1--17:38. Undefined name n.
UnboundImplicits.idr:17:30--17:31
|
13 |
14 | interface Foo (a : Vect n Nat) where
15 | baz : Nat
16 |
17 | implementation Functor (Vect n) where
| ^
^

7
tests/idris2/reg015/expected
View File

@ -2,7 +2,10 @@
Error: showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is not a valid impossible case.
anyfail.idr:21:1--21:48
|
17 | TooComplicatedToBeTrue
18 | (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len))))
19 |
20 | showing : (something : EvenMoreComplicated) -> (TooComplicatedToBeTrue something) -> Void
21 | showing _ SomethingVeryComplicatedIs impossible
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

4
tests/idris2/reg017/expected
View File

@ -3,7 +3,7 @@ Error: While processing right hand side of badmap. When unifying (0 _ : ?a) -> ?
Mismatch between: (0 _ : ?a) -> ?b and ?a -> ?b.
lammult.idr:2:18--2:19
|
1 | badmap : List Int -> List Int
2 | badmap = map (\0 x => 2)
| ^
^

21
tests/idris2/reg019/expected
View File

@ -2,21 +2,30 @@
Error: While processing right hand side of main. Can't solve constraint between: Bool and Lazy Bool.
lazybug.idr:5:22--5:34
|
1 | bools : List Bool
2 | bools = [True, False]
3 |
4 | main : IO ()
5 | main = printLn $ or (map id bools)
| ^^^^^^^^^^^^
^^^^^^^^^^^^
Error: While processing right hand side of main2. Can't solve constraint between: Bool and Lazy Bool.
lazybug.idr:8:23--8:42
|
4 | main : IO ()
5 | main = printLn $ or (map id bools)
6 |
7 | main2 : IO ()
8 | main2 = printLn $ or (map (\x => x) bools)
| ^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^
Error: While processing right hand side of main4. Can't solve constraint between: Bool and Lazy Bool.
lazybug.idr:14:22--14:27
|
10 | main3 : IO ()
11 | main3 = printLn $ or (map (\x => Delay x) bools)
12 |
13 | main4 : IO ()
14 | main4 = printLn $ or bools
| ^^^^^
^^^^^

7
tests/idris2/reg023/expected
View File

@ -2,7 +2,10 @@
Error: While processing right hand side of with block in eraseVar. Can't solve constraint between: S (countGreater thr xs) and countGreater thr xs.
boom.idr:23:42--23:66
|
19 | eraseVar : (thr : Int) -> (ctx : Vect n Int) -> Fin n -> Maybe (Fin (countGreater thr ctx))
20 | eraseVar thr (x :: xs) j with (x .<=. thr)
21 | eraseVar thr (x :: xs) FZ | True = Nothing
22 | eraseVar thr (x :: xs) FZ | False = Just FZ
23 | eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i
| ^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^

7
tests/idris2/reg034/expected
View File

@ -2,7 +2,10 @@
Error: While processing left hand side of Calc. Can't match on ?y [no locals in scope] (Non linear pattern variable).
void.idr:18:19--18:20
|
14 |
15 | public export
16 | Calc : {x : a} -> {y : b} -> FastDerivation x y -> x = y
17 | Calc (|~ x) = Refl
18 | Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der
| ^
^

24
tests/idris2/with003/expected
View File

@ -5,59 +5,52 @@ If Prelude.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:66--1:81
|
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
| ^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:38--1:64
|
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:38--1:64
|
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^
If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
If Prelude.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:66--1:81
|
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
| ^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^
If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b.
Mismatch between: ?_ -> IO () and IO ?b.
(interactive):1:38--1:64
|
1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^
Main> Error: Can't find an implementation for Num ().
(interactive):1:61--1:65
|
1 | with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"
| ^^^^
^^^^
Main> Error: Ambiguous elaboration. Possible results:
Prelude.Nil
Data.Vect.Nil
(interactive):1:4--1:6
|
1 | :t []
| ^^
^^
Main> [] : Vect 0 ?elem
Main> [] : List ?a
@ -65,9 +58,8 @@ Main> Error: When unifying Vect 0 ?elem and List ?a.
Mismatch between: Vect 0 ?elem and List ?a.
(interactive):1:34--1:41
|
1 | :t with [Vect.Nil, Prelude.(::)] [1,2,3]
| ^^^^^^^
^^^^^^^
Main> the (Maybe Integer) (pure 4) : Maybe Integer
Main> Parse error at line 1:2:

14
tests/node/node006/expected
View File

@ -17,14 +17,20 @@ Main> Bye for now!
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).
TypeCase2.idr:5:14--5:17
|
1 | data Bar = MkBar
2 | data Baz = MkBaz
3 |
4 | strangeId : a -> a
5 | strangeId {a=Nat} x = x+1
| ^^^
^^^
Error: While processing left hand side of foo. Can't match on Nat (Erased argument).
TypeCase2.idr:9:5--9:8
|
5 | strangeId {a=Nat} x = x+1
6 | strangeId x = x
7 |
8 | foo : (0 x : Type) -> String
9 | foo Nat = "Nat"
| ^^^
^^^

5
tests/typedd-book/chapter10/expected
View File

@ -2,9 +2,10 @@
Error: While processing left hand side of describe_list_end. Can't match on ?xs ++ [?x] (Not a constructor application or primitive).
DLFail.idr:3:20--3:29
|
1 | describe_list_end : List Int -> String
2 | describe_list_end [] = "Empty"
3 | describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs
| ^^^^^^^^^
^^^^^^^^^
1/13: Building DataStore (DataStore.idr)
2/13: Building DescribeList (DescribeList.idr)