Fixed tests

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"
+	    ^^^^
+

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!

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!

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
+	                            ^
+

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
+

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
+

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	
+

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!

tests/idris2/basic030/expected

@@ -5,3 +5,7 @@ Mismatch between:
 	(1 _ : Nat) -> MyN
 and
 	MyN
+at:
+4	foo x y = case MkN x of
+	               ^^^^^^
+

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"
+	                ^^^^
+

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
+	               ^^
+

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
+

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 _, _)

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

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:27:1--29:1:badeq x y p is not a valid impossible case at:
-eq.idr:30:1--31:1:badeqL xs ys p is not a valid impossible case
+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
+

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)

tests/idris2/error001/expected

@@ -5,3 +5,6 @@ Mismatch between:
 	a
 and
 	Vect ?k ?a
+at:
+6	wrong x xs = x :: x
+

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
+

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
+
 

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

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
+

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	
+

tests/idris2/error007/expected

@@ -4,3 +4,6 @@ Can't solve constraint between:
 	?_ x
 and
 	FS x
+at:
+4	fsprf p = cong _ p
+

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
+Undefined name Nat at:
-Test.idr:6:1--8:1:No type declaration for Test.thing
+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!

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
+

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
+	                        ^^^^^^^^^^^^^^^^^^^^^^^^^
+

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
+

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

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!

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!

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
+

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
+

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

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

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	
+

tests/idris2/reflection005/expected

@@ -5,5 +5,8 @@ Mismatch between:
 	()
 and
 	a
+at:
+13	bad = %runElab mkDecls `(94)
+
 Main> 9400
 Main> Bye for now!

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
+

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 ~=~
+Undefined name ~=~ at:
-Holes.idr:8:1--10:1:No type declaration for Main.Weird
+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
+Undefined name Bool at:
-Holes.idr:11:1--12:1:No type declaration for Main.f
+10	f : Bool -> Nat
-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
+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!

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
+

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]}))]
+	                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+

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
+Undefined name n at:
-UnboundImplicits.idr:9:24--9:26:Undefined name n
+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
+	                             ^
+

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
+

tests/idris2/reg017/expected

@@ -5,3 +5,7 @@ Mismatch between:
 	(0 _ : ?a) -> ?b
 and
 	?a -> ?b
+at:
+2	badmap = map (\0 x => 2)
+	              ^^^^^^^^^
+

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
+

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
+

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 [] = []
+

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 _)

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!

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)