Improving error messages (#786)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>

src/Core/FC.idr

@@ -79,6 +79,17 @@ export
 toplevelFC : FC
 toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
 
+------------------------------------------------------------------------
+-- Basic operations
+export
+mergeFC : FC -> FC -> Maybe FC
+mergeFC (MkFC fname1 start1 end1) (MkFC fname2 start2 end2) = 
+  if fname1 == fname2
+  then Just $ MkFC fname1 (min start1 start2) (max end1 end2)
+  else Nothing
+mergeFC _ _ = Nothing
+
+
 %name FC fc
 
 ------------------------------------------------------------------------

src/Idris/Parser.idr

@@ -1390,13 +1390,14 @@ topDecl fname indents
 -- collectDefs : List PDecl -> List PDecl
 collectDefs [] = []
 collectDefs (PDef annot cs :: ds)
-    = let (cs', rest) = spanBy isClause ds in
+    = let (csWithFC, rest) = spanBy isPDef ds
-          PDef annot (cs ++ concat cs') :: assert_total (collectDefs rest)
+          cs' = cs ++ concat (map snd csWithFC)
-  where
+          annot' = foldr 
-    isClause : PDecl -> Maybe (List PClause)
+                   (\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
-    isClause (PDef annot cs)
+                   annot 
-        = Just cs
+                   (map fst csWithFC)
-    isClause _ = Nothing
+      in
+          PDef annot' cs' :: assert_total (collectDefs rest)
 collectDefs (PNamespace annot ns nds :: ds)
     = PNamespace annot ns (collectDefs nds) :: collectDefs ds
 collectDefs (PMutual annot nds :: ds)

src/Idris/Syntax.idr

@@ -334,6 +334,12 @@ mutual
   getPDeclLoc (PRunElabDecl fc _) = fc
   getPDeclLoc (PDirective fc _) = fc
 
+  export
+  isPDef : PDecl -> Maybe (FC, List PClause)
+  isPDef (PDef annot cs) = Just (annot, cs)
+  isPDef _ = Nothing
+
+
 definedInData : PDataDecl -> List Name
 definedInData (MkPData _ n _ _ cons) = n :: map getName cons
   where

src/Parser/Rule/Common.idr

@@ -16,20 +16,20 @@ EmptyRule token ty = Grammar token False ty
 export
 location : {token : _} -> EmptyRule token (Int, Int)
 location
-    = do tok <- bounds peek
+    = do tok <- removeIrrelevance <$> bounds peek
-         pure (tok.startLine, tok.startCol)
+         pure $ start tok
 
 export
 endLocation : {token : _} -> EmptyRule token (Int, Int)
 endLocation
-    = do tok <- bounds peek
+    = do tok <- removeIrrelevance <$> bounds peek
-         pure (tok.endLine, tok.endCol)
+         pure $ end tok
 
 export
 position : {token : _} -> EmptyRule token ((Int, Int), (Int, Int))
 position
-    = do tok <- bounds peek
+    = do tok <- removeIrrelevance <$> bounds peek
-         pure ((tok.startLine, tok.startCol), (tok.endLine, tok.endCol))
+         pure (start tok, end tok)
 
 
 export

src/Text/Bounded.idr

@@ -46,6 +46,10 @@ export
 irrelevantBounds : ty -> WithBounds ty
 irrelevantBounds x = MkBounded x True (-1) (-1) (-1) (-1)
 
+export
+removeIrrelevance : WithBounds ty -> WithBounds ty
+removeIrrelevance (MkBounded val ir sl sc el ec) = MkBounded val True sl sc el ec
+
 export
 mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'
 mergeBounds (MkBounded _ True _ _ _ _) (MkBounded val True _ _ _ _) = irrelevantBounds val

src/Text/Literate.idr

@@ -64,11 +64,11 @@ rawTokens delims ls =
 ||| Merge the tokens into a single source file.
 reduce : List (WithBounds Token) -> List String -> String
 reduce [] acc = fastAppend (reverse acc)
-reduce (MkBounded (Any x) _ _ _ _ _ :: rest) acc = reduce rest (blank_content::acc)
+reduce (MkBounded (Any x) _ _ _ _ _ :: rest) acc = 
-  where
+  -- newline will always be tokenized as a single token
-    -- Preserve the original document's line count.
+  if x == "\n"
-    blank_content : String
+  then reduce rest ("\n"::acc)
-    blank_content = fastAppend (replicate (length (lines x)) "\n")
+  else reduce rest acc
 
 reduce (MkBounded (CodeLine m src) _ _ _ _ _ :: rest) acc =
     if m == trim src
@@ -83,7 +83,8 @@ reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc with (lines src) --
   reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: ys) with (snocList ys)
     reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
     reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
-        reduce rest ("\n" :: unlines srcs :: acc)
+        -- the "\n" counts for the open deliminator; the closing deliminator should always be followed by a (Any "\n"), so we don't add a newline
+        reduce rest (unlines srcs :: "\n" :: acc)
 
 -- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
 

src/Text/Parser/Core.idr

@@ -240,7 +240,7 @@ mutual
   doParse com (NextIs err f) [] = Failure com False "End of input" []
   doParse com (NextIs err f) (x :: xs)
         = if f x
-             then Res com x (x :: xs)
+             then Res com (removeIrrelevance x) (x :: xs)
              else Failure com False err (x :: xs)
   doParse com (Alt {c1} {c2} x y) xs
       = case doParse False x xs of

tests/Main.idr

@@ -84,7 +84,7 @@ idrisTests = MkTestPool []
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",
        "literate009", "literate010", "literate011", "literate012",
-       "literate013", "literate014",
+       "literate013", "literate014", "literate015", "literate016",
        -- Namespace blocks
        "namespace001",
        -- Parameters blocks

tests/chez/chez031/expected

@@ -2,32 +2,28 @@ Error: The given specifier was not accepted by any backend. Available backends:
   chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
  29 | %foreign "scheme,racket:+"
  30 | plusRacketFail : Int -> Int -> Int
- 31 | 
- 32 | -- We don't actually do any printing this is just to use the specifiers so the
- 33 | -- failures are exposed.
- 34 | main : IO ()
 
 Error: The given specifier was not accepted by any backend. Available backends:
   chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
 
 Main> Loaded file Specifiers.idr
 Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
   chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
 
 Specifiers> [exec] Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
   chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
 
 [exec] Specifiers> 
 Bye for now!

tests/ideMode/ideMode001/expected

@@ -8,7 +8,7 @@
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--62:33 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -8,7 +8,7 @@
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--62:33 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/idris2/basic044/expected

@@ -98,7 +98,7 @@ Term> Bye for now!
 LOG declare.type:1: Processing Vec.Vec
 LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1])
 LOG declare.type:1: Processing Vec.Nil
-LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:19:1--24:7)
+LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:19:1--22:32)
 LOG declare.type:1: Processing Vec.::
 LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
  { Data.Fin.FZ {e:N} => [0] {arg:N}[3]

tests/idris2/coverage010/expected

@@ -1,8 +1,9 @@
 1/1: Building casetot (casetot.idr)
 Error: main is not covering.
 
-casetot.idr:12:1--13:5
+casetot.idr:12:1--12:13
+    |
  12 | main : IO ()
- 13 | main = do
+    | ^^^^^^^^^^^^
 
 Calls non covering function Main.case block in case block in main

tests/idris2/error004/expected

@@ -16,8 +16,8 @@ Error2.idr:13:38--13:45
     |                                      ^^^^^^^
 
 Possible correct results:
-    Show implementation at Error2.idr:11:1--15:6
+    Show implementation at Error2.idr:11:1--13:45
-    Show implementation at Error2.idr:7:1--11:5
+    Show implementation at Error2.idr:7:1--9:45
 Error: While processing right hand side of wrong. Multiple solutions found in search of:
     Show (Vect 1 Integer)
 
@@ -27,5 +27,5 @@ Error2.idr:16:9--16:34
     |         ^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Possible correct results:
-    Show implementation at Error2.idr:11:1--15:6
+    Show implementation at Error2.idr:11:1--13:45
-    Show implementation at Error2.idr:7:1--11:5
+    Show implementation at Error2.idr:7:1--9:45

tests/idris2/error013/expected

@@ -1,21 +1,22 @@
 1/1: Building Issue361 (Issue361.idr)
-Error: main is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--7:5 -> Main.== -> Main./= -> Main.==
+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--8:5
+Issue361.idr:7:1--7:13
+   |
  7 | main : IO ()
- 8 | main = printLn $ T == T
+   | ^^^^^^^^^^^^
 
 Error: /= is not total, possibly not terminating due to recursive path Main./= -> Main.== -> Main./= -> Main.==
 
-Issue361.idr:5:1--7:5
+Issue361.idr:5:1--5:11
+   |
  5 | Eq S where
- 6 | 
+   | ^^^^^^^^^^
- 7 | main : IO ()
 
 Error: == is not total, possibly not terminating due to call to Main./=
 
-Issue361.idr:5:1--7:5
+Issue361.idr:5:1--5:11
+   |
  5 | Eq S where
- 6 | 
+   | ^^^^^^^^^^
- 7 | main : IO ()
 

tests/idris2/interface016/expected

@@ -9,4 +9,4 @@ TwoNum.idr:4:7--4:8
 
 Possible correct results:
     conArg (implicitly bound at TwoNum.idr:4:3--4:8)
-    conArg (implicitly bound at TwoNum.idr:2:1--5:1)
+    conArg (implicitly bound at TwoNum.idr:2:1--4:8)

tests/idris2/linear007/expected

@@ -1,10 +1,9 @@
 1/1: Building LCase (LCase.idr)
 Error: While processing right hand side of foo. There are 0 uses of linear name y. 
 
-LCase.idr:7:11--10:15
+LCase.idr:7:11--9:37
- 07 |     = let 1 test = the Nat $ case z of
+ 7 |     = let 1 test = the Nat $ case z of
- 08 |                         Z => Z
+ 8 |                         Z => Z
- 09 |                         (S k) => S z
+ 9 |                         (S k) => S z
- 10 |             in
 
 Suggestion: linearly bounded variables must be used exactly once.

tests/idris2/literate016/IEdit.org

@@ -0,0 +1,31 @@
+#+TITLE: Interactive Editing Working
+#+Date: 11/22/2020
+
+#+begin_src idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+#+end_src
+
+#+IDRIS: %name Vect xs, ys, zs
+
+#+begin_src idris
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append {n} xs ys = ?foo
+#+end_src
+
+#+begin_src idris
+vadd : Num a => Vect n a -> Vect n a -> Vect n a
+vadd [] ys = ?bar
+vadd (x :: xs) ys = ?baz
+#+end_src
+
+#+begin_src idris
+suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
+suc x y prf = ?quux
+#+end_src
+
+#+begin_src idris
+suc' : x = y -> S x = S y
+suc' {x} {y} prf = ?quuz
+#+end_src

tests/idris2/literate016/IEdit2.org

@@ -0,0 +1,31 @@
+#+TITLE: Interactive Editing Working
+
+#+begin_src idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+#+end_src
+
+#+IDRIS: %name Vect xs, ys, zs
+
+#+begin_src idris
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append {n = Z} [] ys = ?foo_1
+append {n = (S k)} (x :: xs) ys = ?foo_2
+#+end_src
+
+#+begin_src idris
+vadd : Num a => Vect n a -> Vect n a -> Vect n a
+vadd [] [] = ?bar_1
+vadd (x :: xs) (y :: ys) = ?baz_1
+#+end_src
+
+#+begin_src idris
+suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
+suc x x Refl = ?quux_1
+#+end_src
+
+#+begin_src idris
+suc' : x = y -> S x = S y
+suc' {x = y} {y = y} Refl = ?quuz_1
+#+end_src

tests/idris2/literate016/expected

@@ -0,0 +1,8 @@
+1/1: Building IEdit (IEdit.org)
+Main> append {n = 0} [] ys = ?foo_1
+append {n = (S k)} (x :: xs) ys = ?foo_2
+Main> vadd [] [] = ?bar_1
+Main> vadd (x :: xs) (y :: ys) = ?baz_1
+Main> suc x x Refl = ?quux_1
+Main> suc' {x = y} {y = y} Refl = ?quuz_1
+Main> Bye for now!

tests/idris2/literate016/input

@@ -0,0 +1,6 @@
+:cs 14 11 xs
+:cs 19 8 ys
+:cs 20 15 ys
+:cs 25 8 prf
+:cs 30 13 prf
+:q

tests/idris2/literate016/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner IEdit.org < input
+
+rm -rf build

tests/idris2/namespace001/expected

@@ -1,7 +1,7 @@
 1/1: Building Dup (Dup.idr)
 Error: Main.Test is already defined.
 
-Dup.idr:13:1--15:1
+Dup.idr:13:1--14:18
  13 | private
  14 | data Test = A | B
 

tests/idris2/reflection001/expected

@@ -23,7 +23,7 @@ quote.idr:37:1--37:21
 
 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, 12) (11, 32)) [IClaim (MkFC "quote.idr" (10, 12) (11, 15)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) 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)))))
+Main> ILocal (MkFC "quote.idr" (10, 12) (11, 29)) [IClaim (MkFC "quote.idr" (10, 12) (10, 28)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) 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)))))
-Main> ILocal (MkFC "quote.idr" (16, 12) (17, 32)) [IClaim (MkFC "quote.idr" (16, 12) (17, 15)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
+Main> ILocal (MkFC "quote.idr" (16, 12) (17, 29)) [IClaim (MkFC "quote.idr" (16, 12) (16, 28)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
 Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")]
 Main> Bye for now!

tests/idris2/reg013/expected

@@ -20,7 +20,7 @@ UnboundImplicits.idr:14:25--14:26
  14 | interface Foo (a : Vect n Nat) where
     |                         ^
 
-Error: While processing type of Functor implementation at UnboundImplicits.idr:17:1--18:1. Undefined name n. 
+Error: While processing type of Functor implementation at UnboundImplicits.idr:17:1--17:38. Undefined name n. 
 
 UnboundImplicits.idr:17:30--17:31
     |

tests/idris2/total007/expected

@@ -1,18 +1,16 @@
 1/1: Building partial (partial.idr)
 Error: foo is not covering.
 
-partial.idr:5:1--7:4
+partial.idr:5:1--6:19
  5 | total
  6 | foo : Maybe a -> a
- 7 | foo (Just x) = x
 
 Missing cases:
     foo Nothing
 
 Error: qsortBad is not total, possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad
 
-partial.idr:13:1--15:9
+partial.idr:13:1--14:37
  13 | total
  14 | qsortBad : Ord a => List a -> List a
- 15 | qsortBad [] = []
 

tests/idris2/total008/expected

@@ -1,7 +1,7 @@
 1/1: Building partial (partial.idr)
 Error: foo is not covering.
 
-partial.idr:11:1--13:1
+partial.idr:11:1--12:19
  11 | Foo (Maybe Int) where
  12 |   foo Nothing = ()