From bb1edab3aacdade82bef9b3995e5a1560bc21150 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Fri, 12 Feb 2021 01:24:26 +0800 Subject: [PATCH] Show more codes in error report --- src/Idris/Error.idr | 7 ++--- tests/chez/chez006/expected | 14 ++++++--- tests/idris2/basic001/expected | 3 +- tests/idris2/basic003/expected | 7 +++-- tests/idris2/basic005/expected | 3 +- tests/idris2/basic011/expected | 4 +-- tests/idris2/basic014/expected | 14 ++++++--- tests/idris2/basic016/expected | 18 ++++++++---- tests/idris2/basic018/expected | 7 +++-- tests/idris2/basic022/expected | 14 ++++++--- tests/idris2/basic030/expected | 6 ++-- tests/idris2/basic031/expected | 7 +++-- tests/idris2/basic033/expected | 14 ++++++--- tests/idris2/basic034/expected | 7 +++-- tests/idris2/basic041/expected | 7 +++-- tests/idris2/basic042/expected | 6 ++-- tests/idris2/basic049/expected | 7 +++-- tests/idris2/coverage003/expected | 7 +++-- tests/idris2/coverage004/expected | 7 +++-- tests/idris2/coverage007/expected | 14 ++++++--- tests/idris2/coverage009/expected | 12 +++++--- tests/idris2/coverage010/expected | 7 +++-- tests/idris2/error001/expected | 7 +++-- tests/idris2/error002/expected | 7 +++-- tests/idris2/error003/expected | 21 ++++++++++---- tests/idris2/error004/expected | 21 ++++++++++---- tests/idris2/error005/expected | 13 ++++++--- tests/idris2/error006/expected | 14 ++++++--- tests/idris2/error007/expected | 6 ++-- tests/idris2/error009/expected | 3 +- tests/idris2/error010/expected | 4 +-- tests/idris2/error011/expected | 10 ++++--- tests/idris2/error013/expected | 21 ++++++++++---- tests/idris2/error014/expected | 14 ++++++--- tests/idris2/import002/expected | 14 ++++++--- tests/idris2/interface008/expected | 7 +++-- tests/idris2/interface013/expected | 7 +++-- tests/idris2/interface015/expected | 21 ++++++++++---- tests/idris2/interface016/expected | 6 ++-- tests/idris2/interface019/expected | 7 +++-- tests/idris2/interpreter003/expected | 3 +- tests/idris2/linear006/expected | 7 +++-- tests/idris2/params001/expected | 7 +++-- tests/idris2/pkg004/expected | 3 +- tests/idris2/record004/expected | 3 +- tests/idris2/reflection001/expected | 21 ++++++++++---- tests/idris2/reflection003/expected | 28 ++++++++++++------ tests/idris2/reflection005/expected | 7 +++-- tests/idris2/reflection006/expected | 7 +++-- tests/idris2/reg003/expected | 43 +++++++++++++++++----------- tests/idris2/reg005/expected | 7 +++-- tests/idris2/reg007/expected | 7 +++-- tests/idris2/reg013/expected | 28 ++++++++++++------ tests/idris2/reg015/expected | 7 +++-- tests/idris2/reg017/expected | 4 +-- tests/idris2/reg019/expected | 21 ++++++++++---- tests/idris2/reg023/expected | 7 +++-- tests/idris2/reg034/expected | 7 +++-- tests/idris2/with003/expected | 24 ++++++---------- tests/node/node006/expected | 14 ++++++--- tests/typedd-book/chapter10/expected | 5 ++-- 61 files changed, 437 insertions(+), 218 deletions(-) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 694064f00..4a5aa703b 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -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 diff --git a/tests/chez/chez006/expected b/tests/chez/chez006/expected index ab4c8b7f5..6ffa25de4 100644 --- a/tests/chez/chez006/expected +++ b/tests/chez/chez006/expected @@ -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" - | ^^^ + ^^^ diff --git a/tests/idris2/basic001/expected b/tests/idris2/basic001/expected index 566ef5c5b..47821e62f 100644 --- a/tests/idris2/basic001/expected +++ b/tests/idris2/basic001/expected @@ -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! diff --git a/tests/idris2/basic003/expected b/tests/idris2/basic003/expected index ef2d4aa3b..1a336211d 100644 --- a/tests/idris2/basic003/expected +++ b/tests/idris2/basic003/expected @@ -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! diff --git a/tests/idris2/basic005/expected b/tests/idris2/basic005/expected index ee63bc4c4..8cd8b371f 100644 --- a/tests/idris2/basic005/expected +++ b/tests/idris2/basic005/expected @@ -2,8 +2,7 @@ Error: Unsolved holes: Main.{_:1} introduced at: NoInfer.idr:1:7--1:8 - | 1 | foo : ? -> Int - | ^ + ^ Main> Bye for now! diff --git a/tests/idris2/basic011/expected b/tests/idris2/basic011/expected index 782b98399..e6b835d2c 100644 --- a/tests/idris2/basic011/expected +++ b/tests/idris2/basic011/expected @@ -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]. diff --git a/tests/idris2/basic014/expected b/tests/idris2/basic014/expected index 99c33de04..e3c8a205c 100644 --- a/tests/idris2/basic014/expected +++ b/tests/idris2/basic014/expected @@ -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 - | ^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/basic016/expected b/tests/idris2/basic016/expected index b7732c96f..7b1d654f4 100644 --- a/tests/idris2/basic016/expected +++ b/tests/idris2/basic016/expected @@ -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 - | ^^^^ + ^^^^ diff --git a/tests/idris2/basic018/expected b/tests/idris2/basic018/expected index 199d16961..34e959bea 100644 --- a/tests/idris2/basic018/expected +++ b/tests/idris2/basic018/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/basic022/expected b/tests/idris2/basic022/expected index f9cabac9e..07e163e7f 100644 --- a/tests/idris2/basic022/expected +++ b/tests/idris2/basic022/expected @@ -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! diff --git a/tests/idris2/basic030/expected b/tests/idris2/basic030/expected index 748d6d3d5..be7ab1777 100644 --- a/tests/idris2/basic030/expected +++ b/tests/idris2/basic030/expected @@ -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 - | ^^^^^ + ^^^^^ diff --git a/tests/idris2/basic031/expected b/tests/idris2/basic031/expected index 7f553fbd4..f1b4ae906 100644 --- a/tests/idris2/basic031/expected +++ b/tests/idris2/basic031/expected @@ -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" - | ^^^^ + ^^^^ diff --git a/tests/idris2/basic033/expected b/tests/idris2/basic033/expected index 598d2c453..da151a1c3 100644 --- a/tests/idris2/basic033/expected +++ b/tests/idris2/basic033/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/basic034/expected b/tests/idris2/basic034/expected index 89a2cb065..237798557 100644 --- a/tests/idris2/basic034/expected +++ b/tests/idris2/basic034/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/basic041/expected b/tests/idris2/basic041/expected index 475032fae..b93caafb7 100644 --- a/tests/idris2/basic041/expected +++ b/tests/idris2/basic041/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/basic042/expected b/tests/idris2/basic042/expected index e5fc4048e..efb1719ce 100644 --- a/tests/idris2/basic042/expected +++ b/tests/idris2/basic042/expected @@ -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! diff --git a/tests/idris2/basic049/expected b/tests/idris2/basic049/expected index e8bb167da..40f1a1878 100644 --- a/tests/idris2/basic049/expected +++ b/tests/idris2/basic049/expected @@ -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 diff --git a/tests/idris2/coverage003/expected b/tests/idris2/coverage003/expected index d76e1f380..c1139cf93 100644 --- a/tests/idris2/coverage003/expected +++ b/tests/idris2/coverage003/expected @@ -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 _, _) diff --git a/tests/idris2/coverage004/expected b/tests/idris2/coverage004/expected index 6da9987db..d09df91d6 100644 --- a/tests/idris2/coverage004/expected +++ b/tests/idris2/coverage004/expected @@ -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 diff --git a/tests/idris2/coverage007/expected b/tests/idris2/coverage007/expected index f4b4b6c93..fc739c50f 100644 --- a/tests/idris2/coverage007/expected +++ b/tests/idris2/coverage007/expected @@ -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 - | ^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/coverage009/expected b/tests/idris2/coverage009/expected index 533bf4b87..7759920f0 100644 --- a/tests/idris2/coverage009/expected +++ b/tests/idris2/coverage009/expected @@ -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 - | ^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index f33573935..8cdf40d1f 100644 --- a/tests/idris2/coverage010/expected +++ b/tests/idris2/coverage010/expected @@ -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 diff --git a/tests/idris2/error001/expected b/tests/idris2/error001/expected index 89f21d34a..8208910b8 100644 --- a/tests/idris2/error001/expected +++ b/tests/idris2/error001/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/error002/expected b/tests/idris2/error002/expected index ef296b495..3809cb31f 100644 --- a/tests/idris2/error002/expected +++ b/tests/idris2/error002/expected @@ -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 - | ^^ + ^^ diff --git a/tests/idris2/error003/expected b/tests/idris2/error003/expected index 932717ee4..89a1658df 100644 --- a/tests/idris2/error003/expected +++ b/tests/idris2/error003/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/error004/expected b/tests/idris2/error004/expected index 6c5928f45..04bdba943 100644 --- a/tests/idris2/error004/expected +++ b/tests/idris2/error004/expected @@ -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 diff --git a/tests/idris2/error005/expected b/tests/idris2/error005/expected index 288b735e0..4017ebd1f 100644 --- a/tests/idris2/error005/expected +++ b/tests/idris2/error005/expected @@ -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 - | ^^^^^^ + ^^^^^^ diff --git a/tests/idris2/error006/expected b/tests/idris2/error006/expected index cf184c886..f6bfa2cff 100644 --- a/tests/idris2/error006/expected +++ b/tests/idris2/error006/expected @@ -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 - | ^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/error007/expected b/tests/idris2/error007/expected index 3b687853c..d46bc2042 100644 --- a/tests/idris2/error007/expected +++ b/tests/idris2/error007/expected @@ -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 - | ^^^^^^^^ + ^^^^^^^^ diff --git a/tests/idris2/error009/expected b/tests/idris2/error009/expected index 0bf2d190d..4b7ce5e67 100644 --- a/tests/idris2/error009/expected +++ b/tests/idris2/error009/expected @@ -1,8 +1,7 @@ Error: Module DoesntExist not found Exists.idr:1:1--1:19 - | 1 | import DoesntExist - | ^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^ Main> Bye for now! diff --git a/tests/idris2/error010/expected b/tests/idris2/error010/expected index e1003b1a8..d816e79c3 100644 --- a/tests/idris2/error010/expected +++ b/tests/idris2/error010/expected @@ -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 - | ^^^^^^^^ + ^^^^^^^^ diff --git a/tests/idris2/error011/expected b/tests/idris2/error011/expected index a14027ad6..e2d208aad 100644 --- a/tests/idris2/error011/expected +++ b/tests/idris2/error011/expected @@ -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 - | ^^^^^^^^^^^^ + ^^^^^^^^^^^^ diff --git a/tests/idris2/error013/expected b/tests/idris2/error013/expected index fba1d1630..802ebd219 100644 --- a/tests/idris2/error013/expected +++ b/tests/idris2/error013/expected @@ -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 - | ^^^^^^^^^^ + ^^^^^^^^^^ diff --git a/tests/idris2/error014/expected b/tests/idris2/error014/expected index 881c7243d..5be2be6d9 100644 --- a/tests/idris2/error014/expected +++ b/tests/idris2/error014/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/import002/expected b/tests/idris2/import002/expected index e37f8a5ee..f8d5c4028 100644 --- a/tests/idris2/import002/expected +++ b/tests/idris2/import002/expected @@ -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! diff --git a/tests/idris2/interface008/expected b/tests/idris2/interface008/expected index 2f94c41ab..3ef283542 100644 --- a/tests/idris2/interface008/expected +++ b/tests/idris2/interface008/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/interface013/expected b/tests/idris2/interface013/expected index bf92e2461..0d94d6ecd 100644 --- a/tests/idris2/interface013/expected +++ b/tests/idris2/interface013/expected @@ -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 - | ^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/interface015/expected b/tests/idris2/interface015/expected index be32148bf..15957427f 100644 --- a/tests/idris2/interface015/expected +++ b/tests/idris2/interface015/expected @@ -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 - | ^^^^^ + ^^^^^ diff --git a/tests/idris2/interface016/expected b/tests/idris2/interface016/expected index d34d15911..48dc1f509 100644 --- a/tests/idris2/interface016/expected +++ b/tests/idris2/interface016/expected @@ -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) diff --git a/tests/idris2/interface019/expected b/tests/idris2/interface019/expected index d40560aae..7666049b1 100644 --- a/tests/idris2/interface019/expected +++ b/tests/idris2/interface019/expected @@ -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) - | ^^^^^ + ^^^^^ diff --git a/tests/idris2/interpreter003/expected b/tests/idris2/interpreter003/expected index b8282609e..74faa2dba 100644 --- a/tests/idris2/interpreter003/expected +++ b/tests/idris2/interpreter003/expected @@ -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" diff --git a/tests/idris2/linear006/expected b/tests/idris2/linear006/expected index 0fc676e6d..34d3c75d3 100644 --- a/tests/idris2/linear006/expected +++ b/tests/idris2/linear006/expected @@ -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! diff --git a/tests/idris2/params001/expected b/tests/idris2/params001/expected index 875267cbd..899ac4e54 100644 --- a/tests/idris2/params001/expected +++ b/tests/idris2/params001/expected @@ -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. diff --git a/tests/idris2/pkg004/expected b/tests/idris2/pkg004/expected index b500b1b9a..ad4a86f3d 100644 --- a/tests/idris2/pkg004/expected +++ b/tests/idris2/pkg004/expected @@ -2,9 +2,8 @@ Dummy> Error: Undefined name undefined. (interactive):1:4--1:13 - | 1 | :t undefined - | ^^^^^^^^^ + ^^^^^^^^^ Dummy> Dummy.something : String Dummy> "Something something" diff --git a/tests/idris2/record004/expected b/tests/idris2/record004/expected index 0bcedffdb..19040ee3f 100644 --- a/tests/idris2/record004/expected +++ b/tests/idris2/record004/expected @@ -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 diff --git a/tests/idris2/reflection001/expected b/tests/idris2/reflection001/expected index 8736c8fd6..38097754c 100644 --- a/tests/idris2/reflection001/expected +++ b/tests/idris2/reflection001/expected @@ -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")) diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 4c6f1765b..5dc50fa17 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -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 - | ^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/reflection005/expected b/tests/idris2/reflection005/expected index 1ec589c83..df7b5f2c1 100644 --- a/tests/idris2/reflection005/expected +++ b/tests/idris2/reflection005/expected @@ -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! diff --git a/tests/idris2/reflection006/expected b/tests/idris2/reflection006/expected index daab6248e..6b945263b 100644 --- a/tests/idris2/reflection006/expected +++ b/tests/idris2/reflection006/expected @@ -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 - | ^^^^^ + ^^^^^ diff --git a/tests/idris2/reg003/expected b/tests/idris2/reg003/expected index c374b6142..1d12202e7 100644 --- a/tests/idris2/reg003/expected +++ b/tests/idris2/reg003/expected @@ -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! diff --git a/tests/idris2/reg005/expected b/tests/idris2/reg005/expected index 67306eed1..4e897b4d7 100644 --- a/tests/idris2/reg005/expected +++ b/tests/idris2/reg005/expected @@ -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 - | ^^^^ + ^^^^ diff --git a/tests/idris2/reg007/expected b/tests/idris2/reg007/expected index 947762612..5cfb4c238 100644 --- a/tests/idris2/reg007/expected +++ b/tests/idris2/reg007/expected @@ -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]}))] - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/reg013/expected b/tests/idris2/reg013/expected index f85e0fcdf..0f586b6a2 100644 --- a/tests/idris2/reg013/expected +++ b/tests/idris2/reg013/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/reg015/expected b/tests/idris2/reg015/expected index 67a271682..6afc87ba9 100644 --- a/tests/idris2/reg015/expected +++ b/tests/idris2/reg015/expected @@ -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 - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/reg017/expected b/tests/idris2/reg017/expected index 5bb3f132d..1e49e26cd 100644 --- a/tests/idris2/reg017/expected +++ b/tests/idris2/reg017/expected @@ -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) - | ^ + ^ diff --git a/tests/idris2/reg019/expected b/tests/idris2/reg019/expected index 68211dc22..498866f48 100644 --- a/tests/idris2/reg019/expected +++ b/tests/idris2/reg019/expected @@ -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 - | ^^^^^ + ^^^^^ diff --git a/tests/idris2/reg023/expected b/tests/idris2/reg023/expected index 7caeba32d..aa7a74433 100644 --- a/tests/idris2/reg023/expected +++ b/tests/idris2/reg023/expected @@ -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 - | ^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/idris2/reg034/expected b/tests/idris2/reg034/expected index c91238662..1c5172028 100644 --- a/tests/idris2/reg034/expected +++ b/tests/idris2/reg034/expected @@ -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 - | ^ + ^ diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index 4bff9f2fa..8d5f64028 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -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: diff --git a/tests/node/node006/expected b/tests/node/node006/expected index ab4c8b7f5..6ffa25de4 100644 --- a/tests/node/node006/expected +++ b/tests/node/node006/expected @@ -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" - | ^^^ + ^^^ diff --git a/tests/typedd-book/chapter10/expected b/tests/typedd-book/chapter10/expected index dd943179c..220df863f 100644 --- a/tests/typedd-book/chapter10/expected +++ b/tests/typedd-book/chapter10/expected @@ -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)