diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index bfc726c..6eb081e 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -1,36 +1,14 @@
 module Quox.Typing
 
+import public Quox.Typing.Context as Typing
+import public Quox.Typing.EqMode as Typing
+import public Quox.Typing.Error as Typing
+
 import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Reduce
 
-import public Data.SortedMap
-import public Control.Monad.Either
-import Derive.Prelude
-
-%hide TT.Name
 %default total
-%language ElabReflection
-
-%default total
-
-
-public export
-TContext : Type -> Nat -> Nat -> Type
-TContext q d = Context (Term q d)
-
-public export
-QOutput : Type -> Nat -> Type
-QOutput = Context'
-
-
-public export
-record TyContext q d n where
-  constructor MkTyContext
-  dctx : DimEq d
-  tctx : TContext q d n
-
-%name TyContext ctx
 
 
 namespace TContext
@@ -99,105 +77,6 @@ InferResult : DimEq d -> TermLike
 InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n
 
 
-public export
-data EqMode = Equal | Sub | Super
-%runElab derive "EqMode" [Eq, Ord, Show]
-
-
-public export
-data Error q
-= ExpectedTYPE (Term q d n)
-| ExpectedPi   (Term q d n)
-| ExpectedSig  (Term q d n)
-| ExpectedEnum (Term q d n)
-| ExpectedEq   (Term q d n)
-| BadUniverse  Universe Universe
-| TagNotIn     TagVal (SortedSet TagVal)
-| BadCaseQtys  (List (QOutput q n))
-
--- first arg of ClashT is the type
-| ClashT  EqMode (Term q d n) (Term q d n) (Term q d n)
-| ClashTy EqMode (Term q d n) (Term q d n)
-| ClashE  EqMode (Elim q d n) (Elim q d n)
-| ClashU  EqMode Universe     Universe
-| ClashQ        q            q
-| ClashD        (Dim d)      (Dim d)
-| NotInScope    Name
-
-| NotType (Term q d n)
-| WrongType (Term q d n) (Term q d n) (Term q d n)
-
--- extra context
-| WhileChecking
-    (TyContext q d n) q
-    (Term q d n) -- term
-    (Term q d n) -- type
-    (Error q)
-| WhileCheckingTy
-    (TyContext q d n)
-    (Term q d n)
-    (Maybe Universe)
-    (Error q)
-| WhileInferring
-    (TyContext q d n) q
-    (Elim q d n)
-    (Error q)
-| WhileComparingT
-    (TyContext q d n) EqMode
-    (Term q d n) -- type
-    (Term q d n) (Term q d n) -- lhs/rhs
-    (Error q)
-| WhileComparingE
-    (TyContext q d n) EqMode
-    (Elim q d n) (Elim q d n)
-    (Error q)
-
-| WhnfError WhnfError
-
-
-public export
-0 HasErr : Type -> (Type -> Type) -> Type
-HasErr q = MonadError (Error q)
-
-export %inline
-wrapErr : HasErr q m => (Error q -> Error q) -> m a -> m a
-wrapErr f act = catchError act $ throwError . f
-
-export %inline
-ucmp : EqMode -> Universe -> Universe -> Bool
-ucmp Equal = (==)
-ucmp Sub   = (<=)
-ucmp Super = (>=)
-
-export %inline
-flip : EqMode -> EqMode
-flip Equal = Equal
-flip Sub   = Super
-flip Super = Sub
-
-
-parameters {auto _ : HasErr q m}
-  export %inline
-  expect : Eq a => (a -> a -> Error q) -> (a -> a -> Bool) -> a -> a -> m ()
-  expect err cmp x y = unless (x `cmp` y) $ throwError $ err x y
-
-  export %inline
-  expectEqualQ : Eq q => q -> q -> m ()
-  expectEqualQ = expect ClashQ (==)
-
-  export %inline
-  expectCompatQ : IsQty q => q -> q -> m ()
-  expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
-
-  export %inline
-  expectModeU : EqMode -> Universe -> Universe -> m ()
-  expectModeU mode = expect (ClashU mode) $ ucmp mode
-
-  export %inline
-  expectEqualD : Dim d -> Dim d -> m ()
-  expectEqualD = expect ClashD (==)
-
-
 export
 lookupFree' : HasErr q m => Definitions' q g -> Name -> m (Definition' q g)
 lookupFree' defs x =
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
new file mode 100644
index 0000000..6538de2
--- /dev/null
+++ b/lib/Quox/Typing/Context.idr
@@ -0,0 +1,22 @@
+module Quox.Typing.Context
+
+import Quox.Syntax
+import Quox.Context
+
+
+public export
+TContext : Type -> Nat -> Nat -> Type
+TContext q d = Context (Term q d)
+
+public export
+QOutput : Type -> Nat -> Type
+QOutput = Context'
+
+
+public export
+record TyContext q d n where
+  constructor MkTyContext
+  dctx : DimEq d
+  tctx : TContext q d n
+
+%name TyContext ctx
diff --git a/lib/Quox/Typing/EqMode.idr b/lib/Quox/Typing/EqMode.idr
new file mode 100644
index 0000000..5e3c93a
--- /dev/null
+++ b/lib/Quox/Typing/EqMode.idr
@@ -0,0 +1,22 @@
+module Quox.Typing.EqMode
+
+import Quox.Syntax
+import Derive.Prelude
+%language ElabReflection
+%default total
+
+public export
+data EqMode = Equal | Sub | Super
+%runElab derive "EqMode" [Eq, Ord, Show]
+
+export %inline
+ucmp : EqMode -> Universe -> Universe -> Bool
+ucmp Equal = (==)
+ucmp Sub   = (<=)
+ucmp Super = (>=)
+
+export %inline
+flip : EqMode -> EqMode
+flip Equal = Equal
+flip Sub   = Super
+flip Super = Sub
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
new file mode 100644
index 0000000..1e5fe90
--- /dev/null
+++ b/lib/Quox/Typing/Error.idr
@@ -0,0 +1,142 @@
+module Quox.Typing.Error
+
+import Quox.Syntax
+import Quox.Reduce
+import Quox.Typing.Context
+import Quox.Typing.EqMode
+import Quox.Pretty
+
+import Data.List
+import public Control.Monad.Either
+
+
+public export
+data Error q
+= ExpectedTYPE (Term q d n)
+| ExpectedPi   (Term q d n)
+| ExpectedSig  (Term q d n)
+| ExpectedEnum (Term q d n)
+| ExpectedEq   (Term q d n)
+| BadUniverse  Universe Universe
+| TagNotIn     TagVal (SortedSet TagVal)
+| BadCaseQtys  (List (QOutput q n))
+
+-- first arg of ClashT is the type
+| ClashT  EqMode (Term q d n) (Term q d n) (Term q d n)
+| ClashTy EqMode (Term q d n) (Term q d n)
+| ClashE  EqMode (Elim q d n) (Elim q d n)
+| ClashU  EqMode Universe     Universe
+| ClashQ        q            q
+| ClashD        (Dim d)      (Dim d)
+| NotInScope    Name
+
+| NotType (Term q d n)
+| WrongType (Term q d n) (Term q d n) (Term q d n)
+
+-- extra context
+| WhileChecking
+    (TyContext q d n) q
+    (Term q d n) -- term
+    (Term q d n) -- type
+    (Error q)
+| WhileCheckingTy
+    (TyContext q d n)
+    (Term q d n)
+    (Maybe Universe)
+    (Error q)
+| WhileInferring
+    (TyContext q d n) q
+    (Elim q d n)
+    (Error q)
+| WhileComparingT
+    (TyContext q d n) EqMode
+    (Term q d n) -- type
+    (Term q d n) (Term q d n) -- lhs/rhs
+    (Error q)
+| WhileComparingE
+    (TyContext q d n) EqMode
+    (Elim q d n) (Elim q d n)
+    (Error q)
+
+| WhnfError WhnfError
+%name Error err
+
+public export
+0 HasErr : Type -> (Type -> Type) -> Type
+HasErr q = MonadError (Error q)
+
+
+||| whether the error is surrounded in some context
+||| (e.g. "while checking s : A, …")
+public export
+isErrorContext : Error q -> Bool
+isErrorContext (WhileChecking   {}) = True
+isErrorContext (WhileCheckingTy {}) = True
+isErrorContext (WhileInferring  {}) = True
+isErrorContext (WhileComparingT {}) = True
+isErrorContext (WhileComparingE {}) = True
+isErrorContext _                    = False
+
+||| remove one layer of context
+export
+peelContext : (e : Error q) -> (0 _ : So (isErrorContext e)) =>
+              (Error q -> Error q, Error q)
+peelContext (WhileChecking ctx x s t err) =
+  (WhileChecking ctx x s t, err)
+peelContext (WhileCheckingTy ctx s k err) =
+  (WhileCheckingTy ctx s k, err)
+peelContext (WhileInferring ctx x e err) =
+  (WhileInferring ctx x e, err)
+peelContext (WhileComparingT ctx x s t r err) =
+  (WhileComparingT ctx x s t r, err)
+peelContext (WhileComparingE ctx x e f err) =
+  (WhileComparingE ctx x e f, err)
+
+||| separates out all the error context layers
+||| (e.g. "while checking s : A, …")
+export
+explodeContext : Error q -> (List (Error q -> Error q), Error q)
+explodeContext err =
+  case choose $ isErrorContext err of
+    Left y =>
+      let (f,  inner) = peelContext err
+          (fs, root)  = explodeContext $ assert_smaller err inner in
+      (f :: fs, root)
+    Right n => ([], err)
+
+||| leaves the outermost context layer, and the innermost (up to) n, and removes
+||| the rest if there are more than n+1 in total
+export
+trimContext : Nat -> Error q -> Error q
+trimContext n err =
+  case explodeContext err of
+    ([],      err) => err
+    (f :: fs, err) => f $ foldr apply err $ takeEnd n fs
+where
+  takeEnd : Nat -> List a -> List a
+  takeEnd n = reverse . take n . reverse
+
+
+export %inline
+wrapErr : MonadError e m => (e -> e) -> m a -> m a
+wrapErr f act = catchError act $ throwError . f
+
+expect : MonadError e m => (a -> a -> e) -> (a -> a -> Bool) -> a -> a -> m ()
+expect err cmp x y = unless (x `cmp` y) $ throwError $ err x y
+
+parameters {auto _ : HasErr q m}
+  export %inline
+  expectEqualQ : Eq q => q -> q -> m ()
+  expectEqualQ = expect ClashQ (==)
+
+  export %inline
+  expectCompatQ : IsQty q => q -> q -> m ()
+  expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
+
+  export %inline
+  expectModeU : EqMode -> Universe -> Universe -> m ()
+  expectModeU mode = expect (ClashU mode) $ ucmp mode
+
+  export %inline
+  expectEqualD : Dim d -> Dim d -> m ()
+  expectEqualD = expect ClashD (==)
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index c5e851b..7502bb8 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -31,6 +31,9 @@ modules =
   Quox.Context,
   Quox.Equal,
   Quox.Name,
+  Quox.Typing.Context,
+  Quox.Typing.EqMode,
+  Quox.Typing.Error,
   Quox.Typing,
   Quox.Typechecker,
   Quox.Parser.Lexer,