diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
new file mode 100644
index 0000000..4d2491b
--- /dev/null
+++ b/src/Quox/Error.idr
@@ -0,0 +1,335 @@
+module Quox.Error
+
+import Control.Monad.Identity
+import Control.Monad.Trans
+import Control.Monad.Reader
+import Control.Monad.Writer
+import Control.Monad.State
+import Control.Monad.RWS
+
+%default total
+
+
+public export
+data Elem : a -> List a -> Type where
+  Here  : x `Elem` (x :: xs)
+  There : x `Elem` xs -> x `Elem` (y :: xs)
+%builtin Natural Elem
+
+export
+Uninhabited (x `Elem` []) where
+  uninhabited Here      impossible
+  uninhabited (There _) impossible
+
+
+public export
+data Spine : List a -> Type where
+  NIL  : Spine []
+  CONS : Spine xs -> Spine (x :: xs)
+%builtin Natural Spine
+
+
+public export
+record OneOf types where
+  constructor One
+  elem    : type `Elem` types
+  1 value : type
+
+export
+Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
+
+
+export %inline
+inj : ty `Elem` tys => ty -> OneOf tys
+inj value = One %search value
+
+public export
+All : (Type -> Type) -> List Type -> Type
+All p []      = ()
+All p (x::xs) = (p x, All p xs)
+
+
+private
+eq : All Eq types => OneOf types -> OneOf types -> Bool
+eq (One Here      x) (One Here      y) = x == y
+eq (One (There p) x) (One (There q) y) = eq (One p x) (One q y)
+eq (One Here      _) (One (There _) _) = False
+eq (One (There z) x) (One Here      y) = False
+
+export
+All Eq types => Eq (OneOf types) where (==) = eq
+
+
+private
+ordsToEqs : Spine types => All Ord types => All Eq types
+ordsToEqs @{NIL}     = ()
+ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
+
+private
+[eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
+  (==) = eq @{ordsToEqs}
+
+
+private
+cmp : All Ord types => OneOf types -> OneOf types -> Ordering
+cmp (One Here      x) (One Here      y) = compare x y
+cmp (One Here      _) (One (There _) _) = LT
+cmp (One (There _) _) (One Here      _) = GT
+cmp (One (There p) x) (One (There q) y) = cmp (One p x) (One q y)
+
+export
+(Spine types, All Ord types) => Ord (OneOf types) using eqOrds where
+  compare = cmp
+
+
+export
+All Show types => Show (OneOf types) where
+  showPrec d (One Here      value) = showPrec d value
+  showPrec d (One (There p) value) = showPrec d $ One p value
+
+
+public export
+record ErrorT (errs : List Type) (m : Type -> Type) (res : Type) where
+  constructor MkErrorT
+  runErrorT : m (Either (OneOf errs) res)
+
+public export
+Error : List Type -> Type -> Type
+Error errs = ErrorT errs Identity
+
+export
+runError : Error errs a -> Either (OneOf errs) a
+runError = runIdentity . runErrorT
+
+
+export %inline
+Functor m => Functor (ErrorT errs m) where
+  map f (MkErrorT act) = MkErrorT $ map (map f) act
+
+export %inline
+Applicative m => Applicative (ErrorT errs m) where
+  pure = MkErrorT . pure . pure
+  MkErrorT mf <*> MkErrorT mx = MkErrorT [|mf <*> mx|]
+
+export %inline
+Monad m => Monad (ErrorT errs m) where
+  MkErrorT act >>= k = MkErrorT $ act >>= either (pure . Left) (runErrorT . k)
+
+
+private
+without' : (xs : List a) -> x `Elem` xs -> List a
+without' (_ :: xs) Here      = xs
+without' (y :: xs) (There p) = y :: without' xs p
+
+infix 9 `without`
+export %inline
+without : (xs : List a) -> (x : a) -> x `Elem` xs => List a
+xs `without` x = without' {x} xs %search
+
+
+private
+get' : err `Elem` errs -> OneOf errs -> Either err (OneOf (errs `without` err))
+get' Here      (One Here      x) = Left x
+get' Here      (One (There p) x) = Right (One p x)
+get' (There y) (One Here      x) = Right (One Here x)
+get' (There y) (One (There p) x) = mapSnd {elem $= There} $ get' y (One p x)
+
+export %inline
+get : (0 err : Type) -> err `Elem` errs =>
+      OneOf errs -> Either err (OneOf (errs `without` err))
+get _ = get' %search
+
+
+export %inline
+noErrorsT : Monad m => ErrorT [] m a -> m a
+noErrorsT (MkErrorT act) = act >>= either absurd pure
+
+export %inline
+noErrors : Error [] a -> a
+noErrors = runIdentity . noErrorsT
+
+
+public export
+data Embed : List a -> List a -> Type where
+  Nil  : Embed [] ys
+  (::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
+
+
+private
+embedElem' : Embed xs ys -> x `Elem` xs -> x `Elem` ys
+embedElem' (e :: _)  Here      = e
+embedElem' (_ :: es) (There p) = embedElem' es p
+
+export %inline
+embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
+embedElem = embedElem' %search
+
+
+export %inline
+(<|>) : Applicative m => ErrorT errs m a -> ErrorT errs m a -> ErrorT errs m a
+MkErrorT act1 <|> MkErrorT act2 = MkErrorT [|act1 `or` act2|] where
+  or : Either l r -> Either l r -> Either l r
+  one `or` two = case one of Left err => two; Right x => pure x
+
+
+public export
+interface Monad m => MonadThrow errs m | m where
+  throw : err `Elem` errs => err -> m a
+
+public export
+interface
+  (MonadThrow errs1 m1,
+   MonadThrow errs2 m2,
+   err `Elem` errs1) =>
+  MonadCatch err errs1 errs2 m1 m2
+    | err, m1
+where
+  catch : (act : m1 a) -> (catch : err -> m2 a) -> m2 a
+
+public export
+interface
+  (MonadThrow errs1 m1,
+   MonadThrow errs2 m2,
+   Embed errs1 errs2) =>
+  MonadEmbed errs1 errs2 m1 m2
+    | m1, m2
+where
+  embed : m1 a -> m2 a
+
+
+export %inline
+implementation
+  Monad m =>
+  MonadThrow errs (ErrorT errs m)
+where
+  throw = MkErrorT . pure . Left . inj
+
+export %inline
+implementation
+  (Monad m, err `Elem` errs) =>
+  MonadCatch err errs (errs `without` err)
+    (ErrorT errs m)
+    (ErrorT (errs `without` err) m)
+where
+  catch (MkErrorT act) handler = MkErrorT $
+    act <&> mapFst (get err) >>= \case
+      Left (Left  this)  => runErrorT $ handler this
+      Left (Right other) => pure $ Left other
+      Right ok           => pure $ Right ok
+
+export %inline
+implementation
+  (Monad m, Embed errs1 errs2) =>
+  MonadEmbed errs1 errs2 (ErrorT errs1 m) (ErrorT errs2 m)
+where
+  embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
+
+
+export %inline
+MonadTrans (ErrorT errs) where lift = MkErrorT . map Right
+
+export %inline
+MonadReader r m => MonadReader r (ErrorT errs m) where
+  local f (MkErrorT act) = MkErrorT $ local f act
+  ask = lift ask
+
+export %inline
+MonadWriter w m => MonadWriter w (ErrorT errs m) where
+  tell = MkErrorT . map Right . tell
+
+  pass (MkErrorT act) = MkErrorT $ pass $ do
+    Right (res, f) <- act
+        | Left err => pure (Left err, id)
+    pure (Right res, f)
+
+  listen (MkErrorT act) = MkErrorT $ do
+    (res, x) <- listen act
+    pure $ mapSnd (,x) res
+
+export %inline
+MonadState s m => MonadState s (ErrorT errs m) where
+  get   = lift get
+  put   = lift . put
+  state = lift . state
+
+export %inline
+MonadRWS r w s m => MonadRWS r w s (ErrorT errs m) where
+
+export %inline
+HasIO m => HasIO (ErrorT errs m) where
+  liftIO = MkErrorT . map Right . liftIO
+
+
+export %inline
+MonadThrow errs m => MonadThrow errs (ReaderT r m) where throw = lift . throw
+
+export %inline
+MonadThrow errs m => MonadThrow errs (WriterT w m) where throw = lift . throw
+
+export %inline
+MonadThrow errs m => MonadThrow errs (StateT s m) where throw = lift . throw
+
+export %inline
+MonadThrow errs m => MonadThrow errs (RWST r w s m) where throw = lift . throw
+
+
+export %inline
+implementation
+  MonadCatch err errs1 errs2 m1 m2 =>
+  MonadCatch err errs1 errs2 (ReaderT r m1) (ReaderT r m2)
+where
+  catch (MkReaderT act) handler = MkReaderT $ \r =>
+    act r `catch` runReaderT r . handler
+
+export %inline
+implementation
+  MonadCatch err errs1 errs2 m1 m2 =>
+  MonadCatch err errs1 errs2 (WriterT w m1) (WriterT w m2)
+where
+  catch (MkWriterT act) handler = MkWriterT $ \w =>
+    act w `catch` \e => unWriterT (handler e) w
+
+export %inline
+implementation
+  MonadCatch err errs1 errs2 m1 m2 =>
+  MonadCatch err errs1 errs2 (StateT s m1) (StateT s m2)
+where
+  catch (ST act) handler = ST $ \s =>
+    act s `catch` \e => runStateT' (handler e) s
+
+export %inline
+implementation
+  MonadCatch err errs1 errs2 m1 m2 =>
+  MonadCatch err errs1 errs2 (RWST r w s m1) (RWST r w s m2)
+where
+  catch (MkRWST act) handler = MkRWST $ \r, s, w =>
+    act r s w `catch` \e => unRWST (handler e) r s w
+
+
+export %inline
+implementation
+  MonadEmbed errs1 errs2 m1 m2 =>
+  MonadEmbed errs1 errs2 (ReaderT r m1) (ReaderT r m2)
+where
+  embed (MkReaderT act) = MkReaderT $ embed . act
+
+export %inline
+implementation
+  MonadEmbed errs1 errs2 m1 m2 =>
+  MonadEmbed errs1 errs2 (WriterT w m1) (WriterT w m2)
+where
+  embed (MkWriterT act) = MkWriterT $ embed . act
+
+export %inline
+implementation
+  MonadEmbed errs1 errs2 m1 m2 =>
+  MonadEmbed errs1 errs2 (StateT s m1) (StateT s m2)
+where
+  embed (ST act) = ST $ embed . act
+
+export %inline
+implementation
+  MonadEmbed errs1 errs2 m1 m2 =>
+  MonadEmbed errs1 errs2 (RWST r w s m1) (RWST r w s m2)
+where
+  embed (MkRWST act) = MkRWST $ \r, s, w => embed $ act r s w