From 9c5bdf598380e455719af871746e0a4d2f118317 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 7 Aug 2024 16:35:27 -0700
Subject: [PATCH] switch to fc

---
 src/Lib/Check.idr       | 224 +++++++++++++++++++---------------------
 src/Lib/Parser.idr      |  66 ++++++------
 src/Lib/Parser/Impl.idr |  25 +++--
 src/Lib/ProcessDecl.idr |  36 +++----
 src/Lib/Syntax.idr      | 135 +++++++++++++-----------
 src/Lib/TT.idr          |  62 +++++------
 src/Lib/Types.idr       | 125 ++++++++++++----------
 7 files changed, 346 insertions(+), 327 deletions(-)

diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index cf680ad..8962eb9 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -21,19 +21,19 @@ data Pden = PR Nat Nat (List Nat)
 -- IORef for metas needs IO
 
 forceMeta : Val -> M Val
-forceMeta (VMeta ix sp) = case !(lookupMeta ix) of
-  (Unsolved pos k xs) => pure (VMeta ix sp)
+forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
+  (Unsolved pos k xs) => pure (VMeta fc ix sp)
   (Solved k t) => vappSpine t sp
 forceMeta x = pure x
 
 -- Lennart needed more forcing for recursive nat,
 forceType : Val -> M Val
-forceType (VRef nm def sp) =
+forceType (VRef fc nm def sp) =
     case lookup nm !(get) of
       (Just (MkEntry name type (Fn t))) => vappSpine !(eval [] CBN t) sp
-      _ => pure (VRef nm def sp)
-forceType (VMeta ix sp) = case !(lookupMeta ix) of
-  (Unsolved x k xs) => pure (VMeta ix sp)
+      _ => pure (VRef fc nm def sp)
+forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
+  (Unsolved x k xs) => pure (VMeta fc ix sp)
   (Solved k t) => vappSpine t sp >>= forceType
 forceType x = pure x
 
@@ -45,11 +45,11 @@ parameters (ctx: Context)
     where
       go : SnocList Val -> List Nat -> M (List Nat)
       go [<] acc = pure $ reverse acc
-      go (xs :< VVar k [<]) acc = do
+      go (xs :< VVar emptyFC k [<]) acc = do
         if elem k acc
-          then error [DS "non-linear pattern"]
+          then error emptyFC "non-linear pattern"
           else go xs (k :: acc)
-      go _ _ = error [DS "non-variable in pattern"]
+      go _ _ = error emptyFC "non-variable in pattern"
 
   -- we have to "lift" the renaming when we go under a lambda
   -- I think that essentially means our domain ix are one bigger, since we're looking at lvl
@@ -62,23 +62,23 @@ parameters (ctx: Context)
       goSpine ren lvl tm [<] = pure tm
       goSpine ren lvl tm (xs :< x) = do
         xtm <- go ren lvl x
-        goSpine ren lvl (App tm xtm) xs
+        goSpine ren lvl (App emptyFC tm xtm) xs
 
-      go ren lvl (VVar k sp) = case findIndex (== k) ren of
-        Nothing => error [DS "scope/skolem thinger"]
-        Just x => goSpine ren lvl (Bnd $ cast x) sp
-      go ren lvl (VRef nm def sp) = goSpine ren lvl (Ref nm def) sp
-      go ren lvl (VMeta ix sp) = if ix == meta
-        then error [DS "meta occurs check"]
-        else goSpine ren lvl (Meta ix) sp
-      go ren lvl (VLam n t) = pure (Lam n !(go (lvl :: ren) (S lvl) !(t $$ VVar lvl [<])))
-      go ren lvl (VPi n icit ty tm) = pure (Pi n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar lvl [<])))
-      go ren lvl VU = pure U
+      go ren lvl (VVar fc k sp) = case findIndex (== k) ren of
+        Nothing => error emptyFC "scope/skolem thinger"
+        Just x => goSpine ren lvl (Bnd fc $ cast x) sp
+      go ren lvl (VRef fc nm def sp) = goSpine ren lvl (Ref fc nm def) sp
+      go ren lvl (VMeta fc ix sp) = if ix == meta
+        then error emptyFC "meta occurs check"
+        else goSpine ren lvl (Meta fc ix) sp
+      go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar emptyFC lvl [<])))
+      go ren lvl (VPi fc n icit ty tm) = pure (Pi fc n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<])))
+      go ren lvl (VU fc) = pure (U fc)
 
   lams : Nat -> Tm -> Tm
   lams 0 tm = tm
   -- REVIEW can I get better names in here?
-  lams (S k) tm = Lam "arg_\{show k}" (lams k tm)
+  lams (S k) tm = Lam emptyFC "arg_\{show k}" (lams k tm)
 
 
   solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
@@ -94,10 +94,10 @@ parameters (ctx: Context)
   unify : (l : Nat) -> Val -> Val  -> M  ()
 
   unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M  ()
-  unifySpine l False _ _ = error [DS "unify failed at head"] -- unreachable now
+  unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now
   unifySpine l True [<] [<] = pure ()
   unifySpine l True (xs :< x) (ys :< y) = unify l x y >> unifySpine l True xs ys
-  unifySpine l True _ _ = error [DS "meta spine length mismatch"]
+  unifySpine l True _ _ = error emptyFC "meta spine length mismatch"
 
   unify l t u = do
     debug "Unify \{show ctx.lvl}"
@@ -106,32 +106,32 @@ parameters (ctx: Context)
     t' <- forceMeta t
     u' <- forceMeta u
     case (t',u') of
-      (VLam _ t,  VLam _ t') => unify (l + 1) !(t $$ VVar l [<]) !(t' $$ VVar l [<])
-      (t,         VLam _ t') => unify (l + 1) !(t `vapp` VVar l [<]) !(t' $$ VVar l [<])
-      (VLam _ t,  t'       ) => unify (l + 1) !(t $$ VVar l [<]) !(t' `vapp` VVar l [<])
-      (VPi _ _ a b, VPi _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar l [<]) !(b' $$ VVar l [<])
-      (VVar k sp,   VVar k' sp'  ) =>
+      (VLam _ _ t,  VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+      (t,         VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+      (VLam fc _ t,  t'       ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
+      (VPi fc _ _ a b, VPi fc' _ _ a' b') => unify l a a' >> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<])
+      (VVar fc k sp,   VVar fc' k' sp'  ) =>
         if k == k' then unifySpine l (k == k') sp sp'
-        else error [DS "vvar mismatch \{show k} \{show k'}"]
-      (VRef k def sp,   VRef k' def' sp'  ) =>
+        else error emptyFC "vvar mismatch \{show k} \{show k'}"
+      (VRef fc k def sp,   VRef fc' k' def' sp'  ) =>
         if k == k' then unifySpine l (k == k') sp sp'
         -- REVIEW - consider forcing?
-        else error [DS "vref mismatch \{show k} \{show k'}"]
-      (VMeta k sp,  VMeta k' sp' ) =>
+        else error emptyFC "vref mismatch \{show k} \{show k'}"
+      (VMeta fc k sp,  VMeta fc' k' sp' ) =>
         if k == k' then unifySpine l (k == k') sp sp'
-        else solve l k sp (VMeta k' sp')
-      (t,           VMeta i' sp') => solve l i' sp' t
-      (VMeta i sp, t'           ) => solve l i sp t'
-      (VU, VU) => pure ()
+        else solve l k sp (VMeta fc' k' sp')
+      (t,           VMeta fc' i' sp') => solve l i' sp' t
+      (VMeta fc i sp, t'           ) => solve l i sp t'
+      (VU _, VU _) => pure ()
       -- Lennart.newt cursed type references itself
       -- We _could_ look up the ref, eval against [] and vappSpine...
-      (t,         VRef k' def sp') => do
+      (t,         VRef fc' k' def sp') => do
         debug "expand \{show t} =?= %ref \{k'}"
         case lookup k' !(get) of
           Just (MkEntry name ty (Fn tm)) => unify l t !(vappSpine !(eval [] CBN tm) sp')
-          _ => error [DS "unify failed \{show t'} =?= \{show u'} [no Fn]\n  env is \{show ctx.env} \{show $ map fst ctx.types}" ]
+          _ => error emptyFC "unify failed \{show t'} =?= \{show u'} [no Fn]\n  env is \{show ctx.env} \{show $ map fst ctx.types}"
       -- REVIEW I'd like to quote this back, but we have l that aren't in the environment.
-      _ => error [DS "unify failed \{show t'} =?= \{show u'} \n  env is \{show ctx.env} \{show $ map fst ctx.types}" ]
+      _ => error emptyFC "unify failed \{show t'} =?= \{show u'} \n  env is \{show ctx.env} \{show $ map fst ctx.types}"
 
 unifyCatch : Context -> Val -> Val -> M ()
 unifyCatch ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do
@@ -144,20 +144,20 @@ unifyCatch ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do
 insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
   case !(forceMeta ty) of
-    VPi x Implicit a b => do
-      m <- freshMeta ctx
+    VPi fc x Implicit a b => do
+      m <- freshMeta ctx fc
       mv <- eval ctx.env CBN m
-      insert ctx (App tm m) !(b $$ mv)
+      insert ctx (App emptyFC tm m) !(b $$ mv)
     va => pure (tm, va)
 
 lookupName : Context -> Raw -> M (Maybe (Tm, Val))
-lookupName ctx (RVar nm) = go 0 ctx.types
+lookupName ctx (RVar fc nm) = go 0 ctx.types
   where
     go : Nat -> Vect n (String, Val)  -> M  (Maybe (Tm, Val))
     go i [] = case lookup nm !(get) of
-      Just (MkEntry name ty def) => pure $ Just (Ref nm def, !(eval [] CBN ty))
+      Just (MkEntry name ty def) => pure $ Just (Ref fc nm def, !(eval [] CBN ty))
       Nothing => pure Nothing
-    go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd i, ty)
+    go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd fc i, ty)
       else go (i + 1) xs
 lookupName ctx _ = pure Nothing
 
@@ -176,7 +176,7 @@ checkAlt scty ctx ty (MkAlt ptm body) = do
   (con, args) <- getArgs ptm []
   debug "ALT con \{con} args \{show args}"
   let Just (MkEntry _ dcty (DCon arity _)) = lookup con !(get)
-    | _ => error [DS "expected datacon, got \{con}"]
+    | _ => error emptyFC "expected datacon, got \{con}"
 
   -- arity is wrong, but we actually need the type anyway
   -- in fact arity is for later (eval?) and we need to do implicits first
@@ -203,94 +203,89 @@ checkAlt scty ctx ty (MkAlt ptm body) = do
   where
 
     go : Val -> Raw -> Context -> M Tm
-    go ctype (RSrcPos x tm) ctx = go ctype tm ctx
     -- FIXME icit
-    go (VPi str Explicit a b) (RApp t (RSrcPos _ (RVar nm)) Explicit) ctx = do
+    go (VPi fc str Explicit a b) (RApp _ t (RVar _ nm) Explicit) ctx = do
       debug "*** \{nm} : \{show a}"
-      let var = VVar (length ctx.env) [<]
+      let var = VVar emptyFC (length ctx.env) [<]
       let ctx' = extend ctx nm a
-      Lam nm <$> go !(b $$ var) t ctx'
-    go (VPi str Implicit a b) (RApp t (RSrcPos _ (RVar nm)) Implicit) ctx = do
+      Lam emptyFC nm <$> go !(b $$ var) t ctx'
+    go (VPi fc str Implicit a b) (RApp _ t (RVar _ nm) Implicit) ctx = do
       debug "*** \{nm} : \{show a}"
-      let var = VVar (length ctx.env) [<]
+      let var = VVar emptyFC (length ctx.env) [<]
       let ctx' = extend ctx nm a
-      Lam nm <$> go !(b $$ var) t ctx'
-    go (VPi str Implicit a b) t ctx = do
-      let var = VVar (length ctx.env) [<]
+      Lam emptyFC nm <$> go !(b $$ var) t ctx'
+    go (VPi fc str Implicit a b) t ctx = do
+      let var = VVar emptyFC (length ctx.env) [<]
       let ctx' = extend ctx "_" a
-      Lam "_" <$> go !(b $$ var) t ctx'
+      Lam emptyFC "_" <$> go !(b $$ var) t ctx'
     -- same deal with _ for name
-    go (VPi str icit x y) (RApp t RImplicit icit') ctx = ?rhs_19
-    go (VPi str icit x y) tm ctx = error {ctx} [DS "Can't use \{show tm} as pattern"]
+    go (VPi fc str icit x y) (RApp _ t (RImplicit _) icit') ctx = ?rhs_19
+    go (VPi fc str icit x y) tm ctx = error emptyFC "Can't use \{show tm} as pattern"
 
     -- nameless variable
-    go ctype RImplicit ctx = ?rhs_2
-    go ctype (RVar nm) ctx = do
+    go ctype (RImplicit _) ctx = ?rhs_2
+    go ctype (RVar _ nm) ctx = do
       debug "*** end"
       check ctx body ty
       -- pure ctx -- this should be our constructor.
     -- This happens if we run out of runway (more args and no pi)
-    go ctype tm ctx = error {ctx} [DS "unhandled in go \{show ctype} \{show tm}"]
+    go ctype tm ctx = error (getFC tm) "unhandled in go \{show ctype} \{show tm}"
 
     getArgs : Raw -> List String -> M (String, List String)
-    getArgs (RVar nm) acc = pure (nm, acc)
+    getArgs (RVar _ nm) acc = pure (nm, acc)
     -- TODO implicits
-    getArgs (RApp t (RSrcPos _ (RVar nm)) icit) acc = getArgs t (nm :: acc)
-    getArgs (RApp t (RVar nm) icit) acc = getArgs t (nm :: acc)
-    getArgs (RApp t RHole icit) acc = getArgs t ("_" :: acc)
-    getArgs (RSrcPos _ t) acc = getArgs t acc
-    getArgs tm _ = error [DS "Patterns must be constructor and vars, got \{show tm}"]
+    getArgs (RApp _ t (RVar _ nm) icit) acc = getArgs t (nm :: acc)
+    getArgs (RApp _ t (RHole _) icit) acc = getArgs t ("_" :: acc)
+    getArgs tm _ = error emptyFC "Patterns must be constructor and vars, got \{show tm}"
 
 
 check ctx tm ty = case (tm, !(forceType ty)) of
-  (RCase rsc alts, ty) => do
+  (RCase fc rsc alts, ty) => do
     (sc, scty) <- infer ctx rsc
-    let (VRef nm (TCon cnames) sp) = scty
-      | _ => error [DS "expected TCon for scrutinee type, got: \{show scty}"]
+    let (VRef fc nm (TCon cnames) sp) = scty
+      | _ => error fc "expected TCon for scrutinee type, got: \{show scty}"
     debug "constructor names \{show cnames}"
     alts' <- for alts $ checkAlt scty ctx ty
-    pure $ Case sc alts'
-    -- error [DS "implement check RCase sctype \{show scty}"]
-  (RSrcPos x tm, ty) => check ({pos := x} ctx) tm ty
+    pure $ Case emptyFC sc alts'
   -- Document a hole, pretend it's implemented
-  (RHole, ty) => do
+  (RHole fc, ty) => do
     ty' <- quote ctx.lvl ty
     let names = (toList $ map fst ctx.types)
     env <- for ctx.types $ \(n,ty) => pure "  \{n} : \{pprint names !(quote ctx.lvl ty)}"
     let msg = unlines (toList $ reverse env) ++ "  -----------\n" ++ "  goal \{pprint names ty'}"
-    debug "INFO at \{show ctx.pos}: "
+    debug "INFO at \{show fc}: "
     debug msg
     -- let context = unlines foo
     -- need to print 'warning' with position
     -- fixme - just put a name on it like idris and stuff it into top.
     -- error [DS "hole:\n\{msg}"]
-    pure $ Ref "?" Axiom  -- TODO - probably want hole opt on Def
-  (t@(RLam nm icit tm), ty@(VPi nm' icit' a b)) => do
+    pure $ Ref emptyFC "?" Axiom  -- TODO - probably want hole opt on Def
+  (t@(RLam fc nm icit tm), ty@(VPi fc' nm' icit' a b)) => do
           debug "icits \{nm} \{show icit} \{nm'} \{show icit'}"
           if icit == icit' then do
-              let var = VVar (length ctx.env) [<]
+              let var = VVar fc (length ctx.env) [<]
               let ctx' = extend ctx nm a
               tm' <- check ctx' tm !(b $$ var)
-              pure $ Lam nm tm'
+              pure $ Lam emptyFC nm tm'
             else if icit' == Implicit then do
-              let var = VVar (length ctx.env) [<]
+              let var = VVar fc (length ctx.env) [<]
               ty' <- b $$ var
               -- use nm' here if we want them automatically in scope
               sc <- check (extend ctx nm' a) t ty'
-              pure $ Lam nm' sc
+              pure $ Lam fc nm' sc
             else
-              error [(DS "Icity issue checking \{show t} at \{show ty}")]
-  (t@(RLam nm icit tm), ty) =>
-            error [(DS "Expected pi type, got \{!(prvalCtx ty)}")]
+              error fc "Icity issue checking \{show t} at \{show ty}"
+  (t@(RLam fc nm icit tm), ty) =>
+            error fc "Expected pi type, got \{!(prvalCtx ty)}"
 
-  (tm, ty@(VPi nm' Implicit a b)) => do
+  (tm, ty@(VPi fc nm' Implicit a b)) => do
     let names = toList $ map fst ctx.types
     debug "XXX edge add implicit lambda to \{show tm}"
-    let var = VVar (length ctx.env) [<]
+    let var = VVar fc (length ctx.env) [<]
     ty' <- b $$ var
     debug "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}"
     sc <- check (extend ctx nm' a) tm ty'
-    pure $ Lam nm' sc
+    pure $ Lam (getFC tm) nm' sc
 
   (tm,ty) => do
     -- We need to insert if tm is not an Implicit Lam
@@ -299,7 +294,7 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     (tm', ty') <- case !(infer ctx tm) of
       -- Kovacs doesn't insert on tm = Implicit Lam, we don't have Plicity there
       -- so I'll check the inferred type for an implicit pi
-      (tm'@(Lam{}), ty'@(VPi _ Implicit _ _)) => do debug "Lambda"; pure (tm', ty')
+      (tm'@(Lam{}), ty'@(VPi _ _ Implicit _ _)) => do debug "Lambda"; pure (tm', ty')
       (tm', ty') => do
         debug "RUN INSERT ON \{pprint names tm'} at \{show ty'}"
         insert ctx tm' ty'
@@ -308,18 +303,18 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     unifyCatch ctx ty' ty
     pure tm'
 
-infer ctx (RVar nm) = go 0 ctx.types
+infer ctx (RVar fc nm) = go 0 ctx.types
   where
     go : Nat -> Vect n (String, Val)  -> M  (Tm, Val)
     go i [] = case lookup nm !(get) of
       Just (MkEntry name ty def) => do
         debug "lookup \{name} as \{show def}"
-        pure (Ref nm def, !(eval [] CBN ty))
-      Nothing => error [DS "\{show nm} not in scope"]
-    go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty)
+        pure (Ref fc nm def, !(eval [] CBN ty))
+      Nothing => error fc "\{show nm} not in scope"
+    go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty)
       else go (i + 1) xs
   -- need environment of name -> type..
-infer ctx (RApp t u icit) = do
+infer ctx (RApp fc t u icit) = do
   (icit, t, tty) <- case the Icit icit of
       Explicit => do
         (t, tty) <- infer ctx t
@@ -330,51 +325,50 @@ infer ctx (RApp t u icit) = do
         pure (Implicit, t, tty)
 
   (a,b) <- case !(forceMeta tty) of
-    (VPi str icit' a b) => if icit' == icit then pure (a,b)
-        else error [DS "IcitMismatch \{show icit} \{show icit'}"]
+    (VPi fc str icit' a b) => if icit' == icit then pure (a,b)
+        else error fc "IcitMismatch \{show icit} \{show icit'}"
 
     -- If it's not a VPi, try to unify it with a VPi
     -- TODO test case to cover this.
     tty => do
       debug "unify PI for \{show tty}"
-      a <- eval ctx.env CBN !(freshMeta ctx)
-      b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a)
-      unify ctx 0 tty (VPi ":ins" icit a b)
+      a <- eval ctx.env CBN !(freshMeta ctx fc)
+      b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc
+      unify ctx 0 tty (VPi fc ":ins" icit a b)
       pure (a,b)
 
   u <- check ctx u a
-  pure (App t u, !(b $$ !(eval ctx.env CBN u)))
+  pure (App fc t u, !(b $$ !(eval ctx.env CBN u)))
 
-infer ctx RU = pure (U, VU) -- YOLO
-infer ctx (RPi nm icit ty ty2) = do
-  ty' <- check ctx ty VU
+infer ctx (RU fc) = pure (U fc, VU fc) -- YOLO
+infer ctx (RPi fc nm icit ty ty2) = do
+  ty' <- check ctx ty (VU fc)
   vty' <- eval ctx.env CBN ty'
   let nm := fromMaybe "_" nm
-  ty2' <- check (extend ctx nm vty') ty2 VU
-  pure (Pi nm icit ty' ty2', VU)
-infer ctx (RLet str tm tm1 tm2) = error [DS "implement RLet"]
-infer ctx (RSrcPos x tm) = infer ({pos := x} ctx) tm
-infer ctx (RAnn tm rty) = do
-  ty <- check ctx rty VU
+  ty2' <- check (extend ctx nm vty') ty2 (VU fc)
+  pure (Pi fc nm icit ty' ty2', (VU fc))
+infer ctx (RLet fc str tm tm1 tm2) = error fc "implement RLet"
+infer ctx (RAnn fc tm rty) = do
+  ty <- check ctx rty (VU fc)
   vty <- eval ctx.env CBN ty
   tm <- check ctx tm vty
   pure (tm, vty)
 
-infer ctx (RLam nm icit tm) = do
-  a <- freshMeta ctx >>= eval ctx.env CBN
+infer ctx (RLam fc nm icit tm) = do
+  a <- freshMeta ctx fc >>= eval ctx.env CBN
   let ctx' = extend ctx nm a
   (tm', b) <- infer ctx' tm
   debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}"
-  pure $ (Lam nm tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
+  pure $ (Lam fc nm tm', VPi fc nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b))
   -- error {ctx} [DS "can't infer lambda"]
 
-infer ctx RImplicit = do
-  ty <- freshMeta ctx
+infer ctx (RImplicit fc) = do
+  ty <- freshMeta ctx fc
   vty <- eval ctx.env CBN ty
-  tm <- freshMeta ctx
+  tm <- freshMeta ctx fc
   pure (tm, vty)
 
-infer ctx tm = error [DS "Implement infer \{show tm}"]
+infer ctx tm = error (getFC tm) "Implement infer \{show tm}"
 
 -- I don't have types for these yet...
 -- infer ctx (RLit (LString str)) = ?rhs_10
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 49d657e..716db5f 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -1,7 +1,7 @@
 module Lib.Parser
 import Lib.Types
 
--- The SourcePos stuff is awkward later on. We might want bounds on productions
+-- The FC stuff is awkward later on. We might want bounds on productions
 -- But we might want to consider something more generic and closer to lean?
 
 -- app: foo {a} a b
@@ -51,22 +51,20 @@ optional pa = Just <$> pa <|> pure Nothing
 lit : Parser Raw
 lit = do
   t <- token Number
-  pure $ RLit (LInt (cast t))
+  fc <- getFC
+  pure $ RLit fc (LInt (cast t))
 
 -- typeExpr is term with arrows.
 export typeExpr : Parser Raw
 export term : (Parser Raw)
 
-withPos : Parser Raw -> Parser Raw
-withPos p = RSrcPos <$> getPos <*> p
-
 -- the inside of Raw
 atom : Parser Raw
-atom = withPos (RU <$ keyword "U"
-              <|> RVar <$> ident
-              <|> lit
-              <|> RImplicit <$ keyword "_"
-              <|> RHole <$ keyword "?")
+atom = RU <$> getFC <* keyword "U"
+    <|> RVar <$> getFC <*> ident
+    <|> lit
+    <|> RImplicit <$> getFC <* keyword "_"
+    <|> RHole <$> getFC <* keyword "?"
     <|> parens typeExpr
 
 -- Argument to a Spine
@@ -88,7 +86,8 @@ parseApp : Parser Raw
 parseApp = do
   hd <- atom
   rest <- many pArg
-  pure $ foldl (\a, (c,b) => RApp a b c) hd rest
+  fc <- getFC
+  pure $ foldl (\a, (c,b) => RApp fc a b c) hd rest
 
 parseOp : Parser Raw
 parseOp = parseApp >>= go 0
@@ -96,13 +95,14 @@ parseOp = parseApp >>= go 0
     go : Int -> Raw -> Parser Raw
     go prec left =
       do
+        fc <- getFC
         op <- token Oper
         let Just (p,fix) = lookup op operators
          | Nothing => fail "expected operator"
         if p >= prec then pure () else fail ""
         let pr = case fix of InfixR => p; _ => p + 1
         right <- go pr !(parseApp)
-        go prec (RApp (RApp (RVar op) left Explicit) right Explicit)
+        go prec (RApp fc (RApp fc (RVar fc op) left Explicit) right Explicit)
       <|> pure left
 
 export
@@ -113,16 +113,17 @@ letExpr = do
   alts <- startBlock $ someSame $ letAssign
   keyword' "in"
   scope <- typeExpr
-
-  pure $ foldl (\ acc, (n,v) => RLet n RImplicit v acc) scope alts
+  fc <- getFC
+  pure $ foldl (\ acc, (n,fc,v) => RLet fc n (RImplicit fc) v acc) scope alts
   where
-    letAssign : Parser (Name,Raw)
+    letAssign : Parser (Name,FC,Raw)
     letAssign = do
+      fc <- getFC
       name <- ident
       -- TODO type assertion
       keyword "="
       t <- typeExpr
-      pure (name,t)
+      pure (name,fc,t)
 
 pLetArg : Parser (Icit, String, Maybe Raw)
 pLetArg = (Implicit,,) <$> braces ident <*> optional (sym ":" >> typeExpr)
@@ -139,7 +140,8 @@ lamExpr = do
   args <- some pLetArg
   keyword "=>"
   scope <- typeExpr
-  pure $ foldr (\(icit, name, ty), sc => RLam name icit sc) scope args
+  fc <- getFC
+  pure $ foldr (\(icit, name, ty), sc => RLam fc name icit sc) scope args
 
 pPattern : Parser Pattern
 pPattern
@@ -163,10 +165,10 @@ caseExpr = do
   sc <- term
   keyword "of"
   alts <- startBlock $ someSame $ caseAlt
-  pure $ RCase sc alts
+  pure $ RCase !(getFC) sc alts
 
 -- This hits an idris codegen bug if parseOp is last and Lazy
-term =  withPos $ caseExpr
+term =  caseExpr
     <|> letExpr
     <|> lamExpr
     <|> parseOp
@@ -187,10 +189,10 @@ ibind = do
   mustWork $ do
     names <- some ident
     ty <- optional (sym ":" >> typeExpr)
-    pos <- getPos
+    pos <- getFC
     sym "}"
-    -- getPos is a hack here, I would like to position at the name...
-    pure $ map (\name => (name, Implicit, fromMaybe (RSrcPos pos RImplicit) ty)) names
+    -- getFC is a hack here, I would like to position at the name...
+    pure $ map (\name => (name, Implicit, fromMaybe (RImplicit pos) ty)) names
 
 arrow : Parser Unit
 arrow = sym "->" <|> sym "→"
@@ -202,10 +204,11 @@ binders = do
   arrow
   commit
   scope <- typeExpr
-  pure $ foldr mkBind scope (join binds)
+  fc <- getFC
+  pure $ foldr (mkBind fc) scope (join binds)
   where
-    mkBind : (String, Icit, Raw) -> Raw -> Raw
-    mkBind (name, icit, ty) scope = RPi (Just name) icit ty scope
+    mkBind : FC -> (String, Icit, Raw) -> Raw -> Raw
+    mkBind fc (name, icit, ty) scope = RPi fc (Just name) icit ty scope
 
 typeExpr = binders
   <|> do
@@ -214,7 +217,7 @@ typeExpr = binders
         case scope of
           Nothing      => pure exp
           -- consider Maybe String to represent missing
-          (Just scope) => pure $ RPi Nothing Explicit exp scope
+          (Just scope) => pure $ RPi !(getFC) Nothing Explicit exp scope
 
 
 -- And top level stuff
@@ -222,20 +225,21 @@ typeExpr = binders
 
 export
 parseSig : Parser Decl
-parseSig = TypeSig <$> ident <* keyword ":" <*> mustWork typeExpr
+parseSig = TypeSig <$> getFC <*> ident <* keyword ":" <*> mustWork typeExpr
 
 parseImport : Parser Decl
-parseImport = DImport <$ keyword "import" <* commit <*> ident
+parseImport = DImport <$> getFC <* keyword "import" <* commit <*> ident
 
 -- Do we do pattern stuff now? or just name = lambda?
 
 export
 parseDef : Parser Decl
-parseDef = Def <$> ident <* keyword "=" <*> mustWork typeExpr
+parseDef = Def <$> getFC <*> ident <* keyword "=" <*> mustWork typeExpr
 
 export
 parseData : Parser Decl
 parseData = do
+  fc <- getFC
   keyword "data"
   name <- ident
   keyword ":"
@@ -244,12 +248,12 @@ parseData = do
   commit
   decls <- startBlock $ manySame $ parseSig
   -- TODO - turn decls into something more useful
-  pure $ Data name ty decls
+  pure $ Data fc name ty decls
 
 -- Not sure what I want here.
 -- I can't get a Tm without a type, and then we're covered by the other stuff
 parseNorm : Parser Decl
-parseNorm = DCheck <$ keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
+parseNorm = DCheck <$> getFC <* keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
 
 export
 parseDecl : Parser Decl
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index 9c58b57..6e0326d 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -21,15 +21,18 @@ data Fixity = InfixL | InfixR | Infix
 
 -- I was going to use a record, but we're peeling this off of bounds at the moment.
 public export
-SourcePos : Type
-SourcePos = (Int,Int)
+FC : Type
+FC = (Int,Int)
 
-emptyPos : SourcePos
-emptyPos = (0,0)
+%name FC fc
+
+export
+emptyFC : FC
+emptyFC = (0,0)
 
 -- Error of a parse
 public export
-data Error = E SourcePos String
+data Error = E FC String
 %name Error err
 
 public export
@@ -64,14 +67,14 @@ Functor Result where
 
 -- dunno why I'm making that a pair..
 export
-data Parser a = P (TokenList -> Bool -> (lc : SourcePos) -> Result a)
+data Parser a = P (TokenList -> Bool -> (lc : FC) -> Result a)
 
 export
-runP : Parser a -> TokenList -> Bool -> SourcePos -> Result a
+runP : Parser a -> TokenList -> Bool -> FC -> Result a
 runP (P f) = f
 
 error : TokenList -> String -> Error
-error [] msg = E emptyPos msg
+error [] msg = E emptyFC msg
 error ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (line, col) msg
 
 export
@@ -156,9 +159,9 @@ mutual
 
 -- withIndentationBlock - sets the col
 export
-getPos : Parser SourcePos
-getPos = P $ \toks,com, (l,c) => case toks of
-  [] => Fail False (error toks "End of file") toks com -- OK emptyPos toks com
+getFC : Parser FC
+getFC = P $ \toks,com, (l,c) => case toks of
+  [] => OK emptyFC toks com
   (t :: ts) => OK (start t) toks com
 
 ||| Start an indented block and run parser in it
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 8231ba8..9c55b9e 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -11,27 +11,23 @@ import Lib.Syntax
 
 export
 processDecl : Decl -> M ()
-processDecl (TypeSig nm tm) = do
+processDecl (TypeSig fc nm tm) = do
   top <- get
   putStrLn "-----"
   putStrLn "TypeSig \{nm} \{show tm}"
-  ty <- check (mkCtx top.metas) tm VU
+  ty <- check (mkCtx top.metas) tm (VU fc)
   ty' <- nf [] ty
   putStrLn "got \{pprint [] ty'}"
   modify $ claim nm ty'
 
-processDecl (Def nm raw) = do
+processDecl (Def fc nm raw) = do
   putStrLn "-----"
   putStrLn "def \{show nm}"
   ctx <- get
-  let pos = case raw of
-        RSrcPos pos _ => pos
-        _ => (0,0)
-
   let Just entry = lookup nm ctx
-    | Nothing => throwError $ E pos "skip def \{nm} without Decl"
+    | Nothing => throwError $ E fc "skip def \{nm} without Decl"
   let (MkEntry name ty Axiom) := entry
-    | _ => throwError $ E pos "\{nm} already defined"
+    | _ => throwError $ E fc "\{nm} already defined"
   putStrLn "check \{nm} = \{show raw} at \{pprint [] ty}"
   vty <- eval empty CBN ty
   putStrLn "vty is \{show vty}"
@@ -48,11 +44,11 @@ processDecl (Def nm raw) = do
   debug "Add def \{nm} \{pprint [] tm} : \{pprint [] ty}"
   put (addDef ctx nm tm ty)
 
-processDecl (DCheck tm ty) = do
+processDecl (DCheck fc tm ty) = do
 
   top <- get
   putStrLn "check \{show tm} at \{show ty}"
-  ty' <- check (mkCtx top.metas) tm VU
+  ty' <- check (mkCtx top.metas) tm (VU fc)
   putStrLn "got type \{pprint [] ty'}"
   vty <- eval [] CBN ty'
   res <- check (mkCtx top.metas) ty vty
@@ -65,22 +61,22 @@ processDecl (DCheck tm ty) = do
   -- norm <- nf [] x
   putStrLn "NF "
 
-processDecl (DImport str) = throwError $ E (0,0) "import not implemented"
+processDecl (DImport fc str) = throwError $ E fc "import not implemented"
 
-processDecl (Data nm ty cons) = do
+processDecl (Data fc nm ty cons) = do
   -- It seems like the FC for the errors are not here?
   ctx <- get
-  tyty <- check (mkCtx ctx.metas) ty VU
+  tyty <- check (mkCtx ctx.metas) ty (VU fc)
   -- FIXME we need this in scope, but need to update
   modify $ claim nm tyty
   ctx <- get
   cnames <- for cons $ \x => case x of
       -- expecting tm to be a Pi type
-      (TypeSig nm' tm) => do
+      (TypeSig fc nm' tm) => do
           ctx <- get
           -- TODO check pi type ending in full tyty application
           -- TODO count arity
-          dty <- check (mkCtx ctx.metas) tm VU
+          dty <- check (mkCtx ctx.metas) tm (VU fc)
           modify $ defcon nm' 0 nm dty
           pure nm'
       _ => throwError $ E (0,0) "expected constructor declaration"
@@ -92,8 +88,6 @@ processDecl (Data nm ty cons) = do
   pure ()
   where
     checkDeclType : Tm -> M ()
-    checkDeclType U = pure ()
-    checkDeclType (Pi str icit t u) = checkDeclType u
-    checkDeclType _ = throwError $ E (0,0) "data type doesn't return U"
-
-
+    checkDeclType (U _) = pure ()
+    checkDeclType (Pi _ str icit t u) = checkDeclType u
+    checkDeclType _ = error fc "data type doesn't return U"
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index d32cdce..15e6b77 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -27,27 +27,43 @@ data Pattern
 public export
 data RCaseAlt = MkAlt Raw Raw
 
+-- FC = MkPair Int Int
+
+
 data Raw : Type where
-  RVar : (nm : Name) -> Raw
-  RLam : (nm : String) -> (icit : Icit) -> (ty : Raw) -> Raw
-  RApp : (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw
-  RU   : Raw
-  RPi  : (nm : Maybe Name) -> (icit : Icit) -> (ty : Raw) -> (sc : Raw) -> Raw
-  RLet : (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw
-  -- REVIEW do we want positions on terms?
-  RSrcPos : SourcePos -> Raw -> Raw
-  RAnn  : (tm : Raw) -> (ty : Raw) -> Raw
-  RLit : Literal -> Raw
-  RCase : (scrut : Raw) -> (alts : List RCaseAlt) -> Raw
-  RImplicit : Raw
-  RHole : Raw
+  RVar : FC -> (nm : Name) -> Raw
+  RLam : FC -> (nm : String) -> (icit : Icit) -> (ty : Raw) -> Raw
+  RApp : FC -> (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw
+  RU   : FC -> Raw
+  RPi  : FC -> (nm : Maybe Name) -> (icit : Icit) -> (ty : Raw) -> (sc : Raw) -> Raw
+  RLet : FC -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw
+  RAnn  : FC -> (tm : Raw) -> (ty : Raw) -> Raw
+  RLit : FC -> Literal -> Raw
+  RCase : FC -> (scrut : Raw) -> (alts : List RCaseAlt) -> Raw
+  RImplicit : FC -> Raw
+  RHole : FC -> Raw
   -- not used, but intended to allow error recovery
-  RParseError : String -> Raw
+  RParseError : FC -> String -> Raw
 
 %name Raw tm
 
+export
+getFC : Raw -> FC
+getFC (RVar fc nm) = fc
+getFC (RLam fc nm icit ty) = fc
+getFC (RApp fc t u icit) = fc
+getFC (RU fc) = fc
+getFC (RPi fc nm icit ty sc) = fc
+getFC (RLet fc nm ty v sc) = fc
+getFC (RAnn fc tm ty) = fc
+getFC (RLit fc y) = fc
+getFC (RCase fc scrut alts) = fc
+getFC (RImplicit fc) = fc
+getFC (RHole fc) = fc
+getFC (RParseError fc str) = fc
 -- derive some stuff - I'd like json, eq, show, ...
 
+-- FIXME - I think I don't want "where" here, but the parser has an issue
 public export
 data Decl : Type where
 
@@ -57,11 +73,11 @@ Telescope = List Decl -- pi-forall, always typeSig?
 data ConstrDef = MkCDef Name Telescope
 
 data Decl
-  = TypeSig Name Raw
-  | Def Name Raw
-  | DImport Name
-  | DCheck Raw Raw
-  | Data Name Raw (List Decl)
+  = TypeSig FC Name Raw
+  | Def FC Name Raw
+  | DImport FC Name
+  | DCheck FC Raw Raw
+  | Data FC Name Raw (List Decl)
 
 public export
 record Module where
@@ -93,11 +109,11 @@ Show ConstrDef where
 
 covering
 Show Decl where
-  show (TypeSig str x) = foo ["TypeSig", show str, show x]
-  show (Def str x) = foo ["Def", show str, show x]
-  show (Data str xs ys) = foo ["Data", show str, show xs, show ys]
-  show (DImport str) = foo ["DImport", show str]
-  show (DCheck x y) = foo ["DCheck", show x, show y]
+  show (TypeSig _ str x) = foo ["TypeSig", show str, show x]
+  show (Def _ str x) = foo ["Def", show str, show x]
+  show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys]
+  show (DImport _ str) = foo ["DImport", show str]
+  show (DCheck _ x y) = foo ["DCheck", show x, show y]
 
 export covering
 Show Module where
@@ -119,20 +135,18 @@ Show RCaseAlt where
 
 covering
 Show Raw where
-  show RImplicit = "_"
-  show RHole = "?"
-  show (RVar name) = foo ["RVar", show name]
-  show (RAnn t ty) = foo [ "RAnn", show t, show ty]
-  show (RLit x) = foo [ "RLit", show x]
-  show (RLet x ty v scope) = foo [ "Let", show x, " : ", show ty, " = ", show v, " in ", show scope]
-  show (RPi str x y z) = foo [ "Pi", show str, show x, show y, show z]
-  show (RApp x y z) = foo [ "App", show x, show y, show z]
-  show (RLam x i y) = foo [ "Lam", show x, show i, show y]
-  show (RCase x xs) = foo [ "Case", show x, show xs]
-  show (RParseError str) = foo [ "ParseError", "str"]
-  show RU = "U"
-  show (RSrcPos pos tm) = foo [ "#", show tm]
-
+  show (RImplicit _) = "_"
+  show (RHole _) = "?"
+  show (RVar _ name) = foo ["RVar", show name]
+  show (RAnn _ t ty) = foo [ "RAnn", show t, show ty]
+  show (RLit _ x) = foo [ "RLit", show x]
+  show (RLet _ x ty v scope) = foo [ "Let", show x, " : ", show ty, " = ", show v, " in ", show scope]
+  show (RPi _ str x y z) = foo [ "Pi", show str, show x, show y, show z]
+  show (RApp _ x y z) = foo [ "App", show x, show y, show z]
+  show (RLam _ x i y) = foo [ "Lam", show x, show i, show y]
+  show (RCase _ x xs) = foo [ "Case", show x, show xs]
+  show (RParseError _ str) = foo [ "ParseError", "str"]
+  show (RU _) = "U"
 
 export
 Pretty Raw where
@@ -146,31 +160,30 @@ Pretty Raw where
     par p p' d = if p' < p then text "(" ++ d ++ text ")" else d
 
     asDoc : Nat -> Raw -> Doc
-    asDoc p (RVar str) = text str
-    asDoc p (RLam str icit x) = par p 0 $ text "\\" ++ wrap icit (text str) <+> text "=>" <+> asDoc 0 x
+    asDoc p (RVar _ str) = text str
+    asDoc p (RLam _ str icit x) = par p 0 $ text "\\" ++ wrap icit (text str) <+> text "=>" <+> asDoc 0 x
     -- This needs precedence and operators...
-    asDoc p (RApp x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y
-    asDoc p (RApp x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}"
-    asDoc p RU = text "U"
-    asDoc p (RPi Nothing Explicit ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
-    asDoc p (RPi (Just x) Explicit ty scope) =
+    asDoc p (RApp _ x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y
+    asDoc p (RApp _ x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}"
+    asDoc p (RU _) = text "U"
+    asDoc p (RPi _ Nothing Explicit ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope
+    asDoc p (RPi _ (Just x) Explicit ty scope) =
       par p 1 $ text "(" <+> text x <+> text ":" <+> asDoc p ty <+> text ")" <+> text "->" <+/> asDoc p scope
-    asDoc p (RPi nm Implicit ty scope) =
+    asDoc p (RPi _ nm Implicit ty scope) =
       par p 1 $ text "{" <+> text (fromMaybe "_" nm) <+> text ":" <+> asDoc p ty <+> text "}" <+> text "->" <+/> asDoc 1 scope
-    asDoc p (RLet x v ty scope) =
+    asDoc p (RLet _ x v ty scope) =
       par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty
           <+> text "=" <+> asDoc p v
           <+/> text "in" <+> asDoc p scope
-    asDoc p (RSrcPos x y) = asDoc p y
     -- does this exist?
-    asDoc p (RAnn x y) = text "TODO - RAnn"
-    asDoc p (RLit (LString str)) = text $ interpolate str
-    asDoc p (RLit (LInt i)) = text $ show i
-    asDoc p (RLit (LBool x)) = text $ show x
-    asDoc p (RCase x xs) = text "TODO - RCase"
-    asDoc p RImplicit = text "_"
-    asDoc p RHole = text "?"
-    asDoc p (RParseError str) = text "ParseError \{str}"
+    asDoc p (RAnn _ x y) = text "TODO - RAnn"
+    asDoc p (RLit _ (LString str)) = text $ interpolate str
+    asDoc p (RLit _ (LInt i)) = text $ show i
+    asDoc p (RLit _ (LBool x)) = text $ show x
+    asDoc p (RCase _ x xs) = text "TODO - RCase"
+    asDoc p (RImplicit _) = text "_"
+    asDoc p (RHole _) = text "?"
+    asDoc p (RParseError _ str) = text "ParseError \{str}"
 
 export
 Pretty Module where
@@ -178,9 +191,9 @@ Pretty Module where
     text "module" <+> text name </> stack (map doDecl decls)
       where
         doDecl : Decl -> Doc
-        doDecl (TypeSig nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
-        doDecl (Def nm tm) = text nm <+> text "=" <+> nest 2 (pretty tm)
-        doDecl (DImport nm) = text "import" <+> text nm ++ line
+        doDecl (TypeSig _ nm ty) = text nm <+> text ":" <+> nest 2 (pretty ty)
+        doDecl (Def _ nm tm) = text nm <+> text "=" <+> nest 2 (pretty tm)
+        doDecl (DImport _ nm) = text "import" <+> text nm ++ line
         -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
-        doDecl (Data nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
-        doDecl (DCheck x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
+        doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
+        doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index 35379f4..868bf9c 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -7,7 +7,7 @@
 -- Kovacs has icity on App, and passes it around, but I'm not sure where it is needed since the insertion happens based on Raw.
 
 module Lib.TT
--- For SourcePos
+-- For FC
 import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.Types
@@ -30,8 +30,8 @@ toDoc (DD x) = pretty x
 toDoc (DS str) = text str
 
 export
-error : {auto ctx : Context} -> List ErrorSeg -> M a
-error xs = throwError $ E ctx.pos (render 80 $ spread $ map toDoc xs)
+error : FC -> String -> M a
+error fc msg = throwError $ E fc msg
 
 export
 error' : String -> M a
@@ -41,18 +41,18 @@ error' msg = throwError $ E (0,0) msg
 -- because of dependent types (if we want something well-typed back out)
 
 export
-freshMeta : Context -> M Tm
-freshMeta ctx = do
+freshMeta : Context -> FC -> M Tm
+freshMeta ctx fc = do
   mc <- readIORef ctx.metas
-  putStrLn "INFO at \{show ctx.pos}: fresh meta \{show mc.next}"
-  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved ctx.pos mc.next ctx.bds ::) } mc
-  pure $ applyBDs 0 (Meta mc.next) ctx.bds
+  putStrLn "INFO at \{show fc}: fresh meta \{show mc.next}"
+  writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx.bds ::) } mc
+  pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
   where
   -- hope I got the right order here :)
   applyBDs : Nat -> Tm -> List BD -> Tm
   applyBDs k t [] = t
   -- review the order here
-  applyBDs k t (Bound :: xs) = App (applyBDs (S k) t xs) (Bnd k)
+  applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k)
   applyBDs k t (Defined :: xs) = applyBDs (S k) t xs
 
 export
@@ -79,7 +79,7 @@ Show Context where
 export
 extend : Context -> String -> Val -> Context
 extend ctx name ty =
-    { lvl $= S, env $= (VVar ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
+    { lvl $= S, env $= (VVar emptyFC ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx
 
 -- I guess we define things as values?
 export
@@ -115,10 +115,10 @@ infixl 8 $$
 
 export
 vapp : Val -> Val -> M Val
-vapp (VLam _ t) u = t $$ u
-vapp (VVar k sp) u = pure $ VVar k (sp :< u)
-vapp (VRef nm def sp) u = pure $ VRef nm def (sp :< u)
-vapp (VMeta k sp) u = pure $ VMeta k (sp :< u)
+vapp (VLam _ _ t) u = t $$ u
+vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u)
+vapp (VRef fc nm def sp) u = pure $ VRef fc nm def (sp :< u)
+vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u)
 vapp t u = error' "impossible in vapp \{show t} to \{show u}"
 
 export
@@ -140,17 +140,17 @@ bind v env = v :: env
 -- I need to be aggressive about reduction, I guess. I'll figure it out
 -- later, maybe need lazy glued values.
 -- TODO - probably want to figure out gluing and handle constructors
-eval env mode (Ref x (Fn tm)) = eval env mode tm
-eval env mode (Ref x def) = pure $ VRef x def [<]
-eval env mode (App t u) = vapp !(eval env mode t) !(eval env mode u)
-eval env mode U = pure VU
-eval env mode (Meta i) =
+eval env mode (Ref _ x (Fn tm)) = eval env mode tm
+eval env mode (Ref fc x def) = pure $ VRef fc x def [<]
+eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u)
+eval env mode (U fc) = pure (VU fc)
+eval env mode (Meta fc i) =
   case !(lookupMeta i) of
-        (Unsolved _ k xs) => pure $ VMeta i [<]
+        (Unsolved _ k xs) => pure $ VMeta fc i [<]
         (Solved k t) => pure $ t
-eval env mode (Lam x t) = pure $ VLam x (MkClosure env t)
-eval env mode (Pi x icit a b) = pure $ VPi x icit !(eval env mode a) (MkClosure env b)
-eval env mode (Bnd i) = case getAt i env of
+eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
+eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
+eval env mode (Bnd fc i) = case getAt i env of
   Just rval => pure rval
   Nothing => error' "Bad deBruin index \{show i}"
 eval env mode (Case{}) = ?todo
@@ -161,17 +161,17 @@ quote : (lvl : Nat) -> Val -> M Tm
 quoteSp : (lvl : Nat) -> Tm -> SnocList Val -> M Tm
 quoteSp lvl t [<] = pure t
 quoteSp lvl t (xs :< x) =
-  pure $ App !(quoteSp lvl t xs) !(quote lvl x)
+  pure $ App emptyFC !(quoteSp lvl t xs) !(quote lvl x)
   -- quoteSp lvl (App t !(quote lvl x)) xs  -- snoc says previous is right
 
-quote l (VVar k sp) = if k < l
-  then quoteSp l (Bnd ((l `minus` k) `minus` 1)) sp -- level to index
+quote l (VVar fc k sp) = if k < l
+  then quoteSp l (Bnd emptyFC ((l `minus` k) `minus` 1)) sp -- level to index
   else ?borken
-quote l (VMeta i sp) = quoteSp l (Meta i) sp
-quote l (VLam x t) = pure $ Lam x !(quote (S l) !(t $$ VVar l [<]))
-quote l (VPi x icit a b) = pure $ Pi x icit !(quote l a) !(quote (S l) !(b $$ VVar l [<]))
-quote l VU = pure U
-quote l (VRef n def sp) = quoteSp l (Ref n def) sp
+quote l (VMeta fc i sp) = quoteSp l (Meta fc i) sp
+quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<]))
+quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
+quote l (VU fc) = pure (U fc)
+quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp
 
 -- Can we assume closed terms?
 -- ezoo only seems to use it at [], but essentially does this:
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 76dc668..2caab08 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -4,7 +4,7 @@ module Lib.Types
 -- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
 -- or drop the indices for now.
 
--- For SourcePos, Error
+-- For FC, Error
 import public Lib.Parser.Impl
 import Lib.Prettier
 
@@ -54,35 +54,47 @@ data CaseAlt : Type where
 data Def : Type
 
 data Tm : Type where
-  Bnd : Nat -> Tm
+  Bnd : FC -> Nat -> Tm
   -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
-  Ref : String -> Def -> Tm
-  Meta : Nat -> Tm
+  Ref : FC -> String -> Def -> Tm
+  Meta : FC -> Nat -> Tm
   -- kovacs optimization, I think we can App out meta instead
   -- InsMeta : Nat -> List BD -> Tm
-  Lam : Name -> Tm -> Tm
-  App : Tm -> Tm -> Tm
-  U   : Tm
-  Pi  : Name -> Icit -> Tm -> Tm -> Tm
+  Lam : FC -> Name -> Tm -> Tm
+  App : FC -> Tm -> Tm -> Tm
+  U   : FC -> Tm
+  Pi  : FC -> Name -> Icit -> Tm -> Tm -> Tm
   -- REVIEW - do we want to just push it up like idris?
-  Case : Tm -> List CaseAlt -> Tm
+  Case : FC -> Tm -> List CaseAlt -> Tm
 
 %name Tm t, u, v
 
+export
+getFC : Tm -> FC
+getFC (Bnd fc k) = fc
+getFC (Ref fc str x) = fc
+getFC (Meta fc k) = fc
+getFC (Lam fc str t) = fc
+getFC (App fc t u) = fc
+getFC (U fc) = fc
+getFC (Pi fc str icit t u) = fc
+getFC (Case fc t xs) = fc
+
+
 Show CaseAlt where
   show alt = "FIXME"
 
 -- public export
 Show Tm where
-  show (Bnd k) = "(Bnd \{show k})"
-  show (Ref str _) = "(Ref \{show str})"
-  show (Lam nm t) = "(\\ \{nm}  => \{show  t})"
-  show (App t u) = "(\{show t} \{show u})"
-  show (Meta i) = "(Meta \{show i})"
-  show U = "U"
-  show (Pi str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
-  show (Pi str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
-  show (Case sc alts) = "(Case \{show sc} \{show alts})"
+  show (Bnd _ k) = "(Bnd \{show k})"
+  show (Ref _ str _) = "(Ref \{show str})"
+  show (Lam _ nm t) = "(\\ \{nm}  => \{show  t})"
+  show (App _ t u) = "(\{show t} \{show u})"
+  show (Meta _ i) = "(Meta \{show i})"
+  show (U _) = "U"
+  show (Pi _ str Implicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
+  show (Pi _ str Explicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
+  show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
 
 -- I can't really show val because it's HOAS...
 
@@ -97,12 +109,12 @@ Eq Icit where
 export
 Eq (Tm) where
   -- (Local x) == (Local y) = x == y
-  (Bnd x) == (Bnd y) = x == y
-  (Ref x _) == (Ref y _) = x == y
-  (Lam n t) == (Lam n' t') = t == t'
-  (App t u) == App t' u' = t == t' && u == u'
-  U == U = True
-  (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u'
+  (Bnd _ x) == (Bnd _ y) = x == y
+  (Ref _ x _) == Ref _ y _ = x == y
+  (Lam _ n t) == Lam _ n' t' = t == t'
+  (App _ t u) == App _ t' u' = t == t' && u == u'
+  (U _) == (U _) = True
+  (Pi _ n icit t u) == (Pi _ n' icit' t' u') = icit == icit' && t == t' && u == u'
   _ == _ = False
 
 -- FIXME prec
@@ -112,30 +124,30 @@ pprint : List String -> Tm -> String
 pprint names tm = render 80 $ go names tm
   where
     go : List String -> Tm -> Doc
-    go names (Bnd k) = case getAt k names of
+    go names (Bnd _ k) = case getAt k names of
       Nothing => text "BND \{show k}"
       Just nm => text "\{nm}:\{show k}"
-    go names (Ref str mt) = text str
-    go names (Meta k) = text "?m:\{show k}"
-    go names (Lam nm t) = text "(\\ \{nm} =>" <+> go (nm :: names) t <+> ")"
-    go names (App t u) = text "(" <+> go names t <+> go names u <+> ")"
-    go names U = "U"
-    go names (Pi nm Implicit t u) =
+    go names (Ref _ str mt) = text str
+    go names (Meta _ k) = text "?m:\{show k}"
+    go names (Lam _ nm t) = text "(\\ \{nm} =>" <+> go (nm :: names) t <+> ")"
+    go names (App _ t u) = text "(" <+> go names t <+> go names u <+> ")"
+    go names (U _) = "U"
+    go names (Pi _ nm Implicit t u) =
       text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "=>" <+> go (nm :: names) u <+> ")"
-    go names (Pi nm Explicit t u) =
+    go names (Pi _ nm Explicit t u) =
       text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")"
-    go names (Case _ _) = "FIXME CASE"
+    go names (Case _ _ _) = "FIXME CASE"
 
 public export
 Pretty Tm where
-  pretty (Bnd k) = ?rhs_0
-  pretty (Ref str mt) = text str
-  pretty (Meta k) = text "?m\{show k}"
-  pretty (Lam str t) = text "(\\ \{str} => " <+> pretty t <+> ")"
-  pretty (App t u) = text "(" <+> pretty t <+> pretty u <+> ")"
-  pretty U = "U"
-  pretty (Pi str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")"
-  pretty (Case _ _) = text "FIXME CASE"
+  pretty (Bnd _ k) = ?rhs_0
+  pretty (Ref _ str mt) = text str
+  pretty (Meta _ k) = text "?m\{show k}"
+  pretty (Lam _ str t) = text "(\\ \{str} => " <+> pretty t <+> ")"
+  pretty (App _ t u) = text "(" <+> pretty t <+> pretty u <+> ")"
+  pretty (U _) = "U"
+  pretty (Pi _ str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")"
+  pretty (Case _ _ _) = text "FIXME CASE"
 
 -- public export
 -- data Closure : Nat -> Type
@@ -159,28 +171,28 @@ data Closure : Type
 public export
 data Val : Type where
   -- This will be local / flex with spine.
-  VVar : (k : Nat) -> (sp : SnocList Val) -> Val
+  VVar : FC -> (k : Nat) -> (sp : SnocList Val) -> Val
   -- I wanted the Maybe Tm in here, but for now we're always expanding.
   -- Maybe this is where I glue
-  VRef : (nm : String) -> Def -> (sp : SnocList Val) -> Val
+  VRef : FC -> (nm : String) -> Def -> (sp : SnocList Val) -> Val
   -- we'll need to look this up in ctx with IO
-  VMeta : (ix : Nat) -> (sp : SnocList Val) -> Val
-  VLam : Name -> Closure -> Val
-  VPi : Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val
-  VU : Val
+  VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val
+  VLam : FC -> Name -> Closure -> Val
+  VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val
+  VU : FC -> Val
 
 
 Show Closure
 
 covering export
 Show Val where
-  show (VVar k sp) = "(%var \{show k} \{show sp})"
-  show (VRef nm _ sp) = "(%ref \{nm} \{show sp})"
-  show (VMeta ix sp) = "(%meta \{show ix} \{show sp})"
-  show (VLam str x) = "(%lam \{str} \{show x})"
-  show (VPi str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
-  show (VPi str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"
-  show VU = "U"
+  show (VVar _ k sp) = "(%var \{show k} \{show sp})"
+  show (VRef _ nm _ sp) = "(%ref \{nm} \{show sp})"
+  show (VMeta _ ix sp) = "(%meta \{show ix} \{show sp})"
+  show (VLam _ str x) = "(%lam \{str} \{show x})"
+  show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show  x}}. \{show  y})"
+  show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show  x}). \{show  y})"
+  show (VU _) = "U"
 
 -- Not used - I was going to change context to have a List Binder
 -- instead of env, types, bds
@@ -234,7 +246,7 @@ Can I get val back? Do we need to quote? What happens if we don't?
 -}
 
 public export
-data MetaEntry = Unsolved SourcePos Nat (List BD) | Solved Nat Val
+data MetaEntry = Unsolved FC Nat (List BD) | Solved Nat Val
 
 export
 covering
@@ -301,7 +313,6 @@ record Context where
   types : Vect lvl (String, Val) -- types and names in scope
   -- so we'll try "bds" determines length of local context
   bds  : List BD          -- bound or defined
-  pos : SourcePos            -- the last SourcePos that we saw
 
   -- We only need this here if we don't pass TopContext
   -- top : TopContext
@@ -320,7 +331,7 @@ M = (StateT TopContext (EitherT Impl.Error IO))
 -- around top
 export
 mkCtx : IORef MetaContext -> Context
-mkCtx metas = MkCtx 0 [] [] [] (0,0) metas
+mkCtx metas = MkCtx 0 [] [] [] metas
 
 ||| Force argument and print if verbose is true
 export