diff --git a/tests/chez/chez006/expected b/tests/chez/chez006/expected index e3982e0c4..4dd529de0 100644 --- a/tests/chez/chez006/expected +++ b/tests/chez/chez006/expected @@ -16,6 +16,12 @@ strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) TypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1: -Can't match on Nat (Erased argument) +Can't match on Nat (Erased argument) at +5 strangeId {a=Nat} x = x+1 + ^^^ + TypeCase2.idr:9:5--9:9:While processing left hand side of foo at TypeCase2.idr:9:1--10:1: -Can't match on Nat (Erased argument) +Can't match on Nat (Erased argument) at +9 foo Nat = "Nat" + ^^^^ + diff --git a/tests/idris2/basic001/expected b/tests/idris2/basic001/expected index f5e5713d7..4efe30d7c 100644 --- a/tests/idris2/basic001/expected +++ b/tests/idris2/basic001/expected @@ -5,4 +5,8 @@ Mismatch between: S Z and Z +at: +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 ac42e64df..c6a8ff508 100644 --- a/tests/idris2/basic003/expected +++ b/tests/idris2/basic003/expected @@ -2,7 +2,10 @@ Main> Bye for now! 1/1: Building Ambig2 (Ambig2.idr) Ambig2.idr:26:21--26:28:While processing right hand side of keepUnique at Ambig2.idr:26:1--28:1: -Ambiguous elaboration. Possible correct results: +Ambiguous elaboration at: +26 keepUnique {b} xs = toList (fromList xs) + ^^^^^^^ +Possible correct results: Main.Set.toList ?arg Main.Vect.toList ?arg Main> Bye for now! diff --git a/tests/idris2/basic011/expected b/tests/idris2/basic011/expected index 9eed2a0cb..0a4c61dde 100644 --- a/tests/idris2/basic011/expected +++ b/tests/idris2/basic011/expected @@ -1,8 +1,15 @@ 1/1: Building Dots1 (Dots1.idr) 1/1: Building Dots2 (Dots2.idr) Dots2.idr:2:7--2:9:While processing left hand side of foo at Dots2.idr:2:1--4:1: -Can't match on ?x [no locals in scope] (Non linear pattern variable) +Can't match on ?x [no locals in scope] (Non linear pattern variable) at +2 foo x x = x + x + ^^ + 1/1: Building Dots3 (Dots3.idr) Dots3.idr:5:29--5:30:While processing left hand side of addBaz at Dots3.idr:5:1--6:1: Pattern variable z unifies with: ?y [no locals in scope] +at: +5 addBaz (x + y) (AddThings x z) = x + y + ^ + diff --git a/tests/idris2/basic014/expected b/tests/idris2/basic014/expected index 0736f4dd3..c75f94686 100644 --- a/tests/idris2/basic014/expected +++ b/tests/idris2/basic014/expected @@ -1,5 +1,11 @@ 1/1: Building Rewrite (Rewrite.idr) Rewrite.idr:15:25--17:1:While processing right hand side of wrongCommutes at Rewrite.idr:15:1--17:1: -Rewriting by m + k = k + m did not change type S k + m = m + S k +Rewriting by m + k = k + m did not change type S k + m = m + S k at: +15 wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar +16 +17 wrongCommutes2 : (n, m : Nat) -> n + m = m + n + Rewrite.idr:19:26--20:1:While processing right hand side of wrongCommutes2 at Rewrite.idr:19:1--20:1: -Nat is not a rewrite rule type +Nat is not a rewrite rule type at: +19 wrongCommutes2 (S k) m = rewrite m in ?bar + diff --git a/tests/idris2/basic016/expected b/tests/idris2/basic016/expected index 55a394e9d..a16119c1e 100644 --- a/tests/idris2/basic016/expected +++ b/tests/idris2/basic016/expected @@ -5,6 +5,9 @@ Mismatch between: Nat and Integer +at: +14 etaBad = Refl + 1/1: Building Eta2 (Eta2.idr) Eta2.idr:2:8--4:1:While processing right hand side of test at Eta2.idr:2:1--4:1: When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_) @@ -12,9 +15,17 @@ Mismatch between: a and Nat +at: +2 test = Refl +3 +4 test2 : ? + Eta2.idr:5:44--6:1:While processing right hand side of test2 at Eta2.idr:5:1--6:1: When unifying \x => (S ?_) = \x => (S ?_) and S = \x => (S ?_) Mismatch between: a and Nat +at: +5 test2 = {a : _} -> the (S = \x : a => S _) Refl + diff --git a/tests/idris2/basic018/expected b/tests/idris2/basic018/expected index a3296b165..cc00cc4cb 100644 --- a/tests/idris2/basic018/expected +++ b/tests/idris2/basic018/expected @@ -1,3 +1,6 @@ 1/1: Building Fin (Fin.idr) Fin.idr:34:7--36:1:While processing right hand side of bar at Fin.idr:34:1--36:1: -Can't find an implementation for IsJust (integerToFin 8 5) +Can't find an implementation for IsJust (integerToFin 8 5) at: +34 bar = 8 +35 + diff --git a/tests/idris2/basic022/expected b/tests/idris2/basic022/expected index 53243c8b9..757fcae93 100644 --- a/tests/idris2/basic022/expected +++ b/tests/idris2/basic022/expected @@ -1,7 +1,13 @@ 1/1: Building Erase (Erase.idr) Erase.idr:5:5--5:11:While processing left hand side of bad at Erase.idr:5:1--6:1: -Can't match on False (Erased argument) +Can't match on False (Erased argument) at +5 bad False = True + ^^^^^^ + Erase.idr:19:18--19:22:While processing left hand side of minusBad at Erase.idr:19:1--20:1: -Can't match on LeZ (Erased argument) +Can't match on LeZ (Erased argument) at +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 3b5d7ffc7..d00172ef9 100644 --- a/tests/idris2/basic030/expected +++ b/tests/idris2/basic030/expected @@ -5,3 +5,7 @@ Mismatch between: (1 _ : Nat) -> MyN and MyN +at: +4 foo x y = case MkN x of + ^^^^^^ + diff --git a/tests/idris2/basic031/expected b/tests/idris2/basic031/expected index 76a14f909..68110935e 100644 --- a/tests/idris2/basic031/expected +++ b/tests/idris2/basic031/expected @@ -1,3 +1,6 @@ 1/1: Building erased (erased.idr) erased.idr:7:17--7:21:While processing left hand side of nameOf at erased.idr:7:1--8:1: -Can't match on Bool (Erased argument) +Can't match on Bool (Erased argument) at +7 nameOf (MyMaybe Bool) = "MyMaybe Bool" + ^^^^ + diff --git a/tests/idris2/basic033/expected b/tests/idris2/basic033/expected index b65d61a56..b635b7fb2 100644 --- a/tests/idris2/basic033/expected +++ b/tests/idris2/basic033/expected @@ -1,5 +1,11 @@ 1/1: Building unboundimps (unboundimps.idr) unboundimps.idr:18:11--18:14:While processing type of len' at unboundimps.idr:18:1--19:1: -Undefined name xs +Undefined name xs at: +18 len': Env xs -> Nat + ^^^ + unboundimps.idr:19:16--19:18:While processing type of append' at unboundimps.idr:19:1--21:1: -Undefined name n +Undefined name n at: +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 b4d5f27a2..07c57462c 100644 --- a/tests/idris2/basic034/expected +++ b/tests/idris2/basic034/expected @@ -5,3 +5,7 @@ Mismatch between: Int and String +at: +22 = do let Just x' : Maybe String = x +23 | Nothing => Nothing + diff --git a/tests/idris2/coverage003/expected b/tests/idris2/coverage003/expected index b4aae9a68..b23de4bc7 100644 --- a/tests/idris2/coverage003/expected +++ b/tests/idris2/coverage003/expected @@ -1,6 +1,9 @@ 1/1: Building Cover (Cover.idr) Cover.idr:16:1--16:8:While processing left hand side of badBar at Cover.idr:16:1--17:1: -Can't match on 0 as it has a polymorphic type +Can't match on 0 as it has a polymorphic type at: +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 2c5e03158..f6bc453c9 100644 --- a/tests/idris2/coverage004/expected +++ b/tests/idris2/coverage004/expected @@ -1,6 +1,9 @@ 1/1: Building Cover (Cover.idr) Cover.idr:14:1--14:5:While processing left hand side of bad at Cover.idr:14:1--15:1: -Can't match on Just (fromInteger 0) as it has a polymorphic type +Can't match on Just (fromInteger 0) as it has a polymorphic type at: +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 0223f4751..de498bd00 100644 --- a/tests/idris2/coverage007/expected +++ b/tests/idris2/coverage007/expected @@ -1,3 +1,9 @@ 1/1: Building eq (eq.idr) -eq.idr:27:1--29:1:badeq x y p is not a valid impossible case -eq.idr:30:1--31:1:badeqL xs ys p is not a valid impossible case +eq.idr:27:1--29:1:badeq x y p is not a valid impossible case at: +27 badeq x y p impossible +28 +29 badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat + +eq.idr:30:1--31:1:badeqL xs ys p is not a valid impossible case at: +30 badeqL xs ys p impossible + diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index b1bc35648..7d7d79445 100644 --- a/tests/idris2/coverage010/expected +++ b/tests/idris2/coverage010/expected @@ -1,3 +1,6 @@ 1/1: Building casetot (casetot.idr) -casetot.idr:12:1--13:1:main is not covering: +casetot.idr:12:1--13:1:main is not covering at: +12 main : IO () +13 main = do + Calls non covering function Main.case block in 2071(287) diff --git a/tests/idris2/error001/expected b/tests/idris2/error001/expected index eb1690742..67e5efc63 100644 --- a/tests/idris2/error001/expected +++ b/tests/idris2/error001/expected @@ -5,3 +5,6 @@ Mismatch between: a and Vect ?k ?a +at: +6 wrong x xs = x :: x + diff --git a/tests/idris2/error002/expected b/tests/idris2/error002/expected index e685a566e..eed329850 100644 --- a/tests/idris2/error002/expected +++ b/tests/idris2/error002/expected @@ -1,3 +1,5 @@ 1/1: Building Error (Error.idr) Error.idr:6:17--7:1:While processing right hand side of wrong at Error.idr:6:1--7:1: -Undefined name ys +Undefined name ys at: +6 wrong xs = x :: ys + diff --git a/tests/idris2/error003/expected b/tests/idris2/error003/expected index fd1c8093a..436bf818e 100644 --- a/tests/idris2/error003/expected +++ b/tests/idris2/error003/expected @@ -6,16 +6,25 @@ Mismatch between: Nat and Vect ?n ?a +at: +12 wrong x = length x + If Data.List.length: When unifying Nat and List ?a Mismatch between: Nat and List ?a +at: +12 wrong x = length x + If Prelude.length: When unifying Nat and String Mismatch between: Nat and String +at: +12 wrong x = length x + diff --git a/tests/idris2/error004/expected b/tests/idris2/error004/expected index aa0572797..e052488ee 100644 --- a/tests/idris2/error004/expected +++ b/tests/idris2/error004/expected @@ -1,16 +1,26 @@ 1/1: Building Error1 (Error1.idr) Error1.idr:8:9--9:1:While processing right hand side of wrong at Error1.idr:8:1--9:1: -Can't find an implementation for Show (Vect 4 Integer) +Can't find an implementation for Show (Vect 4 Integer) at: +8 wrong = show (the (Vect _ _) [1,2,3,4]) + 1/1: Building Error2 (Error2.idr) Error2.idr:13:38--15:1:While processing right hand side of show at Error2.idr:13:3--15:1: Multiple solutions found in search of: Show (Vect k Integer) +at: +13 show (x :: xs) = show x ++ ", " ++ show xs +14 +15 wrong : String + Possible correct results: Show implementation at Error2.idr:11:1--15:1 Show implementation at Error2.idr:7:1--11:1 Error2.idr:16:9--17:1:While processing right hand side of wrong at Error2.idr:16:1--17:1: Multiple solutions found in search of: Show (Vect 1 Integer) +at: +16 wrong = show (the (Vect _ _) [1]) + Possible correct results: Show implementation at Error2.idr:11:1--15:1 Show implementation at Error2.idr:7:1--11:1 diff --git a/tests/idris2/error005/expected b/tests/idris2/error005/expected index 24dcdd0cd..4f3808576 100644 --- a/tests/idris2/error005/expected +++ b/tests/idris2/error005/expected @@ -1,5 +1,11 @@ 1/1: Building IfErr (IfErr.idr) IfErr.idr:4:11--6:1:While processing right hand side of foo at IfErr.idr:4:1--6:1: -Can't find an implementation for Eq a +Can't find an implementation for Eq a at: +4 foo x y = x == y +5 +6 bar : Wibble -> Wibble -> Bool + IfErr.idr:7:11--8:1:While processing right hand side of bar at IfErr.idr:7:1--8:1: -Can't find an implementation for Eq Wibble +Can't find an implementation for Eq Wibble at: +7 bar x y = x == y + diff --git a/tests/idris2/error006/expected b/tests/idris2/error006/expected index 9a8c9b386..1fc52ba5f 100644 --- a/tests/idris2/error006/expected +++ b/tests/idris2/error006/expected @@ -1,5 +1,12 @@ 1/1: Building IfErr (IfErr.idr) IfErr.idr:15:10--17:1:While processing right hand side of test at IfErr.idr:15:1--17:1: -Can't find an implementation for Eq Foo +Can't find an implementation for Eq Foo at: +15 test x = showIfEq MkFoo MkBar +16 +17 Eq Foo where + IfErr.idr:23:9--25:1:While processing right hand side of test2 at IfErr.idr:23:1--25:1: -Can't find an implementation for Show Foo +Can't find an implementation for Show Foo at: +23 test2 = showIfEq MkFoo MkBar +24 + diff --git a/tests/idris2/error007/expected b/tests/idris2/error007/expected index 0c9af99e2..6b0f58fae 100644 --- a/tests/idris2/error007/expected +++ b/tests/idris2/error007/expected @@ -4,3 +4,6 @@ Can't solve constraint between: ?_ x and FS x +at: +4 fsprf p = cong _ p + diff --git a/tests/idris2/import002/expected b/tests/idris2/import002/expected index 55ed33367..d604f18aa 100644 --- a/tests/idris2/import002/expected +++ b/tests/idris2/import002/expected @@ -2,6 +2,12 @@ 2/3: Building Mult (Mult.idr) 3/3: Building Test (Test.idr) Test.idr:5:9--5:13:While processing type of thing at Test.idr:5:1--6:1: -Undefined name Nat -Test.idr:6:1--8:1:No type declaration for Test.thing +Undefined name Nat at: +5 thing : Nat -> Nat + ^^^^ + +Test.idr:6:1--8:1:No type declaration for Test.thing at: +6 thing x = mult x (plus x x) +7 + Test> Bye for now! diff --git a/tests/idris2/interface008/expected b/tests/idris2/interface008/expected index c5361ee3b..ae335b355 100644 --- a/tests/idris2/interface008/expected +++ b/tests/idris2/interface008/expected @@ -1,3 +1,6 @@ 1/1: Building Deps (Deps.idr) Deps.idr:18:13--19:3:While processing right hand side of badcard at Deps.idr:18:3--19:3: -k is not accessible in this context +k is not accessible in this context at: +18 badcard = k +19 badto = id + diff --git a/tests/idris2/interface013/expected b/tests/idris2/interface013/expected index 2d168397f..ecd63d0b2 100644 --- a/tests/idris2/interface013/expected +++ b/tests/idris2/interface013/expected @@ -1,3 +1,6 @@ 1/1: Building TypeInt (TypeInt.idr) TypeInt.idr:14:25--14:50:While processing constructor MkRecord at TypeInt.idr:14:3--15:1: -Can't find an implementation for Interface ?s +Can't find an implementation for Interface ?s at: +14 MkRecord : Value s -> DependentValue {s} value -> Record s + ^^^^^^^^^^^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/interface015/expected b/tests/idris2/interface015/expected index c6279a1d6..6997501b7 100644 --- a/tests/idris2/interface015/expected +++ b/tests/idris2/interface015/expected @@ -2,14 +2,26 @@ gnu.idr:47:27--49:1:While processing right hand side of TestSurprise1 at gnu.idr:47:1--49:1: Multiple solutions found in search of: Gnu +at: +47 TestSurprise1 gnu1 gnu2 = Guess +48 +49 TestSurprise2 : (f,g : Unit -> Gnu) -> String + Possible correct results: gnu1 gnu2 gnu.idr:50:21--52:1:While processing right hand side of TestSurprise2 at gnu.idr:50:1--52:1: Multiple solutions found in search of: Gnu +at: +50 TestSurprise2 f g = Guess +51 +52 TestSurprise3 : (Unit -> Gnu, Unit -> Gnu) -> String + Possible correct results: f () g () gnu.idr:53:19--54:1:While processing right hand side of TestSurprise3 at gnu.idr:53:1--54:1: -Can't find an implementation for Gnu +Can't find an implementation for Gnu at: +53 TestSurprise3 f = Guess + diff --git a/tests/idris2/interface016/expected b/tests/idris2/interface016/expected index 25b1db8e5..fbcf2afd4 100644 --- a/tests/idris2/interface016/expected +++ b/tests/idris2/interface016/expected @@ -3,6 +3,9 @@ TwoNum.idr:4:7--5:1:While processing right hand side of f at TwoNum.idr:2:1--5:1 While processing right hand side of f,g at TwoNum.idr:4:3--5:1: Multiple solutions found in search of: Num a +at: +4 g = 0 + Possible correct results: conArg conArg diff --git a/tests/idris2/linear004/expected b/tests/idris2/linear004/expected index 08bc95d2c..5fc45d234 100644 --- a/tests/idris2/linear004/expected +++ b/tests/idris2/linear004/expected @@ -3,18 +3,32 @@ Main> S Z Main> S (S Z) Main> S Z -Main> (interactive):1:15--1:16:x is not accessible in this context +Main> (interactive):1:15--1:16:x is not accessible in this context at: +1 efn (\x, y => x) -- Bad + ^ + Main> (interactive):1:5--1:31:When unifying Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat Mismatch between: Nat -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat +at: +1 efn plus -- Bad + ^^^^^^^^^^^^^^^^^^^^^^^^^^ + Main> (interactive):1:5--1:31:When unifying (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat Mismatch between: (1 _ : Nat) -> Nat -> Nat and (0 _ : Nat) -> Nat -> Nat -Main> (interactive):1:20--1:22:x is not accessible in this context +at: +1 efn lin -- Bad + ^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Main> (interactive):1:20--1:22:x is not accessible in this context at: +1 efn (\x, y => plus x y) -- Bad + ^^ + Main> S (S Z) Main> S (S Z) Main> (interactive):1:6--1:31:When unifying (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat @@ -22,4 +36,8 @@ Mismatch between: (0 _ : Nat) -> Nat -> Nat and Nat -> Nat -> Nat +at: +1 okfn ignore -- Bad + ^^^^^^^^^^^^^^^^^^^^^^^^^ + Main> Bye for now! diff --git a/tests/idris2/linear006/expected b/tests/idris2/linear006/expected index 3a50bd445..2db636a55 100644 --- a/tests/idris2/linear006/expected +++ b/tests/idris2/linear006/expected @@ -1,5 +1,8 @@ 1/1: Building ZFun (ZFun.idr) ZFun.idr:13:7--15:1:While processing right hand side of bar at ZFun.idr:13:1--15:1: -Main.test is not accessible in this context +Main.test is not accessible in this context at: +13 bar = test foo -- bad! +14 + Main> [tc] Main> 10 [tc] Main> Bye for now! diff --git a/tests/idris2/linear007/expected b/tests/idris2/linear007/expected index 480d6cd06..16430aae4 100644 --- a/tests/idris2/linear007/expected +++ b/tests/idris2/linear007/expected @@ -1,3 +1,8 @@ 1/1: Building LCase (LCase.idr) LCase.idr:7:11--10:13:While processing right hand side of foo at LCase.idr:6:1--12:1: -There are 0 uses of linear name y +There are 0 uses of linear name y at: +7 = let 1 test = the Nat $ case z of +8 Z => Z +9 (S k) => S z +10 in + diff --git a/tests/idris2/params001/expected b/tests/idris2/params001/expected index 4b8fcb1ae..bc747d9c8 100644 --- a/tests/idris2/params001/expected +++ b/tests/idris2/params001/expected @@ -1,4 +1,6 @@ 1/1: Building param (param.idr) 1/1: Building parambad (parambad.idr) parambad.idr:7:7--8:1:While processing right hand side of U at parambad.idr:7:3--8:1: -Name Main.X.foo is private +Name Main.X.foo is private at: +7 U = foo + diff --git a/tests/idris2/record004/expected b/tests/idris2/record004/expected index 094cb3aea..377cbab37 100644 --- a/tests/idris2/record004/expected +++ b/tests/idris2/record004/expected @@ -11,6 +11,10 @@ Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point +at: +1 map .x [MkPoint 1 2, MkPoint 3 4] + ^^^^ + Main> [2.5, 2.5] Main> 7.4 Main> 4.2 diff --git a/tests/idris2/reflection001/expected b/tests/idris2/reflection001/expected index 388168ca1..656a8156e 100644 --- a/tests/idris2/reflection001/expected +++ b/tests/idris2/reflection001/expected @@ -5,6 +5,10 @@ Mismatch between: Int and TTImp +at: +25 xfn ~(val)) + ^^^ + 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")) Main> ILocal (MkFC "quote.idr" (10, 8) (12, 22)) [IClaim (MkFC "quote.idr" (10, 12) (11, 12)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (11, 12)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (11, 12)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 22)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (11, 12)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 30)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 30)) (IApp (MkFC "quote.idr" (11, 12) (11, 20)) (IVar (MkFC "quote.idr" (11, 12) (11, 16)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 20)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 30)) (IApp (MkFC "quote.idr" (11, 22) (11, 30)) (IVar (MkFC "quote.idr" (11, 22) (11, 30)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 26)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 30)) (IVar (MkFC "quote.idr" (11, 28) (11, 30)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 30)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 16)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 13)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 17)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994))))) diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 34042f6d7..8332bb907 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -6,10 +6,25 @@ LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) Stri LOG 0: Resolved name: Prelude.Nat LOG 0: Constructors: [Prelude.Z, Prelude.S] refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1: -Error during reflection: Not really trying +Error during reflection: Not really trying at: +37 dummy1 = %runElab logPrims +38 +39 dummy2 : a + refprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1: -Error during reflection: Still not trying +Error during reflection: Still not trying at: +40 dummy2 = %runElab logDataCons +41 +42 dummy3 : a + refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1: -Error during reflection: Undefined name +Error during reflection: Undefined name at: +43 dummy3 = %runElab logBad +44 +45 dummy4 : a + refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1: -Error during reflection: failed after generating Main.{plus:6078} +Error during reflection: failed after generating Main.{plus:6078} at: +46 dummy4 = %runElab tryGenSym +47 + diff --git a/tests/idris2/reflection005/expected b/tests/idris2/reflection005/expected index 12df87bd9..8bcf80352 100644 --- a/tests/idris2/reflection005/expected +++ b/tests/idris2/reflection005/expected @@ -5,5 +5,8 @@ Mismatch between: () and a +at: +13 bad = %runElab mkDecls `(94) + Main> 9400 Main> Bye for now! diff --git a/tests/idris2/reflection006/expected b/tests/idris2/reflection006/expected index 0b15c0f7b..d457403e1 100644 --- a/tests/idris2/reflection006/expected +++ b/tests/idris2/reflection006/expected @@ -3,4 +3,6 @@ LOG 0: [x, y] LOG 0: Left: ((Prelude.plus x) y) LOG 0: Right: ((Prelude.plus y) x) refleq.idr:24:16--25:1:While processing right hand side of commutes at refleq.idr:24:1--25:1: -Error during reflection: Not done +Error during reflection: Not done at: +24 commutes x y = prove + diff --git a/tests/idris2/reg003/expected b/tests/idris2/reg003/expected index 73cb02d37..03a9130c2 100644 --- a/tests/idris2/reg003/expected +++ b/tests/idris2/reg003/expected @@ -1,14 +1,39 @@ 1/1: Building Holes (Holes.idr) Holes.idr:4:64--4:85:While processing type of Vect_ext at Holes.idr:4:1--7:1: -Undefined name ~=~ +Undefined name ~=~ at: +4 Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w) + ^^^^^^^^^^^^^^^^^^^^^ + Holes.idr:7:26--8:1:While processing type of Weird at Holes.idr:7:1--8:1: -Undefined name ~=~ -Holes.idr:8:1--10:1:No type declaration for Main.Weird +Undefined name ~=~ at: +7 Weird : (v: Vect n a) -> v = v +8 Weird v = Vect_ext ?hole0 ?hole1 ?hole2 + +Holes.idr:8:1--10:1:No type declaration for Main.Weird at: +8 Weird v = Vect_ext ?hole0 ?hole1 ?hole2 +9 +10 f : Bool -> Nat + Holes.idr:10:5--10:10:While processing type of f at Holes.idr:10:1--11:1: -Undefined name Bool -Holes.idr:11:1--12:1:No type declaration for Main.f -Main> (interactive):1:4--1:8:Undefined name help -Main> (interactive):1:4--1:9:Undefined name hole0 -Main> (interactive):1:4--1:9:Undefined name hole1 +Undefined name Bool at: +10 f : Bool -> Nat + ^^^^^ + +Holes.idr:11:1--12:1:No type declaration for Main.f at: +11 f True = 0 +12 f True = ?help + +Main> (interactive):1:4--1:8:Undefined name help at: +1 :t help + ^^^^ + +Main> (interactive):1:4--1:9:Undefined name hole0 at: +1 :t hole0 + ^^^^^ + +Main> (interactive):1:4--1:9:Undefined name hole1 at: +1 :t hole1 + ^^^^^ + Main> Unknown name hole1 Main> Bye for now! diff --git a/tests/idris2/reg005/expected b/tests/idris2/reg005/expected index a487de8a8..e6bed0c54 100644 --- a/tests/idris2/reg005/expected +++ b/tests/idris2/reg005/expected @@ -4,3 +4,6 @@ Can't solve constraint between: if c then "Foo" else "Baz" and if c then "Foo" else "Bar" +at: +15 isInListBad = Here + diff --git a/tests/idris2/reg007/expected b/tests/idris2/reg007/expected index 23d2a4bb4..fae267782 100644 --- a/tests/idris2/reg007/expected +++ b/tests/idris2/reg007/expected @@ -5,3 +5,7 @@ Mismatch between: [MN 0] and [] +at: +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 7aa2491fc..de1541545 100644 --- a/tests/idris2/reg013/expected +++ b/tests/idris2/reg013/expected @@ -1,8 +1,20 @@ 1/1: Building UnboundImplicits (UnboundImplicits.idr) UnboundImplicits.idr:6:22--6:24:While processing constructor Foo at UnboundImplicits.idr:6:1--9:1: -Undefined name n -UnboundImplicits.idr:9:24--9:26:Undefined name n +Undefined name n at: +6 record Foo (x : Vect n Nat) where + ^^ + +UnboundImplicits.idr:9:24--9:26:Undefined name n at: +9 parameters (Foo : Vect n Nat) + ^^ + UnboundImplicits.idr:14:25--14:27:While processing constructor Foo at UnboundImplicits.idr:14:1--17:1: -Undefined name n +Undefined name n at: +14 interface Foo (a : Vect n Nat) where + ^^ + UnboundImplicits.idr:17:30--17:31:While processing type of Functor implementation at UnboundImplicits.idr:17:1--18:1 at UnboundImplicits.idr:17:1--18:1: -Undefined name n +Undefined name n at: +17 implementation Functor (Vect n) where + ^ + diff --git a/tests/idris2/reg015/expected b/tests/idris2/reg015/expected index fea580ce3..69618f6a9 100644 --- a/tests/idris2/reg015/expected +++ b/tests/idris2/reg015/expected @@ -1,2 +1,4 @@ 1/1: Building anyfail (anyfail.idr) -anyfail.idr:21:1--22:1:showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is not a valid impossible case +anyfail.idr:21:1--22:1:showing (MkEvenMoreComplicated (MkMoreComplicated (MkComplicated (PtrAndSize addr len)))) SomethingVeryComplicatedIs is not a valid impossible case at: +21 showing _ SomethingVeryComplicatedIs impossible + diff --git a/tests/idris2/reg017/expected b/tests/idris2/reg017/expected index 575f2925d..3fed643d2 100644 --- a/tests/idris2/reg017/expected +++ b/tests/idris2/reg017/expected @@ -5,3 +5,7 @@ Mismatch between: (0 _ : ?a) -> ?b and ?a -> ?b +at: +2 badmap = map (\0 x => 2) + ^^^^^^^^^ + diff --git a/tests/idris2/reg019/expected b/tests/idris2/reg019/expected index 890ee18f2..97a72dfe5 100644 --- a/tests/idris2/reg019/expected +++ b/tests/idris2/reg019/expected @@ -4,13 +4,24 @@ Can't solve constraint between: Bool and Lazy Bool +at: +5 main = printLn $ or (map id bools) + ^^^^^^^^^^^^ + lazybug.idr:8:23--8:42:While processing right hand side of main2 at lazybug.idr:8:1--10:1: Can't solve constraint between: Bool and Lazy Bool +at: +8 main2 = printLn $ or (map (\x => x) bools) + ^^^^^^^^^^^^^^^^^^^ + lazybug.idr:14:22--15:1:While processing right hand side of main4 at lazybug.idr:14:1--15:1: Can't solve constraint between: Bool and Lazy Bool +at: +14 main4 = printLn $ or bools + diff --git a/tests/idris2/reg023/expected b/tests/idris2/reg023/expected index e69a6fe18..4829eb954 100644 --- a/tests/idris2/reg023/expected +++ b/tests/idris2/reg023/expected @@ -4,3 +4,7 @@ Can't solve constraint between: S (countGreater thr xs) and countGreater thr xs +at: +23 eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i +24 eraseVar thr (x :: xs) (FS i) | False = FS <$> eraseVar thr xs i + diff --git a/tests/idris2/total007/expected b/tests/idris2/total007/expected index 9decfe9d3..40efcc362 100644 --- a/tests/idris2/total007/expected +++ b/tests/idris2/total007/expected @@ -1,5 +1,14 @@ 1/1: Building partial (partial.idr) -partial.idr:5:1--7:1:foo is not covering. Missing cases: +partial.idr:5:1--7:1:foo is not covering at: +5 total +6 foo : Maybe a -> a +7 foo (Just x) = x +Missing cases: foo Nothing partial.idr:13:1--15:1:qsortBad is not total: possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad +at: +13 total +14 qsortBad : Ord a => List a -> List a +15 qsortBad [] = [] + diff --git a/tests/idris2/total008/expected b/tests/idris2/total008/expected index aef8253a9..1494c8e50 100644 --- a/tests/idris2/total008/expected +++ b/tests/idris2/total008/expected @@ -1,3 +1,6 @@ 1/1: Building partial (partial.idr) -partial.idr:11:1--13:1:foo is not covering. Missing cases: +partial.idr:11:1--13:1:foo is not covering at: +11 Foo (Maybe Int) where +12 foo Nothing = () +Missing cases: foo (Just _) diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index a32115a32..e40156698 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -6,12 +6,20 @@ Mismatch between: ?_ -> IO () and IO ?b +at: +1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" + ^^^^^^^^^^^^^ + If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b Mismatch between: ?_ -> IO () and IO ?b +at: +1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" + ^^^^^^^^^^^^^^^^^^^^^^^^ + If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: @@ -20,6 +28,10 @@ Mismatch between: ?_ -> IO () and IO ?b +at: +1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" + ^^^^^^^^^^^^^^^^^^^^^^^^ + If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: If Prelude.>>=: When unifying ?_ -> IO () and IO ?b @@ -27,17 +39,31 @@ Mismatch between: ?_ -> IO () and IO ?b +at: +1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" + ^^^^^^^^^^^^^ + If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b Mismatch between: ?_ -> IO () and IO ?b +at: +1 do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" + ^^^^^^^^^^^^^^^^^^^^^^^^ -Main> (interactive):1:57--1:62:Can't find an implementation for Num () -Main> (interactive):1:4--1:6:Ambiguous elaboration. Possible correct results: + +Main> (interactive):1:57--1:62:Can't find an implementation for Num () at: +1 with Prelude.(>>=) do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo" + ^^^^^ + +Main> (interactive):1:4--1:6:Ambiguous elaboration at: +1 :t [] + ^^ +Possible correct results: [] [] [] @@ -48,6 +74,10 @@ Mismatch between: Vect 0 ?elem and List ?a +at: +1 :t with [Vect.Nil, Prelude.(::)] [1,2,3] + ^^^^^^^ + Main> the (Maybe Integer) (pure 4) : Maybe Integer Main> Parse error: Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input]) Main> Bye for now! diff --git a/tests/typedd-book/chapter10/expected b/tests/typedd-book/chapter10/expected index aa4798f1e..0c45e7781 100644 --- a/tests/typedd-book/chapter10/expected +++ b/tests/typedd-book/chapter10/expected @@ -1,6 +1,9 @@ 1/1: Building DLFail (DLFail.idr) DLFail.idr:3:20--3:29:While processing left hand side of describe_list_end at DLFail.idr:3:1--4:1: -Can't match on ?xs ++ [?x] (Not a constructor application or primitive) +Can't match on ?xs ++ [?x] (Not a constructor application or primitive) at +3 describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs + ^^^^^^^^^ + 1/13: Building DataStore (DataStore.idr) 2/13: Building DescribeList (DescribeList.idr) 3/13: Building DescribeList2 (DescribeList2.idr)