From 36609713acc6b557cad077252bdc43e036283c67 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 31 Mar 2023 19:23:30 +0200
Subject: [PATCH] =?UTF-8?q?mtl=20=E2=87=92=20eff?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Quox/Definition.idr        |  11 +-
 lib/Quox/EffExtra.idr          | 102 ++++++++++++++++++
 lib/Quox/Equal.idr             | 136 ++++++++++++------------
 lib/Quox/Parser/FromParser.idr | 189 ++++++++++++++++++++-------------
 lib/Quox/Typechecker.idr       |  72 +++++++------
 lib/Quox/Typing.idr            |  71 +++++++------
 lib/Quox/Typing/Error.idr      |  24 ++---
 lib/quox-lib.ipkg              |   3 +-
 8 files changed, 382 insertions(+), 226 deletions(-)
 create mode 100644 lib/Quox/EffExtra.idr

diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 51e73c2..c410fa2 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -3,7 +3,7 @@ module Quox.Definition
 import public Quox.No
 import public Quox.Syntax
 import public Data.SortedMap
-import public Control.Monad.Reader
+import Control.Eff
 import Decidable.Decidable
 
 
@@ -79,13 +79,12 @@ Definitions q = Definitions' q IsGlobal
 
 
 public export
-0 HasDefs' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
-HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal)
+0 DefsReader' : (q : Type) -> (q -> Type) -> Type -> Type
+DefsReader' q isGlobal = Reader (Definitions' q isGlobal)
 
 public export
-0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type
-HasDefs q = HasDefs' q IsGlobal
-
+0 DefsReader : (q : Type) -> IsQty q => Type -> Type
+DefsReader q = DefsReader' q IsGlobal
 
 public export %inline
 lookupElim : forall isGlobal. {d, n : Nat} ->
diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr
new file mode 100644
index 0000000..e80a922
--- /dev/null
+++ b/lib/Quox/EffExtra.idr
@@ -0,0 +1,102 @@
+module Quox.EffExtra
+
+import public Control.Eff
+
+import Data.IORef
+
+
+export
+localAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
+          (s -> s) -> Eff fs a -> Eff fs a
+localAt lbl f act = do
+  old <- getAt lbl
+  modifyAt lbl f *> act <* putAt lbl old
+
+export %inline
+localAt_ : (0 lbl : tag) -> Has (StateL lbl s) fs =>
+           s -> Eff fs a -> Eff fs a
+localAt_ lbl x = localAt lbl $ const x
+
+export %inline
+local : Has (State s) fs => (s -> s) -> Eff fs a -> Eff fs a
+local = localAt ()
+
+export %inline
+local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a
+local_ = localAt_ ()
+
+
+export
+hasDrop : (0 neq : Not (a = b)) ->
+          (ha : Has a fs) => (hb : Has b fs) =>
+          Has a (drop fs hb)
+hasDrop neq {ha = Z}    {hb = Z}    = void $ neq Refl
+hasDrop neq {ha = S ha} {hb = Z}    = ha
+hasDrop neq {ha = Z}    {hb = S hb} = Z
+hasDrop neq {ha = S ha} {hb = S hb} = S $ hasDrop neq {ha, hb}
+
+private
+0 ioNotState : Not (IO = StateL _ _)
+ioNotState Refl impossible
+
+export
+runStateIORefAt : (0 lbl : tag) -> (Has IO fs, Has (StateL lbl s) fs) =>
+                  IORef s -> Eff fs a -> Eff (fs - StateL lbl s) a
+runStateIORefAt lbl ref act = do
+  let hh : Has IO (fs - StateL lbl s) := hasDrop ioNotState
+  (val, st) <- runStateAt lbl !(readIORef ref) act
+  writeIORef ref st $> val
+
+export %inline
+runStateIORef : (Has IO fs, Has (State s) fs) =>
+                IORef s -> Eff fs a -> Eff (fs - State s) a
+runStateIORef = runStateIORefAt ()
+
+
+export %inline
+evalStateAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
+              s -> Eff fs a -> Eff (fs - StateL lbl s) a
+evalStateAt lbl s act = map fst $ runStateAt lbl s act
+
+export %inline
+evalState : Has (State s) fs => s -> Eff fs a -> Eff (fs - State s) a
+evalState = evalStateAt ()
+
+
+
+public export
+data Length : List a -> Type where
+  Z : Length []
+  S : Length xs -> Length (x :: xs)
+
+export
+subsetWith : Length xs => (forall z. Has z xs -> Has z ys) ->
+             Subset xs ys
+subsetWith @{Z}     f = []
+subsetWith @{S len} f = f Z :: subsetWith (f . S)
+
+export
+subsetSelf : Length xs => Subset xs xs
+subsetSelf = subsetWith id
+
+export
+subsetTail : Length xs => Subset xs (x :: xs)
+subsetTail = subsetWith S
+
+
+-- [fixme] allow the error to be anywhere in the effect list
+export
+wrapErrAt : Length fs => (0 lbl : tag) -> (e -> e) ->
+            Eff (ExceptL lbl e :: fs) a -> Eff (ExceptL lbl e :: fs) a
+wrapErrAt lbl f act =
+  rethrowAt lbl . mapFst f =<< lift @{subsetTail} (runExceptAt lbl act)
+
+export %inline
+wrapErr : Length fs => (e -> e) ->
+          Eff (Except e :: fs) a -> Eff (Except e :: fs) a
+wrapErr = wrapErrAt ()
+
+
+export %inline
+runIO : (MonadRec io, HasIO io) => Eff [IO] a -> io a
+runIO act = runEff act [liftIO]
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 4ef63c4..2a272bf 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -2,49 +2,46 @@ module Quox.Equal
 
 import Quox.BoolExtra
 import public Quox.Typing
-import public Control.Monad.Either
-import public Control.Monad.Reader
 import Data.Maybe
+import Quox.EffExtra
 
 %default total
 
 
 public export
-record CmpContext where
-  constructor MkCmpContext
-  mode : EqMode
-
+0 EqModeState : Type -> Type
+EqModeState = State EqMode
 
 public export
-0 HasCmpContext : (Type -> Type) -> Type
-HasCmpContext = MonadReader CmpContext
+0 EqualEff : Type -> List (Type -> Type)
+EqualEff q = [ErrorEff q, EqModeState]
 
 public export
-0 CanEqual : (q : Type) -> (Type -> Type) -> Type
-CanEqual q m = (HasErr q m, HasCmpContext m)
+0 EqualE : Type -> Type -> Type
+EqualE q = Eff $ EqualEff q
 
 
+export %inline
+mode : Has EqModeState fs => Eff fs EqMode
+mode = get
 
-private %inline
-mode : HasCmpContext m => m EqMode
-mode = asks mode
 
-parameters {auto _ : CanEqual q m} (ctx : EqContext q n)
+parameters (ctx : EqContext q n)
   private %inline
-  clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> m a
-  clashT ty s t = throwError $ ClashT ctx !mode ty s t
+  clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> EqualE q a
+  clashT ty s t = throw $ ClashT ctx !mode ty s t
 
   private %inline
-  clashTy : Term q 0 n -> Term q 0 n -> m a
-  clashTy s t = throwError $ ClashTy ctx !mode s t
+  clashTy : Term q 0 n -> Term q 0 n -> EqualE q a
+  clashTy s t = throw $ ClashTy ctx !mode s t
 
   private %inline
-  clashE : Elim q 0 n -> Elim q 0 n -> m a
-  clashE e f = throwError $ ClashE ctx !mode e f
+  clashE : Elim q 0 n -> Elim q 0 n -> EqualE q a
+  clashE e f = throw $ ClashE ctx !mode e f
 
   private %inline
-  wrongType : Term q 0 n -> Term q 0 n -> m a
-  wrongType ty s = throwError $ WrongType ctx ty s
+  wrongType : Term q 0 n -> Term q 0 n -> EqualE q a
+  wrongType ty s = throw $ WrongType ctx ty s
 
 
 ||| true if a term is syntactically a type, or is neutral.
@@ -105,10 +102,11 @@ parameters (defs : Definitions' q g)
   |||   boundary separation.
   ||| * an enum type is a subsingleton if it has zero or one tags.
   public export covering
-  isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool
-  isSubSing ty = do
-    Element ty nc <- whnfT defs ty
-    case ty of
+  isSubSing : Has (ErrorEff q) fs =>
+              {n : Nat} -> Term q 0 n -> Eff fs Bool
+  isSubSing ty0 = do
+    Element ty0 nc <- whnfT defs ty0
+    case ty0 of
       TYPE _          => pure False
       Pi   {res, _}   => isSubSing res.term
       Lam  {}         => pure False
@@ -128,13 +126,14 @@ parameters (defs : Definitions' q g)
 
 
 export
-ensureTyCon : HasErr q m =>
-              (ctx : EqContext q n) -> (t : Term q 0 n) -> m (So (isTyCon t))
+ensureTyCon : Has (ErrorEff q) fs =>
+              (ctx : EqContext q n) -> (t : Term q 0 n) ->
+              Eff fs (So (isTyCon t))
 ensureTyCon ctx t = case nchoose $ isTyCon t of
   Left  y => pure y
-  Right n => throwError $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
+  Right n => throw $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
 
-parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
+parameters (defs : Definitions' q _) {auto _ : IsQty q}
   mutual
     namespace Term
       ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
@@ -142,7 +141,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       |||
       ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
       export covering %inline
-      compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> m ()
+      compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> EqualE q ()
       compare0 ctx ty s t =
         wrapErr (WhileComparingT ctx !mode ty s t) $ do
           let Val n = ctx.termLen
@@ -163,10 +162,10 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
                   (ty, s, t : Term q 0 n) ->
                   (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
                   (0 ns  : NotRedex defs s)  => (0 nt  : NotRedex defs t) =>
-                  m ()
+                  EqualE q ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
 
-      compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local {mode := Equal} $
+      compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local_ Equal $
         case (s, t) of
           --           Γ, x : A ⊢ s = t : B
           -- -------------------------------------------
@@ -188,11 +187,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           ctx' : EqContext q (S n)
           ctx' = extendTy qty res.name arg ctx
 
-          eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
+          eta : Elim q 0 n -> ScopeTerm q 0 n -> EqualE q ()
           eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
           eta e (S _ (N _)) = clashT ctx ty s t
 
-      compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
+      compare0' ctx ty@(Sig {fst, snd, _}) s t = local_ Equal $
         case (s, t) of
           --  Γ ⊢ s₁ = t₁ : A     Γ ⊢ s₂ = t₂ : B{s₁/x}
           -- --------------------------------------------
@@ -212,7 +211,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           (E _,     t) => wrongType ctx ty t
           (s,       _) => wrongType ctx ty s
 
-      compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $
+      compare0' ctx ty@(Enum tags) s t = local_ Equal $
         case (s, t) of
           -- --------------------
           --  Γ ⊢ `t = `t : {ts}
@@ -234,7 +233,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
         -- Γ ⊢ e = f : Eq [i ⇒ A] s t
         pure ()
 
-      compare0' ctx Nat s t = local {mode := Equal} $
+      compare0' ctx Nat s t = local_ Equal $
         case (s, t) of
           -- ---------------
           --  Γ ⊢ 0 = 0 : ℕ
@@ -259,7 +258,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           (E _,    t) => wrongType ctx Nat t
           (s,      _) => wrongType ctx Nat s
 
-      compare0' ctx ty@(BOX q ty') s t = local {mode := Equal} $
+      compare0' ctx ty@(BOX q ty') s t = local_ Equal $
         case (s, t) of
           --     Γ ⊢ s = t : A
           -- -----------------------
@@ -282,7 +281,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
     ||| compares two types, using the current variance `mode` for universes.
     ||| fails if they are not types, even if they would happen to be equal.
     export covering %inline
-    compareType : EqContext q n -> (s, t : Term q 0 n) -> m ()
+    compareType : EqContext q n -> (s, t : Term q 0 n) -> EqualE q ()
     compareType ctx s t = do
       let Val n = ctx.termLen
       Element s ns <- whnfT defs s
@@ -298,7 +297,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
                    (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
                    (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
                    (0 st : So (sameTyCon s t)) =>
-                   m ()
+                   EqualE q ()
     -- equality is the same as subtyping, except with the
     -- "≤" in the TYPE rule being replaced with "="
     compareType' ctx (TYPE k) (TYPE l) =
@@ -313,7 +312,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       -- ----------------------------------------
       --  Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
       expectEqualQ sQty tQty
-      local {mode $= flip} $ compareType ctx sArg tArg -- contra
+      local flip $ compareType ctx sArg tArg -- contra
       compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term
 
     compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
@@ -332,7 +331,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
       compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
       compareType (extendDim sTy.name One  ctx) sTy.one  tTy.one
-      local {mode := Equal} $ do
+      local_ Equal $ do
         Term.compare0 ctx sTy.zero sl tl
         Term.compare0 ctx sTy.one  sr tr
 
@@ -364,7 +363,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
     private covering
     computeElimType : EqContext q n -> (e : Elim q 0 n) ->
                       (0 ne : NotRedex defs e) ->
-                      m (Term q 0 n)
+                      EqualE q (Term q 0 n)
     computeElimType ctx (F x) _ = do
       defs <- lookupFree' defs x
       pure $ injectT ctx defs.type
@@ -384,7 +383,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
     private covering
     replaceEnd : EqContext q n ->
                  (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
-                 m (Elim q 0 n)
+                 EqualE q (Elim q 0 n)
     replaceEnd ctx e p ne = do
       (ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne)
       pure $ ends l r p :# dsub1 ty (K p)
@@ -398,7 +397,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       ||| ⚠ **assumes that they have both been typechecked, and have
       ||| equal types.** ⚠
       export covering %inline
-      compare0 : EqContext q n -> (e, f : Elim q 0 n) -> m ()
+      compare0 : EqContext q n -> (e, f : Elim q 0 n) -> EqualE q ()
       compare0 ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
           let Val n = ctx.termLen
@@ -412,7 +411,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       compare0' : EqContext q n ->
                   (e, f : Elim q 0 n) ->
                   (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
-                  m ()
+                  EqualE q ()
       -- replace applied equalities with the appropriate end first
       -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
       --
@@ -429,7 +428,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       compare0' ctx e@(B _) f _ _ = clashE ctx e f
 
       compare0' ctx (e :@ s) (f :@ t) ne nf =
-        local {mode := Equal} $ do
+        local_ Equal $ do
           compare0 ctx e f
           (_, arg, _) <- expectPiE defs ctx !(computeElimType ctx e (noOr1 ne))
           Term.compare0 ctx arg s t
@@ -437,7 +436,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
 
       compare0' ctx (CasePair epi e eret ebody)
                     (CasePair fpi f fret fbody) ne nf =
-        local {mode := Equal} $ do
+        local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
           compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@@ -451,7 +450,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
 
       compare0' ctx (CaseEnum epi e eret earms)
                     (CaseEnum fpi f fret farms) ne nf =
-        local {mode := Equal} $ do
+        local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
           compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@@ -460,15 +459,15 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
               !(lookupArm t earms) !(lookupArm t farms)
           expectEqualQ epi fpi
         where
-          lookupArm : TagVal -> CaseEnumArms q d n -> m (Term q d n)
+          lookupArm : TagVal -> CaseEnumArms q d n -> EqualE q (Term q d n)
           lookupArm t arms = case lookup t arms of
             Just arm => pure arm
-            Nothing  => throwError $ TagNotIn t (fromList $ keys arms)
+            Nothing  => throw $ TagNotIn t (fromList $ keys arms)
       compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f
 
       compare0' ctx (CaseNat epi epi' e eret ezer esuc)
                     (CaseNat fpi fpi' f fret fzer fsuc) ne nf =
-        local {mode := Equal} $ do
+        local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
           compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@@ -483,7 +482,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
 
       compare0' ctx (CaseBox epi e eret ebody)
                     (CaseBox fpi f fret fbody) ne nf =
-        local {mode := Equal} $ do
+        local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
           compareType (extendTy zero eret.name ety ctx) eret.term fret.term
@@ -497,15 +496,16 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       compare0' ctx (s :# a) (t :# b) _ _ =
           Term.compare0 ctx !(bigger a b) s t
         where
-          bigger : forall a. a -> a -> m a
-          bigger l r = asks mode <&> \case Super => l; _ => r
+          bigger : forall a. a -> a -> EqualE q a
+          bigger l r = mode <&> \case Super => l; _ => r
 
       compare0' ctx   (s :# a) f        _ _ = Term.compare0 ctx a s (E f)
       compare0' ctx e          (t :# b) _ _ = Term.compare0 ctx b (E e) t
       compare0' ctx e@(_ :# _) f        _ _ = clashE ctx e f
 
 
-parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)}
+parameters {auto _ : (Has (DefsReader' q _) fs, Has (ErrorEff q) fs)}
+           {auto _ : IsQty q}
            (ctx : TyContext q d n)
   -- [todo] only split on the dvars that are actually used anywhere in
   -- the calls to `splits`
@@ -513,51 +513,51 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, IsQty q)}
   parameters (mode : EqMode)
     namespace Term
       export covering
-      compare : (ty, s, t : Term q d n) -> m ()
+      compare : (ty, s, t : Term q d n) -> Eff fs ()
       compare ty s t = do
         defs <- ask
-        runReaderT {m} (MkCmpContext {mode}) $
+        map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            compare0 defs ectx (ty // th) (s // th) (t // th)
+            lift $ compare0 defs ectx (ty // th) (s // th) (t // th)
 
       export covering
-      compareType : (s, t : Term q d n) -> m ()
+      compareType : (s, t : Term q d n) -> Eff fs ()
       compareType s t = do
         defs <- ask
-        runReaderT {m} (MkCmpContext {mode}) $
+        map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            compareType defs ectx (s // th) (t // th)
+            lift $ compareType defs ectx (s // th) (t // th)
 
     namespace Elim
       ||| you don't have to pass the type in but the arguments must still be
       ||| of the same type!!
       export covering %inline
-      compare : (e, f : Elim q d n) -> m ()
+      compare : (e, f : Elim q d n) -> Eff fs ()
       compare e f = do
         defs <- ask
-        runReaderT {m} (MkCmpContext {mode}) $
+        map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            compare0 defs ectx (e // th) (f // th)
+            lift $ compare0 defs ectx (e // th) (f // th)
 
   namespace Term
     export covering %inline
-    equal, sub, super : (ty, s, t : Term q d n) -> m ()
+    equal, sub, super : (ty, s, t : Term q d n) -> Eff fs ()
     equal = compare Equal
     sub   = compare Sub
     super = compare Super
 
     export covering %inline
-    equalType, subtype, supertype : (s, t : Term q d n) -> m ()
+    equalType, subtype, supertype : (s, t : Term q d n) -> Eff fs ()
     equalType = compareType Equal
     subtype   = compareType Sub
     supertype = compareType Super
 
   namespace Elim
     export covering %inline
-    equal, sub, super : (e, f : Elim q d n) -> m ()
+    equal, sub, super : (e, f : Elim q d n) -> Eff fs ()
     equal = compare Equal
     sub   = compare Sub
     super = compare Super
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 597d223..93ffd88 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -7,15 +7,27 @@ import Quox.Typechecker
 
 import Data.List
 import Data.SnocVect
-import public Control.Monad.Either
-import public Control.Monad.State
-import public Control.Monad.Reader
+import Quox.EffExtra
 
 import System.File
 import System.Path
+import Data.IORef
 
-%hide Context.(<$>)
-%hide Context.(<*>)
+
+%default total
+
+%hide Typing.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+
+public export
+0 Def : Type
+Def = Definition Three
+
+public export
+0 NDef : Type
+NDef = (Name, Def)
 
 public export
 0 Defs : Type
@@ -33,30 +45,26 @@ data FromParserError =
   | ParseError Parser.Error
 
 public export
-0 CanError : (Type -> Type) -> Type
-CanError = MonadError FromParserError
+0 IncludePath : Type
+IncludePath = List String
 
 public export
-0 HasDefsRW : (Type -> Type) -> Type
-HasDefsRW = MonadState Defs
-
-public export
-0 HasNamespace : (Type -> Type) -> Type
-HasNamespace = MonadReader Mods
+0 SeenFiles : Type
+SeenFiles = SortedSet String
 
 
 public export
-0 LoadFile : (Type -> Type) -> Type
-LoadFile m =
-  (HasIO m, MonadReader (List String) m, MonadState (SortedSet String) m)
-    -- reader for include paths, state for seen files
-
+data StateTag = DEFS | NS | SEEN
 
 public export
-0 FromParser : (Type -> Type) -> Type
-FromParser m =
-  (CanError m, HasDefsRW m, HasNamespace m, LoadFile m)
+0 FromParserEff : List (Type -> Type)
+FromParserEff =
+  [Except Error, StateL DEFS Defs, StateL NS Mods,
+   Reader IncludePath, StateL SEEN SeenFiles, IO]
 
+public export
+0 FromParser : Type -> Type
+FromParser = Eff FromParserEff
 
 
 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
@@ -70,24 +78,24 @@ parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
   fromName x = if null x.mods then fromBaseName x.base else f x
 
 export
-fromPDimWith : CanError m =>
-               Context' BName d -> PDim -> m (Dim d)
+fromPDimWith : Has (Except Error) fs =>
+               Context' BName d -> PDim -> Eff fs (Dim d)
 fromPDimWith ds (K e) = pure $ K e
 fromPDimWith ds (V i) =
-  fromBaseName (pure . B) (const $ throwError $ DimNotInScope i) ds i
+  fromBaseName (pure . B) (const $ throw $ DimNotInScope i) ds i
 
 private
-avoidDim : CanError m => Context' BName d -> PName -> m (Term q d n)
+avoidDim : Has (Except Error) fs =>
+           Context' BName d -> PName -> Eff fs (Term q d n)
 avoidDim ds x =
-  fromName (const $ throwError $ DimNameInTerm x.base)
-           (pure . FT . fromPName) ds x
+  fromName (const $ throw $ DimNameInTerm x.base) (pure . FT . fromPName) ds x
 
 
 mutual
   export
-  fromPTermWith : CanError m =>
+  fromPTermWith : Has (Except Error) fs =>
                   Context' BName d -> Context' BName n ->
-                  PTerm -> m (Term Three d n)
+                  PTerm -> Eff fs (Term Three d n)
   fromPTermWith ds ns t0 = case t0 of
     TYPE k =>
       pure $ TYPE $ k
@@ -136,7 +144,7 @@ mutual
       if length strs == length (SortedSet.toList set) then
         pure $ Enum set
       else
-        throwError $ DuplicatesInEnum strs
+        throw $ DuplicatesInEnum strs
 
     Tag str => pure $ Tag str
 
@@ -168,27 +176,27 @@ mutual
       map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
 
   private
-  fromPTermEnumArms : CanError m =>
+  fromPTermEnumArms : Has (Except Error) fs =>
                       Context' BName d -> Context' BName n ->
-                      List (TagVal, PTerm) -> m (CaseEnumArms Three d n)
+                      List (TagVal, PTerm) -> Eff fs (CaseEnumArms Three d n)
   fromPTermEnumArms ds ns =
     map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
 
   private
-  fromPTermElim : CanError m =>
+  fromPTermElim : Has (Except Error) fs =>
                   Context' BName d -> Context' BName n ->
-                  PTerm -> m (Elim Three d n)
+                  PTerm -> Eff fs (Elim Three d n)
   fromPTermElim ds ns e =
     case !(fromPTermWith ds ns e) of
       E e => pure e
-      _   => throwError $ AnnotationNeeded e
+      _   => throw $ AnnotationNeeded e
 
   -- [todo] use SN if the var is named but still unused
   private
-  fromPTermTScope : {s : Nat} -> CanError m =>
+  fromPTermTScope : {s : Nat} -> Has (Except Error) fs =>
                     Context' BName d -> Context' BName n ->
                     SnocVect s BName ->
-                    PTerm -> m (ScopeTermN s Three d n)
+                    PTerm -> Eff fs (ScopeTermN s Three d n)
   fromPTermTScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
@@ -197,10 +205,10 @@ mutual
         <$> fromPTermWith ds (ns ++ xs) t
 
   private
-  fromPTermDScope : {s : Nat} -> CanError m =>
+  fromPTermDScope : {s : Nat} -> Has (Except Error) fs =>
                     Context' BName d -> Context' BName n ->
                     SnocVect s BName ->
-                    PTerm -> m (DScopeTermN s Three d n)
+                    PTerm -> Eff fs (DScopeTermN s Three d n)
   fromPTermDScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
@@ -210,29 +218,32 @@ mutual
 
 
 export %inline
-fromPTerm : CanError m => PTerm -> m (Term Three 0 0)
+fromPTerm : Has (Except Error) fs => PTerm -> Eff fs (Term Three 0 0)
 fromPTerm = fromPTermWith [<] [<]
 
 
 export
-globalPQty : CanError m => (q : PQty) -> m (IsGlobal q)
+globalPQty : Has (Except Error) fs =>
+             (q : PQty) -> Eff fs (IsGlobal q)
 globalPQty pi = case isGlobal pi of
   Yes y => pure y
-  No  n => throwError $ QtyNotGlobal pi
+  No  n => throw $ QtyNotGlobal pi
 
 
 export
-fromPNameNS : HasNamespace m => PName -> m Name
-fromPNameNS name = asks $ \ns => addMods ns $ fromPName name
+fromPNameNS : Has (StateL NS Mods) fs => PName -> Eff fs Name
+fromPNameNS name = pure $ addMods !(getAt NS) $ fromPName name
 
 private
-injTC : (CanError m, HasDefsRW m) => (forall m'. CanTC Three m' => m' a) -> m a
-injTC act =
-  either (throwError . TypeError) pure $
-  runReaderT {m = Either _} !get act
+injTC : (Has (StateL DEFS Defs) fs, Has (Except Error) fs) =>
+        TC Three a -> Eff fs a
+injTC act = rethrow $ mapFst TypeError $ runTC !(getAt DEFS) act
 
-export
-fromPDef : (CanError m, HasDefsRW m, HasNamespace m) => PDefinition -> m ()
+export covering
+fromPDef : (Has (StateL DEFS Defs) fs,
+            Has (StateL NS Mods) fs,
+            Has (Except Error) fs) =>
+           PDefinition -> Eff fs NDef
 fromPDef (MkPDef qty pname ptype pterm) = do
   name <- fromPNameNS pname
   qtyGlobal <- globalPQty qty
@@ -243,39 +254,73 @@ fromPDef (MkPDef qty pname ptype pterm) = do
     Just type => do
       injTC $ checkTypeC empty type Nothing
       injTC $ ignore $ checkC empty sqty term type
-      modify $ insert name $ mkDef qty type term
+      let def = mkDef qty type term
+      modifyAt DEFS $ insert name def
+      pure (name, def)
     Nothing => do
-      let E elim = term | _ => throwError $ AnnotationNeeded pterm
+      let E elim = term | _ => throw $ AnnotationNeeded pterm
       res <- injTC $ inferC empty sqty elim
-      modify $ insert name $ mkDef qty res.type term
+      let def = mkDef qty res.type term
+      modifyAt DEFS $ insert name def
+      pure (name, def)
 
-export
-fromPDecl : FromParser m => PDecl -> m ()
-fromPDecl (PDef def) = fromPDef def
+export covering
+fromPDecl : (Has (StateL DEFS Defs) fs,
+             Has (StateL NS Mods) fs,
+             Has (Except Error) fs) =>
+            PDecl -> Eff fs (List NDef)
+fromPDecl (PDef def) = singleton <$> fromPDef def
 fromPDecl (PNs  ns)  =
-  local (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
+  localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
 
 
-export
-loadFile : (LoadFile m, CanError m) => String -> m (Maybe String)
+export covering
+loadFile : (Has IO fs,
+            Has (StateL SEEN SeenFiles) fs,
+            Has (Reader IncludePath) fs,
+            Has (Except Error) fs) =>
+           String -> Eff fs (Maybe String)
 loadFile file =
-  if contains file !get then
+  if contains file !(getAt SEEN) then
     pure Nothing
   else do
     Just file <- firstExists (map (</> file) !ask)
-      | Nothing => throwError $ LoadError file FileNotFound
+      | Nothing => throw $ LoadError file FileNotFound
     case !(readFile file) of
-      Right res => pure $ Just res
-      Left  err => throwError $ LoadError file err
+      Right res => modifyAt SEEN (insert file) $> Just res
+      Left  err => throw $ LoadError file err
+
+parameters {auto _ : (Has IO fs,
+                      Has (StateL SEEN SeenFiles) fs,
+                      Has (Reader IncludePath) fs,
+                      Has (Except Error) fs,
+                      Has (StateL DEFS Defs) fs,
+                      Has (StateL NS Mods) fs)}
+ mutual
+  export covering
+  loadProcessFile : String -> Eff fs (List NDef)
+  loadProcessFile file =
+    case !(loadFile file) of
+      Just inp => do
+        tl <- either (throw . ParseError) pure $ lexParseInput inp
+        concat <$> traverse fromPTopLevel tl
+      Nothing => pure []
+
+  ||| populates the `defs` field of the state
+  export covering
+  fromPTopLevel : PTopLevel -> Eff fs (List NDef)
+  fromPTopLevel (PD    decl) = fromPDecl decl
+  fromPTopLevel (PLoad file) = loadProcessFile file
 
 
-||| populates the `defs` field of the state
 export
-fromPTopLevel : FromParser m => PTopLevel -> m ()
-fromPTopLevel (PD    decl) = fromPDecl decl
-fromPTopLevel (PLoad file) =
-  case !(loadFile file) of
-    Just inp => do
-      tl <- either (throwError . ParseError) pure $ lexParseInput inp
-      traverse_ fromPTopLevel tl
-    Nothing => pure ()
+fromParserIO : (MonadRec io, HasIO io) =>
+               IncludePath -> IORef SeenFiles -> IORef Defs ->
+               FromParser a -> io (Either Error a)
+fromParserIO inc seen defs act =
+  runIO $
+  runExcept $
+  evalStateAt NS [<] $
+  runStateIORefAt SEEN seen $
+  runStateIORefAt DEFS defs $
+  runReader inc act
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index e923d09..7c6b6b7 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -6,27 +6,33 @@ import public Quox.Equal
 import Data.List
 import Data.SnocVect
 import Data.List1
+import Quox.EffExtra
 
 %default total
 
 
 public export
-0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
-CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)
+0 TCEff : (q : Type) -> IsQty q => List (Type -> Type)
+TCEff q = [ErrorEff q, DefsReader q]
 
 public export
-0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
-CanTC q = CanTC' q IsGlobal
+0 TC : (q : Type) -> IsQty q => Type -> Type
+TC q = Eff $ TCEff q
+
+export
+runTC : (0 _ : IsQty q) => Definitions q -> TC q a -> Either (Error q) a
+runTC defs = extract . runExcept . runReader defs
 
 
 export
-popQs : HasErr q m => IsQty q =>
-        QOutput q s -> QOutput q (s + n) -> m (QOutput q n)
+popQs : IsQty q => Has (ErrorEff q) fs =>
+        QOutput q s -> QOutput q (s + n) -> Eff fs (QOutput q n)
 popQs [<]         qout         = pure qout
 popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
 export %inline
-popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
+popQ : IsQty q => Has (ErrorEff q) fs =>
+       q -> QOutput q (S n) -> Eff fs (QOutput q n)
 popQ pi = popQs [< pi]
 
 export
@@ -42,7 +48,7 @@ lubs ctx []        = Just $ zeroFor ctx
 lubs ctx (x :: xs) = lubs1 $ x ::: xs
 
 
-parameters {auto _ : IsQty q} {auto _ : CanTC q m}
+parameters {auto _ : IsQty q}
  mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
   |||
@@ -54,21 +60,21 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   ||| doing any further work.
   export covering %inline
   check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
-          m (CheckResult ctx.dctx q n)
+          TC q (CheckResult ctx.dctx q n)
   check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
   |||
   ||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
   export covering %inline
-  check0 : TyContext q d n -> Term q d n -> Term q d n -> m ()
+  check0 : TyContext q d n -> Term q d n -> Term q d n -> TC q ()
   check0 ctx tm ty = ignore $ check ctx szero tm ty
     -- the output will always be 𝟎 because the subject quantity is 0
 
   ||| `check`, assuming the dimension context is consistent
   export covering %inline
   checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
-           m (CheckResult' q n)
+           TC q (CheckResult' q n)
   checkC ctx sg subj ty =
     wrapErr (WhileChecking ctx sg.fst subj ty) $
       let Element subj nc = pushSubsts subj in
@@ -79,16 +85,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   ||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the
   ||| universe doesn't matter, only that a term is _a_ type, so it is optional.
   export covering %inline
-  checkType : TyContext q d n -> Term q d n -> Maybe Universe -> m ()
+  checkType : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
   checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
 
   export covering %inline
-  checkTypeC : TyContext q d n -> Term q d n -> Maybe Universe -> m ()
+  checkTypeC : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
   checkTypeC ctx subj l =
     wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l
 
   export covering %inline
-  checkTypeNoWrap : TyContext q d n -> Term q d n -> Maybe Universe -> m ()
+  checkTypeNoWrap : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
   checkTypeNoWrap ctx subj l =
     let Element subj nc = pushSubsts subj in
     checkType' ctx subj l
@@ -102,13 +108,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   ||| doing any further work.
   export covering %inline
   infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
-          m (InferResult ctx.dctx q d n)
+          TC q (InferResult ctx.dctx q d n)
   infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
 
   ||| `infer`, assuming the dimension context is consistent
   export covering %inline
   inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
-           m (InferResult' q d n)
+           TC q (InferResult' q d n)
   inferC ctx sg subj =
     wrapErr (WhileInferring ctx sg.fst subj) $
       let Element subj nc = pushSubsts subj in
@@ -118,7 +124,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   private covering
   toCheckType : TyContext q d n -> SQty q ->
                 (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
-                m (CheckResult' q n)
+                TC q (CheckResult' q n)
   toCheckType ctx sg t ty = do
     u <- expectTYPE !ask ctx ty
     expectEqualQ zero sg.fst
@@ -128,7 +134,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   private covering
   check' : TyContext q d n -> SQty q ->
            (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
-           m (CheckResult' q n)
+           TC q (CheckResult' q n)
 
   check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty
 
@@ -160,7 +166,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   check' ctx sg (Tag t) ty = do
     tags <- expectEnum !ask ctx ty
     -- if t ∈ ts
-    unless (t `elem` tags) $ throwError $ TagNotIn t tags
+    unless (t `elem` tags) $ throw $ TagNotIn t tags
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
     pure $ zeroFor ctx
 
@@ -207,12 +213,12 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   private covering
   checkType' : TyContext q d n ->
                (subj : Term q d n) -> (0 nc : NotClo subj) =>
-               Maybe Universe -> m ()
+               Maybe Universe -> TC q ()
 
   checkType' ctx (TYPE k) u = do
     -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
     case u of
-      Just l  => unless (k < l) $ throwError $ BadUniverse k l
+      Just l  => unless (k < l) $ throw $ BadUniverse k l
       Nothing => pure ()
 
   checkType' ctx (Pi qty arg res) u = do
@@ -225,7 +231,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
 
   checkType' ctx t@(Lam {}) u =
-    throwError $ NotType ctx t
+    throw $ NotType ctx t
 
   checkType' ctx (Sig fst snd) u = do
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
@@ -237,13 +243,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
 
   checkType' ctx t@(Pair {}) u =
-    throwError $ NotType ctx t
+    throw $ NotType ctx t
 
   checkType' ctx (Enum _) u = pure ()
     -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
 
   checkType' ctx t@(Tag {}) u =
-    throwError $ NotType ctx t
+    throw $ NotType ctx t
 
   checkType' ctx (Eq t l r) u = do
     -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
@@ -257,14 +263,14 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
 
   checkType' ctx t@(DLam {}) u =
-    throwError $ NotType ctx t
+    throw $ NotType ctx t
 
   checkType' ctx Nat u = pure ()
-  checkType' ctx Zero u = throwError $ NotType ctx Zero
-  checkType' ctx t@(Succ _) u = throwError $ NotType ctx t
+  checkType' ctx Zero u = throw $ NotType ctx Zero
+  checkType' ctx t@(Succ _) u = throw $ NotType ctx t
 
   checkType' ctx (BOX q ty) u = checkType ctx ty u
-  checkType' ctx t@(Box _) u = throwError $ NotType ctx t
+  checkType' ctx t@(Box _) u = throw $ NotType ctx t
 
   checkType' ctx (E e) u = do
     -- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
@@ -279,7 +285,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   private covering
   infer' : TyContext q d n -> SQty q ->
            (subj : Elim q d n) -> (0 nc : NotClo subj) =>
-           m (InferResult' q d n)
+           TC q (InferResult' q d n)
 
   infer' ctx sg (F x) = do
     -- if π·x : A {≔ s} in global context
@@ -289,7 +295,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
     pure $ InfRes {type = injectT ctx g.type, qout = zeroFor ctx}
    where
-    lookupFree : Name -> m (Definition q)
+    lookupFree : Name -> TC q (Definition q)
     lookupFree x = lookupFree' !ask x
 
   infer' ctx sg (B i) =
@@ -352,11 +358,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- with Σ₂ = lubs Σᵢ
     let arms = SortedMap.toList arms
     let armTags = SortedSet.fromList $ map fst arms
-    unless (ttags == armTags) $ throwError $ BadCaseEnum ttags armTags
+    unless (ttags == armTags) $ throw $ BadCaseEnum ttags armTags
     armres <- for arms $ \(a, s) =>
       checkC ctx sg s (sub1 ret (Tag a :# tres.type))
     let Just armout = lubs ctx armres
-          | _ => throwError $ BadCaseQtys ctx $
+          | _ => throw $ BadCaseQtys ctx $
               zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
     pure $ InfRes {
       type = sub1 ret t,
@@ -381,7 +387,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
         sucType   = substCaseNatRet ret
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
     let Just armout = lubs ctx [zerout, sucout]
-          | _ => throwError $ BadCaseQtys ctx $
+          | _ => throw $ BadCaseQtys ctx $
               [(zerout, Zero), (sucout, Succ $ FT $ unq p)]
     expectCompatQ qih (pi' * sg.fst)
     -- [fixme] better error here
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index a9f0a6d..9da8d50 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -8,6 +8,8 @@ import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Reduce
 
+import Control.Eff
+
 %default total
 
 
@@ -31,11 +33,12 @@ InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n
 
 
 export
-lookupFree' : HasErr q m => Definitions' q g -> Name -> m (Definition' q g)
+lookupFree' : Has (ErrorEff q) fs =>
+              Definitions' q g -> Name -> Eff fs (Definition' q g)
 lookupFree' defs x =
   case lookup x defs of
     Just d  => pure d
-    Nothing => throwError $ NotInScope x
+    Nothing => throw $ NotInScope x
 
 
 public export
@@ -53,98 +56,100 @@ substCaseBoxRet : Term q d n -> ScopeTerm q d n -> Term q d (S n)
 substCaseBoxRet dty retty =
   retty.term // (Box (BVT 0) :# weakT dty ::: shift 1)
 
-parameters {auto _ : HasErr q m} (defs : Definitions' q _)
+
+parameters (defs : Definitions' q _) {auto _ : Has (ErrorEff q) fs}
   export covering %inline
   whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
-          {d, n : Nat} -> tm q d n -> m (NonRedex tm q d n defs)
-  whnfT = either (throwError . WhnfError) pure . whnf defs
+          {d, n : Nat} -> tm q d n -> Eff fs (NonRedex tm q d n defs)
+  whnfT = either (throw . WhnfError) pure . whnf defs
 
   parameters {d2, n : Nat} (ctx : Lazy (TyContext q d1 n))
              (th : Lazy (DSubst d2 d1))
     export covering %inline
-    expectTYPE_ : Term q d2 n -> m Universe
+    expectTYPE_ : Term q d2 n -> Eff fs Universe
     expectTYPE_ s = case fst !(whnfT s) of
       TYPE l => pure l
-      _      => throwError $ ExpectedTYPE ctx (s // th)
+      _      => throw $ ExpectedTYPE ctx (s // th)
 
     export covering %inline
-    expectPi_ : Term q d2 n -> m (q, Term q d2 n, ScopeTerm q d2 n)
+    expectPi_ : Term q d2 n -> Eff fs (q, Term q d2 n, ScopeTerm q d2 n)
     expectPi_ s = case fst !(whnfT s) of
       Pi {qty, arg, res, _} => pure (qty, arg, res)
-      _                     => throwError $ ExpectedPi ctx (s // th)
+      _                     => throw $ ExpectedPi ctx (s // th)
 
     export covering %inline
-    expectSig_ : Term q d2 n -> m (Term q d2 n, ScopeTerm q d2 n)
+    expectSig_ : Term q d2 n -> Eff fs (Term q d2 n, ScopeTerm q d2 n)
     expectSig_ s = case fst !(whnfT s) of
       Sig {fst, snd, _} => pure (fst, snd)
-      _                 => throwError $ ExpectedSig ctx (s // th)
+      _                 => throw $ ExpectedSig ctx (s // th)
 
     export covering %inline
-    expectEnum_ : Term q d2 n -> m (SortedSet TagVal)
+    expectEnum_ : Term q d2 n -> Eff fs (SortedSet TagVal)
     expectEnum_ s = case fst !(whnfT s) of
       Enum tags => pure tags
-      _         => throwError $ ExpectedEnum ctx (s // th)
+      _         => throw $ ExpectedEnum ctx (s // th)
 
     export covering %inline
-    expectEq_ : Term q d2 n -> m (DScopeTerm q d2 n, Term q d2 n, Term q d2 n)
+    expectEq_ : Term q d2 n ->
+                Eff fs (DScopeTerm q d2 n, Term q d2 n, Term q d2 n)
     expectEq_ s = case fst !(whnfT s) of
       Eq {ty, l, r, _} => pure (ty, l, r)
-      _                => throwError $ ExpectedEq ctx (s // th)
+      _                => throw $ ExpectedEq ctx (s // th)
 
     export covering %inline
-    expectNat_ : Term q d2 n -> m ()
+    expectNat_ : Term q d2 n -> Eff fs ()
     expectNat_ s = case fst !(whnfT s) of
       Nat => pure ()
-      _   => throwError $ ExpectedNat ctx (s // th)
+      _   => throw $ ExpectedNat ctx (s // th)
 
     export covering %inline
-    expectBOX_ : Term q d2 n -> m (q, Term q d2 n)
+    expectBOX_ : Term q d2 n -> Eff fs (q, Term q d2 n)
     expectBOX_ s = case fst !(whnfT s) of
       BOX q a => pure (q, a)
-      _       => throwError $ ExpectedBOX ctx (s // th)
+      _       => throw $ ExpectedBOX ctx (s // th)
 
 
   -- [fixme] refactor this stuff
 
   parameters (ctx : TyContext q d n)
     export covering %inline
-    expectTYPE : Term q d n -> m Universe
+    expectTYPE : Term q d n -> Eff fs Universe
     expectTYPE =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectTYPE_ ctx id
 
     export covering %inline
-    expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
+    expectPi : Term q d n -> Eff fs (q, Term q d n, ScopeTerm q d n)
     expectPi =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectPi_ ctx id
 
     export covering %inline
-    expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
+    expectSig : Term q d n -> Eff fs (Term q d n, ScopeTerm q d n)
     expectSig =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectSig_ ctx id
 
     export covering %inline
-    expectEnum : Term q d n -> m (SortedSet TagVal)
+    expectEnum : Term q d n -> Eff fs (SortedSet TagVal)
     expectEnum =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectEnum_ ctx id
 
     export covering %inline
-    expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
+    expectEq : Term q d n -> Eff fs (DScopeTerm q d n, Term q d n, Term q d n)
     expectEq =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectEq_ ctx id
 
     export covering %inline
-    expectNat : Term q d n -> m ()
+    expectNat : Term q d n -> Eff fs ()
     expectNat =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectNat_ ctx id
 
     export covering %inline
-    expectBOX : Term q d n -> m (q, Term q d n)
+    expectBOX : Term q d n -> Eff fs (q, Term q d n)
     expectBOX =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectBOX_ ctx id
@@ -152,43 +157,43 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
 
   parameters (ctx : EqContext q n)
     export covering %inline
-    expectTYPEE : Term q 0 n -> m Universe
+    expectTYPEE : Term q 0 n -> Eff fs Universe
     expectTYPEE t =
       let Val n = ctx.termLen in
       expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectPiE : Term q 0 n -> m (q, Term q 0 n, ScopeTerm q 0 n)
+    expectPiE : Term q 0 n -> Eff fs (q, Term q 0 n, ScopeTerm q 0 n)
     expectPiE t =
       let Val n = ctx.termLen in
       expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectSigE : Term q 0 n -> m (Term q 0 n, ScopeTerm q 0 n)
+    expectSigE : Term q 0 n -> Eff fs (Term q 0 n, ScopeTerm q 0 n)
     expectSigE t =
       let Val n = ctx.termLen in
       expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectEnumE : Term q 0 n -> m (SortedSet TagVal)
+    expectEnumE : Term q 0 n -> Eff fs (SortedSet TagVal)
     expectEnumE t =
       let Val n = ctx.termLen in
       expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectEqE : Term q 0 n -> m (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
+    expectEqE : Term q 0 n -> Eff fs (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
     expectEqE t =
       let Val n = ctx.termLen in
       expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectNatE : Term q 0 n -> m ()
+    expectNatE : Term q 0 n -> Eff fs ()
     expectNatE t =
       let Val n = ctx.termLen in
       expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectBOXE : Term q 0 n -> m (q, Term q 0 n)
+    expectBOXE : Term q 0 n -> Eff fs (q, Term q 0 n)
     expectBOXE t =
       let Val n = ctx.termLen in
       expectBOX_ (toTyContext ctx) (shift0 ctx.dimLen) t
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index 8ce1b2d..634240c 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -7,7 +7,7 @@ import Quox.Typing.EqMode
 import Quox.Pretty
 
 import Data.List
-import public Control.Monad.Either
+import Control.Eff
 
 
 public export
@@ -64,8 +64,8 @@ data Error q
 %name Error err
 
 public export
-0 HasErr : Type -> (Type -> Type) -> Type
-HasErr q = MonadError (Error q)
+ErrorEff : Type -> Type -> Type
+ErrorEff q = Except $ Error q
 
 
 ||| whether the error is surrounded in some context
@@ -119,24 +119,22 @@ where
   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
+private
+expect : Has (Except e) fs =>
+         (a -> a -> e) -> (a -> a -> Bool) -> a -> a -> Eff fs ()
+expect err cmp x y = unless (x `cmp` y) $ throw $ err x y
 
-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}
+parameters {auto _ : Has (Except $ Error q) fs}
   export %inline
-  expectEqualQ : Eq q => q -> q -> m ()
+  expectEqualQ : Eq q => q -> q -> Eff fs ()
   expectEqualQ = expect ClashQ (==)
 
   export %inline
-  expectCompatQ : IsQty q => q -> q -> m ()
+  expectCompatQ : IsQty q => q -> q -> Eff fs ()
   expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
 
   export %inline
-  expectModeU : EqMode -> Universe -> Universe -> m ()
+  expectModeU : EqMode -> Universe -> Universe -> Eff fs ()
   expectModeU mode = expect (ClashU mode) $ ucmp mode
 
 
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 7502bb8..e588c9a 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -5,11 +5,12 @@ authors   = "rhiannon morris"
 sourceloc = "https://git.rhiannon.website/rhi/quox"
 license   = "acsl"
 
-depends = base, contrib, elab-util, snocvect
+depends = base, contrib, elab-util, snocvect, eff
 
 modules =
   Quox.BoolExtra,
   Quox.CharExtra,
+  Quox.EffExtra,
   Quox.Decidable,
   Quox.No,
   Quox.Pretty,