Introduce better logging.

Led to immediate bug fixes for Pi types.

7 files changed, 349 insertions, 168 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 92a1da7..bee4872 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -9,6 +9,7 @@ main = Obs.Main
 
 modules
   = Obs.Abstract
+  , Obs.Logging
   , Obs.Main
   , Obs.NormalForm
   , Obs.Parser
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 0915152..90616d4 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -3,6 +3,7 @@ module Obs.Abstract
 import Data.Fin
 import Data.String
 
+import Obs.Logging
 import Obs.Syntax
 import Obs.Term
 
@@ -11,31 +12,17 @@ import Text.Bounded
 
 %default total
 
-public export
 Context : Nat -> Type
 Context n = List (String, Fin n)
 
 bind : Context n -> String -> Context (S n)
 bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 
-Error : Type -> Type
-Error = Either (Bounds, String)
-
-report : Bounds -> String -> Error a
-report = curry Left
-
 export
-printErr : Error a -> IO a
-printErr (Left (b, str)) = do
-  () <- putStrLn "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
-  exitFailure
-printErr (Right x) = pure x
-
-export
-abstractSyntax : Context n -> Syntax -> Error (Term n)
+abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntax ctx (Var var) = do
   let Just i = lookup var.val ctx
-    | Nothing => report var.bounds "unbound variable: \{var.val}"
+    | Nothing => inScope "unbound variable" $ fatal var
   pure (Var var i)
 abstractSyntax ctx (Sort bounds s) = pure (Sort bounds s)
 abstractSyntax ctx (Pi bounds var a b) = do
@@ -57,8 +44,7 @@ abstractSyntax ctx (Absurd bounds a t) = do
   t <- abstractSyntax ctx t
   pure (Absurd bounds a t)
 
-export
-abstractDefinition : Context n -> Definition -> Error (Definition n)
+abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
   { name = def.name
   , bounds = def.bounds
@@ -67,12 +53,12 @@ abstractDefinition ctx def = pure $ MkDefinition
   }
 
 export
-abstractBlock : (defs : List Definition) -> Error (Block (length defs))
+abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
 abstractBlock defs =
   let asContext : Block n -> Context n
       asContext []            = []
       asContext (defs :< def) = bind (asContext defs) def.name
-  in let helper : Block n -> (defs : List Definition) -> Error (Block (length defs + n))
+  in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
          helper blk []            = pure blk
          helper blk (def :: defs) = do
            def <- abstractDefinition (asContext blk) def
diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
new file mode 100644
index 0000000..0761775
--- /dev/null
+++ b/src/Obs/Logging.idr
@@ -0,0 +1,148 @@
+module Obs.Logging
+
+import Data.List.Lazy
+
+import System
+
+import Text.Bounded
+import public Text.PrettyPrint.Prettyprinter
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
+
+-- Logging Levels --------------------------------------------------------------
+
+public export
+data Level = Trace | Info | Debug | Warn | Error
+
+export
+Show Level where
+  show Trace = "trace"
+  show Info  = "info"
+  show Debug = "debug"
+  show Warn  = "warn"
+  show Error = "error"
+
+levelToNat : Level -> Nat
+levelToNat Trace = 4
+levelToNat Info  = 3
+levelToNat Debug = 2
+levelToNat Warn  = 1
+levelToNat Error = 0
+
+export
+Eq Level where
+  l == l' = levelToNat l == levelToNat l'
+
+export
+Ord Level where
+  compare l l' = compare (levelToNat l) (levelToNat l')
+
+-- Logging Messages ------------------------------------------------------------
+
+record Message (ann : Type) where
+  constructor MkMessage
+  lvl  : Level
+  msg  : Doc ann
+  tags : List String
+
+pretty : Message ann -> Doc ann
+pretty msg =
+  hsep $
+  [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
+  reverse (map (\s => pretty s <+> colon) msg.tags) ++
+  [ align msg.msg ]
+
+-- Logging Monad ---------------------------------------------------------------
+
+export
+record Logging (ann, t : Type) where
+  constructor MkLogging
+  out  : Maybe t
+  msgs : LazyList (Message ann)
+
+export
+Functor (Logging ann) where
+  map f = {out $= map f}
+
+export
+Applicative (Logging ann) where
+  pure v = MkLogging {out = pure v, msgs = []}
+  f <*> v = MkLogging {out = f.out <*> v.out, msgs = f.msgs ++ v.msgs}
+
+export
+Monad (Logging ann) where
+  (MkLogging Nothing  msgs) >>= f = MkLogging Nothing msgs
+  (MkLogging (Just v) msgs) >>= f = {msgs $= (msgs ++)} (f v)
+
+-- -- Eliminators -----------------------------------------------------------------
+
+export
+discard : Logging ann a -> Maybe a
+discard = out
+
+export
+logToTerminal : Level -> Logging AnsiStyle a -> IO a
+logToTerminal lvl log = do
+  Lazy.for_ (filter (\msg => msg.lvl <= lvl) log.msgs) (putDoc . pretty)
+  case log.out of
+    Just v => pure v
+    Nothing => exitFailure
+
+export
+abort : Logging ann a
+abort = MkLogging Nothing []
+
+export
+inScope : (tag : String) -> Logging ann a -> Logging ann a
+inScope tag = {msgs $= map {tags $= (tag ::)}}
+
+public export
+interface Loggable (0 ann, ty : Type) where
+  log : Level -> ty -> Logging ann ()
+
+export
+trace : Loggable ann ty => ty -> Logging ann ()
+trace = log Trace
+
+export
+info : Loggable ann ty => ty -> Logging ann ()
+info = log Info
+
+export
+debug : Loggable ann ty => ty -> Logging ann ()
+debug = log Debug
+
+export
+warn : Loggable ann ty => ty -> Logging ann ()
+warn = log Warn
+
+export
+error : Loggable ann ty => ty -> Logging ann ()
+error = log Error
+
+export
+fatal : Loggable ann ty => ty -> Logging ann a
+fatal msg = do error msg; abort
+  
+export
+Loggable ann (Doc ann) where
+  log lvl msg = MkLogging (pure ()) [MkMessage lvl msg []]
+
+export
+Pretty x => Loggable ann x where
+  log lvl msg = log lvl $ pretty {ann = ann} msg
+
+export
+Loggable ann x => Loggable ann (WithBounds x) where
+  log lvl msg =
+    let f : Logging ann () -> Logging ann ()
+        f = case msg.isIrrelevant of
+          True => id
+          False => inScope $
+            show (1 + msg.bounds.startLine) ++
+            ":" ++
+            show msg.bounds.startCol ++
+            "--" ++
+            show (1 + msg.bounds.endLine) ++
+            ":" ++
+            show msg.bounds.endCol
+    in f (log lvl msg.val)
diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index 5e0903e..fc7140a 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -1,6 +1,9 @@
 module Obs.Main
 
+import Data.DPair
+
 import Obs.Abstract
+import Obs.Logging
 import Obs.NormalForm
 import Obs.Parser
 import Obs.Syntax
@@ -8,23 +11,59 @@ import Obs.Term
 import Obs.Typing
 
 import System
+import System.File
 
-import Text.PrettyPrint.Prettyprinter
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default total
 
-usage : IO ()
-usage = do
-  () <- putStrLn "usage: obs <file>"
+record Options where
+  constructor MkOptions
+  file : String
+  lvl  : Level
+
+usage : String -> IO a
+usage prog = do
+  () <- putStrLn "usage: \{prog} <file>"
   exitFailure
 
+parseLevel : String -> Maybe Level
+parseLevel "0" = Just Error
+parseLevel "1" = Just Warn
+parseLevel "2" = Just Debug
+parseLevel "3" = Just Info
+parseLevel "4" = Just Trace
+parseLevel "error" = Just Error
+parseLevel "warn"  = Just Warn
+parseLevel "debug" = Just Debug
+parseLevel "info"  = Just Info
+parseLevel "trace" = Just Trace
+parseLevel _ = Nothing
+
+parseOptions : List1 String -> IO Options
+parseOptions (prog ::: [file, "-v", lvl]) = do
+  let Just lvl = parseLevel lvl
+    | Nothing => usage prog
+  pure $ MkOptions file lvl
+parseOptions (prog ::: [file, "-v"]) = pure $ MkOptions file Debug
+parseOptions (prog ::: [file]) = pure $ MkOptions file Error
+parseOptions (prog ::: _) = usage prog
+
+partial
+main' : (input: String) -> Logging AnsiStyle (Exists NormalForm.Context)
+main' input = do
+  defs <- parse input
+  blk  <- abstractBlock defs
+  ctx  <- checkBlock blk
+  pure (Evidence _ ctx)
+
 partial
 main : IO ()
 main = do
-  [_, file] <- getArgs
-    | _ => usage
-  defs <- parseFile file
-  blk <- Abstract.printErr $ abstractBlock defs
-  ctx <- Typing.printErr $ checkBlock blk
+  (prog :: args) <- getArgs
+    | _ => usage "obs"
+  opts <- parseOptions (prog ::: args)
+  Right input <- readFile opts.file
+    | Left err => do putStrLn "failed to open file: \{show err}"; exitFailure
+  ctx <- logToTerminal opts.lvl $ main' input
   putStrLn "Everything type checks."
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 8ee3b19..a15c3c1 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -18,14 +18,14 @@ data NormalForm  : Nat -> Type
 public export
 data Constructor : Nat -> Type where
   Sort   : Sort -> Constructor n
-  Pi     : Sort -> Sort -> NormalForm n -> NormalForm (S n) -> Constructor n
-  Lambda : NormalForm (S n) -> Constructor n
+  Pi     : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
+  Lambda : String -> NormalForm (S n) -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
 public export
 data Neutral : Nat -> Type where
-  Var    : Fin n -> Neutral n
+  Var    : String -> Fin n -> Neutral n
   App    : Neutral n -> NormalForm n -> Neutral n
   Absurd : Neutral n
 
@@ -56,13 +56,13 @@ eqNtrl  : Neutral n -> Neutral n -> Bool
 eqWhnf  : NormalForm n -> NormalForm n -> Bool
 
 eqCnstr (Sort s) (Sort s') = s == s'
-eqCnstr (Pi s s' a b) (Pi l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Lambda t) (Lambda u) = eqWhnf t u
+eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
+eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
 
-eqNtrl (Var i) (Var j) = i == j
+eqNtrl (Var _ i) (Var _ j) = i == j
 eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
 eqNtrl Absurd Absurd = True
 eqNtrl _ _ = False
@@ -99,20 +99,22 @@ prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
 prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
 
 prettyPrecCnstr d (Sort s) = prettyPrec d s
-prettyPrecCnstr d (Pi _ _ a b) =
+prettyPrecCnstr d (Pi _ _ var a b) =
   parenthesise (d > Open) $
   group $
-  parens (prettyPrecWhnf Open a) <++>
+  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
   pretty "->" <+> softline <+>
   prettyPrecWhnf Open b
-prettyPrecCnstr d (Lambda t) =
+prettyPrecCnstr d (Lambda var t) =
   parenthesise (d > Open) $
   group $
-  backslash <+> softline <+> prettyPrecWhnf Open t
+  backslash <+> pretty var <++>
+  pretty "=>" <+> softline <+>
+  prettyPrecWhnf Open t
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
-prettyPrecNtrl d (Var i) = pretty "$\{show i}"
+prettyPrecNtrl d (Var var i) = pretty "\{show var}@\{show i}"
 prettyPrecNtrl d (App t u) =
   parenthesise (d >= App) $
   group $
@@ -156,12 +158,12 @@ renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
 renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 
 renameCnstr (Sort s) f = Sort s
-renameCnstr (Pi s s' a b) f = Pi s s' (renameWhnf a f) (renameWhnf b $ lift 1 f)
-renameCnstr (Lambda t) f = Lambda (renameWhnf t $ lift 1 f)
+renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
+renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
-renameNtrl (Var i) f = Var (f i)
+renameNtrl (Var var i) f = Var var (f i)
 renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
 renameNtrl Absurd f = Absurd
 
@@ -183,7 +185,7 @@ Rename NormalForm where
 
 export
 PointedRename Neutral where
-  point = Var
+  point = Var ""
 
 export
 PointedRename NormalForm where
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index c9705fb..f9daa62 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -2,6 +2,7 @@ module Obs.Parser
 
 import Data.String
 
+import Obs.Logging
 import Obs.Sort
 import Obs.Syntax
 
@@ -13,12 +14,6 @@ import Text.Parser
 
 %default total
 
-Error : Type -> Type -> Type
-Error tok = Either (List1 (ParsingError tok))
-
-report : List1 (ParsingError tok) -> Error tok a
-report = Left
-
 data ObsTokenKind
   = OTNewline
   | OTIgnore
@@ -230,35 +225,24 @@ postprocess (tok :: tail@(tok' :: toks)) = case (tok.val.kind, tok'.val.kind) of
   (OTPOpen, OTPClose) => map (\_ => Tok OTUnit "()") (mergeBounds tok tok') :: postprocess toks
   _ => if ignored tok then postprocess tail else tok :: postprocess tail
 
+castErr : Either (List1 (ParsingError tok)) a -> Logging ann a
+castErr (Right x) = pure x
+castErr (Left errs) = do
+  for_ {b = ()} errs
+    (\(Error msg bounds) =>
+      error $
+      maybe
+        (irrelevantBounds $ msg)
+        (\bounds => MkBounded msg False bounds) $
+      bounds)
+  abort
+
 partial
 export
-parse : String -> Error ObsToken (List Definition)
+parse : String -> Logging ann (List Definition)
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
-    | (_, l, c, rem) => report (Error "failed to lex input" (Just $ MkBounds { startLine = l, startCol = c, endLine = l, endCol = c }) ::: [])
-  (defs, []) <- parse file $ postprocess toks
-    | (_, (t :: _)) => report (Error "unparsed tokens" (Just t.bounds) ::: [])
-  pure defs
-
-printErr : ParsingError tok -> IO ()
-printErr (Error str Nothing)  = putStrLn "error: \{str}"
-printErr (Error str (Just b)) = putStrLn
-  "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
-
-reportErrs : List (ParsingError tok) -> IO a
-reportErrs []          = exitFailure
-reportErrs (e :: errs) = do
-  () <- printErr e
-  reportErrs errs
-
-partial
-export
-parseFile : (fname : String) -> IO (List Definition)
-parseFile fname = do
-  Right str <- readFile fname
-    | Left err => do
-      () <- putStrLn "error: \{show err}"
-      exitFailure
-  let Right defs = parse str
-    | Left err => reportErrs (forget err)
+    | (_, l, c, rem) => inScope "lex" $ fatal "failed to lex input"
+  (defs, []) <- inScope "parse" $ castErr $ parse file $ postprocess toks
+    | (_, (t :: _)) => inScope "parse" $ fatal "unparsed tokens"
   pure defs
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index e23a9a2..c5d837f 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -1,7 +1,8 @@
 module Obs.Typing
 
-import Data.Fin
+import Data.Vect
 
+import Obs.Logging
 import Obs.NormalForm
 import Obs.Sort
 import Obs.Substitution
@@ -15,60 +16,58 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default total
 
--- Errors ----------------------------------------------------------------------
+-- Loggings ----------------------------------------------------------------------
 
-export
-Error : Type -> Type -> Type
-Error ann = Either (Maybe Bounds, Doc ann)
-
-export
-printErr : Error ? a -> IO a
-printErr (Left (Just b, p)) = do
-  () <- putDoc (pretty "typing: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}:" <+> softline <+> p)
-  exitFailure
-printErr (Left (Nothing, p)) = do
-  () <- putDoc (pretty "typing:" <+> softline <+> p)
-  exitFailure
-printErr (Right x) = pure x
-
-report : Bounds -> Doc ann -> Error ann a
-report = curry Left . Just
-
-internal : Doc ann -> Error ann a
-internal = Left . (Nothing, )
-
-Rename (Error ann . NormalForm) where
+Rename (Logging ann . NormalForm) where
   rename t f = pure $ rename !t f
 
-PointedRename (Error ann . NormalForm) where
-  point = pure . point
+mismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
+mismatch bounds lhs rhs = fatal $
+  MkBounded
+    (pretty "expected" <++> lhs <+> comma <+> softline <+> pretty "got" <++> rhs)
+    False
+    bounds
+
+typeMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
+typeMismatch bounds lhs rhs = inScope "type mismatch" $ mismatch bounds lhs rhs
+
+sortMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
+sortMismatch bounds lhs rhs = inScope "sort mismatch" $ mismatch bounds lhs rhs
 
 -- Substitution ----------------------------------------------------------------
 
-wkn : (k : _) -> (Fin n -> Error ann (NormalForm m)) -> Fin (k + n) -> Error ann (NormalForm (k + m))
-wkn = lift {x = Error ann . NormalForm}
+wkn : Vect k String -> (Fin n -> Logging ann (NormalForm m)) -> Fin (k + n) -> Logging ann (NormalForm (k + m))
+wkn []            f = f
+wkn (var :: vars) f =
+  add
+    (Logging ann . NormalForm)
+    (pure $ Ntrl $ Var var FZ)
+    (\i => pure $ rename !(wkn vars f i) FS)
 
 covering partial
-substCnstr : Constructor n -> (Fin n -> Error ann (NormalForm m)) -> Error ann (Constructor m)
+substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
 covering partial
-substNtrl  : Neutral n -> (Fin n -> Error ann (NormalForm m)) -> Error ann (NormalForm m)
+substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
 covering partial
-subst      : NormalForm n -> (Fin n -> Error ann (NormalForm m)) -> Error ann (NormalForm m)
+subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
 covering partial
-doApp      : NormalForm n -> NormalForm n -> Error ann (NormalForm n)
+doApp      : NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
 
 substCnstr (Sort s) f = pure $ Sort s
-substCnstr (Pi s s' a b) f = do
+substCnstr (Pi s s' var a b) f = do
   a <- subst a f
-  b <- subst b (wkn 1 f)
-  pure (Pi s s' a b)
-substCnstr (Lambda t) f = do
-  t <- subst t (wkn 1 f)
-  pure (Lambda t)
+  b <- subst b (wkn [var] f)
+  pure (Pi s s' var a b)
+substCnstr (Lambda var t) f = do
+  t <- subst t (wkn [var] f)
+  pure (Lambda var t)
 substCnstr Top f = pure $ Top
 substCnstr Bottom  f = pure $ Bottom
 
-substNtrl (Var i) f = f i
+substNtrl (Var var i) f = do
+  Ntrl (Var "" j) <- f i
+    | t => pure t
+  pure (Ntrl (Var var j))
 substNtrl (App t u) f = do
   t <- substNtrl t f
   u <- subst u f
@@ -81,26 +80,26 @@ subst Irrel     f = pure Irrel
 
 doApp (Ntrl t) u = pure $ Ntrl (App t u)
 doApp Irrel u = pure $ Irrel
-doApp (Cnstr (Lambda t)) u = subst t (add (Error ann . NormalForm) (pure u) (pure . point))
-doApp (Cnstr t) u = internal (pretty "wrong constructor in apply:" <++> pretty t)
+doApp (Cnstr (Lambda var t)) u = subst t (add (Logging ann . NormalForm) (pure u) (pure . point))
+doApp (Cnstr t) u = inScope "wrong constructor in apply:" $ fatal t
 
 partial
-subst1 : NormalForm n -> NormalForm (S n) -> Error ann (NormalForm n)
-subst1 t u = subst u (add (Error ann . NormalForm) (pure t) (pure . point))
+subst1 : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
+subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
 
 -- Conversion ------------------------------------------------------------------
 
 -- invariant: all definitions fully expanded
 -- invariant: m |- t, u <- a : s
 covering partial
-convert : (t, u, a : NormalForm n) -> Sort -> Error ann Bool
+convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
 -- In sort Prop
 convert Irrel Irrel a Prop = pure True
 -- In unknown type in set
 convert t u (Ntrl _) (Set k) = pure $ t == u
 -- In type Set
 convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ s' == s''
-convert (Cnstr (Pi s s' a b)) (Cnstr (Pi l l' a' b')) (Cnstr (Sort _)) (Set _) =
+convert (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) (Cnstr (Sort _)) (Set _) =
   pure $
   s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s'))
 convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = pure True
@@ -109,12 +108,14 @@ convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = pure $ Ntrl t == u
 convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = pure $ t == Ntrl u
 convert t u (Cnstr (Sort s)) (Set k) = pure $ False
 -- In type Pi
-convert t u (Cnstr (Pi s s' a b)) (Set k) = do
-  t <- doApp (weaken 1 t) (point FZ)
-  u <- doApp (weaken 1 u) (point FZ)
+convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
+  t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
+  u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
   convert t u b s'
 -- Default
-convert t u a s = internal $ fillSep ["invalid convert:", prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
+convert t u a s =
+  inScope "invalid conversion:" $ fatal $
+  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
 
 
 -- Typing Contexts -------------------------------------------------------------
@@ -136,89 +137,109 @@ countVars (ctx :< y)  = weaken $ countVars ctx
 countVars (ctx ::< y) = FS $ countVars ctx
 
 index : TyContext m n -> Fin n -> (NormalForm n, NormalForm n, Sort)
-index (ctx :< def)         FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
-index (ctx ::< (_, ty, s)) FZ     = (point FZ, weaken 1 ty, s)
-index (ctx :< _)           (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
-index (ctx ::< _)          (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
+index (ctx :< def)           FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
+index (ctx ::< (var, ty, s)) FZ     = (Ntrl $ Var var FZ, weaken 1 ty, s)
+index (ctx :< _)             (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
+index (ctx ::< _)            (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 
 covering partial
-asSubst : (ctx : TyContext m n) -> Fin n -> Error ann (NormalForm m)
-asSubst (ctx :< def) FZ     = subst def.tm (asSubst ctx)
-asSubst (ctx ::< _)  FZ     = pure $ point FZ
-asSubst (ctx :< def) (FS i) = asSubst ctx i
-asSubst (ctx ::< _)  (FS i) = map (weaken 1) (asSubst ctx i)
+asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m)
+asSubst (ctx :< def)           FZ     = subst def.tm (asSubst ctx)
+asSubst (ctx ::< (var, _, _))  FZ     = pure $ Ntrl $ Var var FZ
+asSubst (ctx :< def)           (FS i) = asSubst ctx i
+asSubst (ctx ::< _)            (FS i) = map (weaken 1) (asSubst ctx i)
 
 -- Checking and Inference ------------------------------------------------------
 
 covering partial
-check : TyContext m n -> Term n -> NormalForm n -> Sort -> Error ann (NormalForm n)
+check : TyContext m n -> Term n -> NormalForm n -> Sort -> Logging ann (NormalForm n)
 covering partial
-infer : TyContext m n -> Term n -> Error ann (NormalForm n, NormalForm n, Sort)
+infer : TyContext m n -> Term n -> Logging ann (NormalForm n, NormalForm n, Sort)
 covering partial
-inferSort : {default "type mismatch" tag : String}
-  -> TyContext m n -> Term n -> Error ann (NormalForm n, Sort)
+inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a}
+  -> TyContext m n -> Term n -> Logging ann (NormalForm n, Sort)
 
-check ctx (Lambda _ var t) (Cnstr (Pi s s' a b)) _ = do
+check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do
+  inScope "check" $ trace $ map (\_ => pretty {ann} "checking under lambda with type" <++> pretty a) (fullBounds tm)
+  inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") (fullBounds tm)
+  inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) (fullBounds tm)
   t <- check (ctx ::< (var, a, s)) t b s'
-  pure (Cnstr $ Lambda t)
-check ctx tm@(Lambda _ _ _) ty _ =
-  report (fullBounds tm).bounds
-    (pretty "type mismatch: expected pi" <+> comma <+> softline <+> "got" <++> pretty ty)
+  pure (Cnstr $ Lambda var t)
+check ctx tm@(Lambda _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "pi") (pretty ty)
 check ctx tm ty s = do
-  let bounds = (fullBounds tm).bounds
+  let bounded = fullBounds tm
+  inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded
   (tm, ty', s') <- infer ctx tm
+  inScope "check" $ trace $ map (\_ => pretty {ann} "inferred type is" <++> pretty ty') bounded
   let True = s == s'
-    | False => report bounds
-      (pretty "sort mismatch: expected" <++> pretty s <+> comma <+> softline <+> "got" <++> pretty s')
+    | False => sortMismatch bounded.bounds (pretty s) (pretty s')
   True <- convert !(subst ty $ asSubst ctx) !(subst ty' $ asSubst ctx) (cast s) (suc s)
-    | False => report bounds
-      (pretty "type mismatch: expected" <++> pretty ty <+> comma <+> softline <+> "got" <++> pretty ty')
+    | False => typeMismatch bounded.bounds (pretty ty) (pretty ty')
+  inScope "check" $ trace $ map (\_ => pretty {ann} "converted" <++> pretty ty' <+> softline <+> pretty "to" <++> pretty ty) bounded
   pure tm
 
-infer ctx (Var b i) = pure $ index ctx i
+infer ctx tm@(Var b i) = do
+  inScope "infer" $ trace $ map (\_ => "encountered variable \{b.val}@\{show i}") (fullBounds tm)
+  let (t, a, s) = index ctx i
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) (fullBounds tm)
+  pure $ (t, a, s)
 infer ctx (Sort b s) = pure $ (cast s, cast (suc s), suc (suc s))
-infer ctx (Pi _ var a b) = do
-  (a, s) <- inferSort ctx a
-  let aDef = MkDefinition {name = var, sort = suc s, ty = cast s, tm = a}
-  (b, s') <- inferSort (ctx :< aDef) b
-  pure (Cnstr (Pi s s' a b), cast (s ~> s'), suc (s ~> s'))
-infer ctx tm@(Lambda _ _ _) = report (fullBounds tm).bounds (pretty "cannot infer type:" <+> softline <+> pretty tm)
-infer ctx (App t u) = do
-  let bounds = (fullBounds t).bounds
-  (t, Cnstr (Pi s s' a b), _) <- infer ctx t
-    | (_, t, _) => report bounds (pretty "wrong type to apply:" <+> softline <+> pretty t)
+infer ctx tm@(Pi _ var a b) = do
+  inScope "infer" $ trace $ map (\_ => "encountered Pi type") (fullBounds tm)
+  (a, s) <- inferType ctx a
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "argument has type" <++> pretty a) (fullBounds tm)
+  (b, s') <- inferType (ctx ::< (var, a, s)) b
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "result has type" <++> pretty b <+> comma <+> softline <+> pretty "so Pi type has type" <++> pretty (s ~> s')) (fullBounds tm)
+  pure (Cnstr (Pi s s' var a b), cast (s ~> s'), suc (s ~> s'))
+infer ctx tm@(Lambda _ _ _) = inScope "cannot infer type" $ fatal (fullBounds tm)
+infer ctx tm@(App t u) = do
+  inScope "infer" $ trace $ map (\_ => "encountered application") (fullBounds tm)
+  let bounded = fullBounds t
+  (t, ty@(Cnstr (Pi s s' _ a b)), _) <- infer ctx t
+    | (_, t, _) => inScope "wrong type to apply" $ fatal (map (\_ => t) bounded)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "function has type" <++> pretty ty) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "checking argument has type" <++> pretty a) (fullBounds tm)
   u <- check ctx u a s
+  inScope "infer" $ trace $ map (\_ => "argument is well typed") (fullBounds tm)
   res <- doApp t u
-  ty <- subst1 t b
+  ty <- subst1 u b
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) (fullBounds tm)
   pure (res, ty, s')
 infer ctx (Top b) = pure $ (Cnstr Top, cast Prop, Set 0)
 infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
 infer ctx (Bottom b) = pure $ (Cnstr Bottom, cast Prop, Set 0)
-infer ctx (Absurd b a t) = do
-  (a, s) <- inferSort ctx a
+infer ctx tm@(Absurd b a t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered absurd") (fullBounds tm)
+  (a, s) <- inferType ctx a
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "will fudge to type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "checking for proof of false") (fullBounds tm)
   _ <- check ctx t (Cnstr Bottom) Prop
+  inScope "infer" $ trace $ map (\_ => "proof of false is well typed") (fullBounds tm)
   pure (Ntrl Absurd, a, s)
 
-inferSort ctx a = do
+inferType ctx a = do
   (a, Cnstr (Sort s), _) <- infer ctx a
-    | (_, ty, _) => report (fullBounds a).bounds
-      (pretty "\{tag}: expected sort" <+> comma <+> softline <+> "got" <++> pretty ty)
+    | (_, ty, _) => tag (fullBounds a).bounds (pretty "sort") (pretty ty)
   pure (a, s)
 
 -- Checking Definitions and Blocks ---------------------------------------------
 
 covering partial
-checkDef : Context n -> Term.Definition n -> Error ann (NormalForm.Definition n)
+checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n)
 checkDef ctx def = do
   let tyBounds = (fullBounds def.ty).bounds
   let tmBounds = (fullBounds def.tm).bounds
-  (ty, sort) <- inferSort {tag = "invalid declaration"} (fromContext ctx) def.ty
+  (ty, sort) <-
+    inferType {tag = \bounds, lhs, rhs => inScope "invalid declaration" $ mismatch bounds lhs rhs}
+      (fromContext ctx) def.ty
+  inScope "check" $ debug (pretty {ann} "\{def.name} has type" <++> pretty ty)
   tm <- check (fromContext ctx) def.tm ty sort
+  inScope "check" $ debug (pretty {ann} "\{def.name} is well typed with value" <++> pretty tm)
   pure $ MkDefinition {name = def.name, ty, tm, sort}
 
 covering partial
 export
-checkBlock : Block n -> Error ann (Context n)
+checkBlock : Block n -> Logging ann (Context n)
 checkBlock [] = pure []
 checkBlock (blk :< def) = do
   ctx <- checkBlock blk