print location of implicit name shadowing with the warning. (#1968)

* print location of implicit name shadowing with the warning.

* move location output to bottom of warning.

src/Idris/Error.idr

@@ -166,14 +166,18 @@ pwarning (UnreachableClause fc env tm)
     = pure $ errorDesc (reflow "Unreachable clause:"
         <++> code !(pshow env tm))
         <+> line <+> !(ploc fc)
-pwarning (ShadowingGlobalDefs _ ns)
+pwarning (ShadowingGlobalDefs fc ns)
     = pure $ vcat
     $ reflow "We are about to implicitly bind the following lowercase names."
    :: reflow "You may be unintentionally shadowing the associated global definitions:"
-   :: map (\ (n, ns) => indent 2 $ hsep $ pretty n
-                            :: reflow "is shadowing"
-                            :: punctuate comma (map pretty (forget ns)))
-          (forget ns)
+   :: map pshadowing (forget ns)
+   `snoc` !(ploc fc)
+  where
+    pshadowing : (String, List1 Name) -> Doc IdrisAnn
+    pshadowing (n, ns) = indent 2 $ hsep $
+                           pretty n
+                        :: reflow "is shadowing"
+                        :: punctuate comma (map pretty (forget ns))
 
 pwarning (Deprecated s)
     = pure $ pretty "Deprecation warning:" <++> pretty s

tests/idris2/basic049/expected

@@ -2,44 +2,153 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R1.R1.a
+
+Fld:66:11--66:20
+ 62 | 
+ 63 |   public export
+ 64 |   record R2 where
+ 65 |     constructor MkR
+ 66 |     {auto field : a}
+                ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:74:1--79:38
+ 74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
+ 75 |   constructor MkIface
+ 76 |                                              -- constraints
+ 77 |   data MyData : a -> Type                    -- and a data declaration.
+ 78 |   someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
+ 79 |   giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:74:1--79:38
+ 74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
+ 75 |   constructor MkIface
+ 76 |                                              -- constraints
+ 77 |   data MyData : a -> Type                    -- and a data declaration.
+ 78 |   someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
+ 79 |   giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:83:1--84:37
+ 83 | data MyDataImpl : a -> Type where            -- implementation of MyData
+ 84 |   MkMyData : (x : a) -> MyDataImpl x
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:84:3--84:11
+ 80 |                                              -- constructor)
+ 81 | 
+ 82 | 
+ 83 | data MyDataImpl : a -> Type where            -- implementation of MyData
+ 84 |   MkMyData : (x : a) -> MyDataImpl x
+        ^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:110:1--110:11
+ 106 | Show' String where
+ 107 |    show' = id
+ 108 | 
+ 109 | %hint
+ 110 | showMaybe' : Show' a => Show' (Maybe a)
+       ^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
   b is shadowing Main.Other.b
+
+Fld:139:3--139:10
+ 135 | setName : String -> OrdinaryDog -> OrdinaryDog
+ 136 | setName name' = {name := name'}
+ 137 | 
+ 138 | data Three : Type -> Type -> Type -> Type where
+ 139 |   MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
+         ^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
   b is shadowing Main.Other.b
+
+Fld:141:1--141:10
+ 137 | 
+ 138 | data Three : Type -> Type -> Type -> Type where
+ 139 |   MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
+ 140 | 
+ 141 | mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
+       ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:217:15--217:21
+ 213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
+ 214 | dontCare2 {} = plusCommutative {}
+ 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+ 216 | 
+ 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
+                     ^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:217:24--217:48
+ 213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
+ 214 | dontCare2 {} = plusCommutative {}
+ 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+ 216 | 
+ 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
+                              ^^^^^^^^^^^^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:219:1--219:7
+ 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+ 216 | 
+ 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
+ 218 | 
+ 219 | isNode : Tree a -> Bool
+       ^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:223:1--224:24
+ 223 | data IsNode : Tree a -> Type where
+ 224 |   Is : IsNode (Node {})
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
+
+Fld:226:1--226:10
+ 222 | 
+ 223 | data IsNode : Tree a -> Type where
+ 224 |   Is : IsNode (Node {})
+ 225 | 
+ 226 | decIsNode : (x : Tree a) -> Dec (IsNode x)
+       ^^^^^^^^^
+
 Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
     Main.R2.MkR
     Main.R1.MkR Type

tests/idris2/coverage015/expected

@@ -40,12 +40,39 @@ Missing cases:
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   f is shadowing Main.f
+
+Issue1366:30:3--30:4
+ 26 |   uninhabited (Z _) impossible
+ 27 |   uninhabited (S _) impossible
+ 28 | 
+ 29 | data Funny : (a : Type) -> (f : Type -> Type) -> Type where
+ 30 |   A : List a -> f a -> Funny a f
+        ^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   f is shadowing Main.f
+
+Issue1366:31:3--31:4
+ 27 |   uninhabited (S _) impossible
+ 28 | 
+ 29 | data Funny : (a : Type) -> (f : Type -> Type) -> Type where
+ 30 |   A : List a -> f a -> Funny a f
+ 31 |   B : Funny a f
+        ^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   f is shadowing Main.f
+
+Issue1366:33:1--33:7
+ 29 | data Funny : (a : Type) -> (f : Type -> Type) -> Type where
+ 30 |   A : List a -> f a -> Funny a f
+ 31 |   B : Funny a f
+ 32 | 
+ 33 | decode : NS [[List a, f a], []] -> Funny a f
+      ^^^^^^
+
 Error: decode is not covering.
 
 Issue1366:33:1--33:45

tests/idris2/interface008/expected

@@ -2,6 +2,15 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   card is shadowing Main.card
+
+Deps:15:3--15:8
+ 11 |   to = id
+ 12 | 
+ 13 | interface BadFinite t where
+ 14 |   badcard   : Nat
+ 15 |   badto     : t -> Fin card
+        ^^^^^
+
 Error: While processing right hand side of badcard. k is not accessible in this context.
 
 Deps:18:13--18:14

tests/idris2/real001/expected

@@ -3,4 +3,13 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   any is shadowing Prelude.Interfaces.any
+
+Channel:63:6--63:11
+ 59 | AsServer proto = ServerK proto (\res => Close)
+ 60 | 
+ 61 | public export
+ 62 | data QueueEntry : Type where
+ 63 |      Entry : (1 val : any) -> QueueEntry
+           ^^^^^
+
 3/3: Building TestProto (TestProto.idr)

tests/idris2/real002/expected

@@ -2,9 +2,27 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   any is shadowing Prelude.Interfaces.any
+
+Control.App:143:1--143:12
+ 139 |     = \k => MkApp1 (\w => let MkApp1ResW x' w' = fn w
+ 140 |                               MkApp1 res = k x' in
+ 141 |                               res w')
+ 142 | 
+ 143 | absurdWith1 : (1 w : b) -> OneOf e NoThrow -> any
+       ^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   any is shadowing Prelude.Interfaces.any
+
+Control.App:146:1--146:12
+ 142 | 
+ 143 | absurdWith1 : (1 w : b) -> OneOf e NoThrow -> any
+ 144 | absurdWith1 w (First p) impossible
+ 145 | 
+ 146 | absurdWith2 : (1 x : a) -> (1 w : b) -> OneOf e NoThrow -> any
+       ^^^^^^^^^^^
+
 2/3: Building Control.App.Console (Control/App/Console.idr)
 3/3: Building Store (Store.idr)
 3/3: Building StoreL (StoreL.idr)

tests/idris2/reflection006/expected

@@ -5,9 +5,27 @@ LOG 0: Right: ((Prelude.Types.plus y) x)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   any is shadowing Prelude.Interfaces.any
+
+refleq:5:1--5:15
+ 1 | import Language.Reflection
+ 2 | 
+ 3 | %language ElabReflection
+ 4 | 
+ 5 | solveReflected : TTImp -> Elab any
+     ^^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   any is shadowing Prelude.Interfaces.any
+
+refleq:15:1--15:6
+ 11 |     = do logTerm "" 0 "Goal" g
+ 12 |          fail "I don't know how to prove this"
+ 13 | 
+ 14 | %macro
+ 15 | prove : Elab any
+      ^^^^^
+
 Error: While processing right hand side of commutes. Error during reflection: Not done
 
 refleq:24:16--24:21

tests/idris2/warning001/expected

@@ -2,21 +2,62 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   idF is shadowing Main.idF
+
+Issue539:10:1--10:7
+ 06 | 
+ 07 | leftIdPoint : (f : a -> b) -> (x : a) -> idF (f x) = f x
+ 08 | leftIdPoint f x = Refl
+ 09 | 
+ 10 | leftId : (f : a -> b) -> (idF . f = f)
+      ^^^^^^
+
 1/1: Building Issue621 (Issue621.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a1 is shadowing Main.a1
   a2 is shadowing Main.a2
+
+Issue621:8:1--8:7
+ 4 | 
+ 5 | a2 : Char
+ 6 | a2 = 'a'
+ 7 | 
+ 8 | whyNot : a1 = a2
+     ^^^^^^
+
 1/1: Building Issue1401 (Issue1401.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   fst is shadowing Builtin.fst, Builtin.DPair.DPair.fst
   dup is shadowing Prelude.Basics.dup
+
+Issue1401:1:1--1:7
+ 1 | fstDup: (xs : List a) -> map fst (map dup xs) === xs
+     ^^^^^^
+
 1/1: Building PR1407 (PR1407.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   f is shadowing Main.Hoo.f
+
+PR1407:7:3--7:10
+ 3 |   f : Either a b -> Either b a
+ 4 |   f (Left a) = Right a
+ 5 |   f (Right b) = Left b
+ 6 | 
+ 7 |   natural : (xs : Either a b) -> ((f . f) . map g) xs === (map g . (f . f)) xs
+       ^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   g is shadowing Main.g
+
+PR1407:15:3--15:4
+ 11 | 
+ 12 |   g : h === h
+ 13 |   g = Refl
+ 14 | 
+ 15 |   h : g === g
+        ^
+
 1/1: Building Holes (Holes.idr)

tests/typedd-book/chapter03/expected

@@ -3,19 +3,60 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+Matrix:3:1--3:14
+ 1 | import Data.Vect
+ 2 | 
+ 3 | createEmpties : {n : _} -> Vect n (Vect 0 elem)
+     ^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+Matrix:7:1--7:16
+ 3 | createEmpties : {n : _} -> Vect n (Vect 0 elem)
+ 4 | createEmpties {n = Z} = []
+ 5 | createEmpties {n = (S k)} = [] :: createEmpties
+ 6 | 
+ 7 | transposeHelper : (x : Vect n elem) -> (xs_trans : Vect n (Vect k elem)) -> Vect n (Vect (S k) elem)
+     ^^^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+Matrix:11:1--11:13
+ 07 | transposeHelper : (x : Vect n elem) -> (xs_trans : Vect n (Vect k elem)) -> Vect n (Vect (S k) elem)
+ 08 | transposeHelper [] [] = []
+ 09 | transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
+ 10 | 
+ 11 | transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
+      ^^^^^^^^^^^^
+
 3/8: Building VecSort (VecSort.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+VecSort:3:1--3:7
+ 1 | import Data.Vect
+ 2 | 
+ 3 | insert : Ord elem => (x : elem) -> (xsSorted : Vect k elem) -> Vect (S k) elem
+     ^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+VecSort:9:1--9:8
+ 5 | insert x (y :: xs) = case x < y of
+ 6 |                           False => y :: insert x xs
+ 7 |                           True => x :: y :: xs
+ 8 | 
+ 9 | insSort : Ord elem => Vect n elem -> Vect n elem
+     ^^^^^^^
+
 4/8: Building Vectors (Vectors.idr)
 5/8: Building WordLength (WordLength.idr)
 6/8: Building WordLength_vec (WordLength_vec.idr)

tests/typedd-book/chapter04/expected

@@ -2,12 +2,34 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+BSTree:2:6--2:11
+ 1 | data BSTree : Type -> Type where
+ 2 |      Empty : Ord elem => BSTree elem
+          ^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+BSTree:3:6--3:10
+ 1 | data BSTree : Type -> Type where
+ 2 |      Empty : Ord elem => BSTree elem
+ 3 |      Node : Ord elem => (left : BSTree elem) -> (val : elem) ->
+          ^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+BSTree:6:1--6:7
+ 2 |      Empty : Ord elem => BSTree elem
+ 3 |      Node : Ord elem => (left : BSTree elem) -> (val : elem) ->
+ 4 |                         (right : BSTree elem) -> BSTree elem
+ 5 | 
+ 6 | insert : elem -> BSTree elem -> BSTree elem
+     ^^^^^^
+
  2/12: Building DataStore (DataStore.idr)
  3/12: Building Direction (Direction.idr)
  4/12: Building Generic (Generic.idr)
@@ -18,16 +40,45 @@ You may be unintentionally shadowing the associated global definitions:
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:1:18--1:23
+ 1 | data Tree elem = Empty
+                      ^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:2:18--2:51
+ 1 | data Tree elem = Empty
+ 2 |                | Node (Tree elem) elem (Tree elem)
+                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:6:1--6:7
+ 2 |                | Node (Tree elem) elem (Tree elem)
+ 3 | 
+ 4 | %name Tree tree, tree1
+ 5 | 
+ 6 | insert : Ord elem => elem -> Tree elem -> Tree elem
+     ^^^^^^
+
  9/12: Building TryIndex (TryIndex.idr)
 10/12: Building Vect (Vect.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Vect:7:1--7:7
+ 3 |      (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
+ 4 | 
+ 5 | %name Vect xs, ys, zs
+ 6 | 
+ 7 | append : Vect n elem -> Vect m elem -> Vect (n + m) elem
+     ^^^^^^
+
 11/12: Building Vehicle (Vehicle.idr)
 12/12: Building All (All.idr)

tests/typedd-book/chapter06/expected

@@ -3,34 +3,124 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:26:5--26:14
+ 22 | 
+ 23 | addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
+ 24 | addToStore (MkData schema size store) newitem = MkData schema _ (addToData store)
+ 25 |   where
+ 26 |     addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
+          ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:36:6--36:15
+ 32 |                               Z => Just (MkData schema _ [])
+ 33 |                               S k => Nothing
+ 34 | 
+ 35 | data Command : Schema -> Type where
+ 36 |      SetSchema : Schema -> Command schema
+           ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:37:6--37:9
+ 33 |                               S k => Nothing
+ 34 | 
+ 35 | data Command : Schema -> Type where
+ 36 |      SetSchema : Schema -> Command schema
+ 37 |      Add : SchemaType schema -> Command schema
+           ^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:38:6--38:9
+ 34 | 
+ 35 | data Command : Schema -> Type where
+ 36 |      SetSchema : Schema -> Command schema
+ 37 |      Add : SchemaType schema -> Command schema
+ 38 |      Get : Integer -> Command schema
+           ^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:39:6--39:10
+ 35 | data Command : Schema -> Type where
+ 36 |      SetSchema : Schema -> Command schema
+ 37 |      Add : SchemaType schema -> Command schema
+ 38 |      Get : Integer -> Command schema
+ 39 |      Quit : Command schema
+           ^^^^
+
 3/8: Building DataStoreHoles (DataStoreHoles.idr)
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStoreHoles:25:5--25:14
+ 21 | 
+ 22 | addToStore : (d : DataStore) -> SchemaType (schema d) -> DataStore
+ 23 | addToStore (MkData schema size store) newitem = MkData schema _ (addToData store)
+ 24 |   where
+ 25 |     addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
+          ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStoreHoles:30:6--30:9
+ 26 |     addToData [] = [newitem]
+ 27 |     addToData (x :: xs) = x :: addToData xs
+ 28 | 
+ 29 | data Command : Schema -> Type where
+ 30 |      Add : SchemaType schema -> Command schema
+           ^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStoreHoles:31:6--31:9
+ 27 |     addToData (x :: xs) = x :: addToData xs
+ 28 | 
+ 29 | data Command : Schema -> Type where
+ 30 |      Add : SchemaType schema -> Command schema
+ 31 |      Get : Integer -> Command schema
+           ^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStoreHoles:32:6--32:10
+ 28 | 
+ 29 | data Command : Schema -> Type where
+ 30 |      Add : SchemaType schema -> Command schema
+ 31 |      Get : Integer -> Command schema
+ 32 |      Quit : Command schema
+           ^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStoreHoles:34:1--34:13
+ 30 |      Add : SchemaType schema -> Command schema
+ 31 |      Get : Integer -> Command schema
+ 32 |      Quit : Command schema
+ 33 | 
+ 34 | parseCommand : String -> String -> Maybe (Command schema)
+      ^^^^^^^^^^^^
+
 4/8: Building Maybe (Maybe.idr)
 5/8: Building Printf (Printf.idr)
 6/8: Building TypeFuns (TypeFuns.idr)

tests/typedd-book/chapter07/expected

@@ -6,13 +6,40 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:1:18--1:23
+ 1 | data Tree elem = Empty
+                      ^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:2:18--2:51
+ 1 | data Tree elem = Empty
+ 2 |                | Node (Tree elem) elem (Tree elem)
+                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:4:1--8:21
+ 4 | Eq elem => Eq (Tree elem) where
+ 5 |     (==) Empty Empty = True
+ 6 |     (==) (Node left e right) (Node left' e' right')
+ 7 |           = left == left' && e == e' && right == right'
+ 8 |     (==) _ _ = False
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+Tree:4:1--8:21
+ 4 | Eq elem => Eq (Tree elem) where
+ 5 |     (==) Empty Empty = True
+ 6 |     (==) (Node left e right) (Node left' e' right')
+ 7 |           = left == left' && e == e' && right == right'
+ 8 |     (==) _ _ = False
+
 6/6: Building All (All.idr)

tests/typedd-book/chapter08/expected

@@ -2,12 +2,38 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+AppendVec:4:1--4:11
+ 1 | import Data.Nat
+ 2 | import Data.Vect
+ 3 | 
+ 4 | append_nil : Vect m elem -> Vect (plus m 0) elem
+     ^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+AppendVec:7:1--7:10
+ 3 | 
+ 4 | append_nil : Vect m elem -> Vect (plus m 0) elem
+ 5 | append_nil {m} xs = rewrite plusZeroRightNeutral m in xs
+ 6 | 
+ 7 | append_xs : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
+     ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Data.Vect.elem, Prelude.Types.elem
+
+AppendVec:10:1--10:7
+ 06 | 
+ 07 | append_xs : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
+ 08 | append_xs {m} {k} xs = rewrite sym (plusSuccRightSucc m k) in xs
+ 09 | 
+ 10 | append : Vect n elem -> Vect m elem -> Vect (m + n) elem
+      ^^^^^^
+
  2/10: Building CheckEqDec (CheckEqDec.idr)
  3/10: Building CheckEqMaybe (CheckEqMaybe.idr)
  4/10: Building EqNat (EqNat.idr)

tests/typedd-book/chapter11/expected

@@ -8,6 +8,12 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   elem is shadowing Prelude.Types.elem
+
+InfList:2:6--2:10
+ 1 | data InfList : Type -> Type where
+ 2 |      (::) : (value : elem) -> Inf (InfList elem) -> InfList elem
+          ^^^^
+
  8/12: Building Label (Label.idr)
  9/12: Building RunIO (RunIO.idr)
 10/12: Building Streams (Streams.idr)

tests/typedd-book/chapter12/expected

@@ -3,15 +3,51 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:23:6--23:15
+ 19 | setSchema : DataStore 0 -> Schema -> DataStore 0
+ 20 | setSchema (MkData schema []) schema' = MkData schema' []
+ 21 | 
+ 22 | data Command : Schema -> Type where
+ 23 |      SetSchema : Schema -> Command schema
+           ^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:24:6--24:9
+ 20 | setSchema (MkData schema []) schema' = MkData schema' []
+ 21 | 
+ 22 | data Command : Schema -> Type where
+ 23 |      SetSchema : Schema -> Command schema
+ 24 |      Add : SchemaType schema -> Command schema
+           ^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:25:6--25:9
+ 21 | 
+ 22 | data Command : Schema -> Type where
+ 23 |      SetSchema : Schema -> Command schema
+ 24 |      Add : SchemaType schema -> Command schema
+ 25 |      Get : Integer -> Command schema
+           ^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   schema is shadowing Main.DataStore.schema
+
+DataStore:26:6--26:10
+ 22 | data Command : Schema -> Type where
+ 23 |      SetSchema : Schema -> Command schema
+ 24 |      Add : SchemaType schema -> Command schema
+ 25 |      Get : Integer -> Command schema
+ 26 |      Quit : Command schema
+           ^^^^
+
  3/10: Building Record (Record.idr)
  4/10: Building State (State.idr)
  5/10: Building StateMonad (StateMonad.idr)

tests/typedd-book/chapter14/expected

@@ -4,4 +4,13 @@
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   letters is shadowing Main.letters
+
+Hangman:28:3--28:8
+ 24 | 
+ 25 |   Won :  GameCmd () (Running (S guesses) 0) (const NotRunning)
+ 26 |   Lost : GameCmd () (Running 0 (S guesses)) (const NotRunning)
+ 27 | 
+ 28 |   Guess : (c : Char) ->
+        ^^^^^
+
 4/4: Building All (All.idr)