diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr
index 4c4afd6..85420f7 100644
--- a/lib/Quox/EffExtra.idr
+++ b/lib/Quox/EffExtra.idr
@@ -52,6 +52,7 @@ public export
 data Length : List a -> Type where
   Z : Length []
   S : Length xs -> Length (x :: xs)
+%builtin Natural Length
 
 export
 subsetWith : Length xs => (forall z. Has z xs -> Has z ys) ->
@@ -64,20 +65,28 @@ subsetSelf : Length xs => Subset xs xs
 subsetSelf = subsetWith id
 
 export
-subsetTail : Length xs => Subset xs (x :: xs)
-subsetTail = subsetWith S
+subsetTail : Length xs => (0 x : a) -> 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)
+catchMaybeAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
+               (e -> Eff fs a) -> Eff fs a -> Eff fs a
+catchMaybeAt lbl hnd act =
+  catchAt lbl hnd $ lift @{subsetTail $ ExceptL lbl e} act
 
 export %inline
-wrapErr : Length fs => (e -> e') ->
-          Eff (Except e :: fs) a -> Eff (Except e' :: fs) a
+catchMaybe : (Has (Except e) fs, Length fs) =>
+             (e -> Eff fs a) -> Eff fs a -> Eff fs a
+catchMaybe = catchMaybeAt ()
+
+export
+wrapErrAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
+            (e -> e) -> Eff fs a -> Eff fs a
+wrapErrAt lbl wrap = catchMaybeAt lbl (\ex => throwAt lbl $ wrap ex)
+
+export %inline
+wrapErr : (Has (Except e) fs, Length fs) => (e -> e) -> Eff fs a -> Eff fs a
 wrapErr = wrapErrAt ()
 
 
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index a4417e7..bb66b43 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -363,38 +363,49 @@ parameters (defs : Definitions)
       ||| equal types.** ⚠
       export covering %inline
       compare0 : EqContext n -> (e, f : Elim 0 n) -> Eff EqualInner (Term 0 n)
-      compare0 ctx e f =
+      compare0 ctx e f = do
+        (err, ty) <- compare0Inner ctx e f
+        maybe (pure ty) throw err
+
+      private covering
+      compare0Inner : EqContext n -> (e, f : Elim 0 n) ->
+                      Eff EqualInner (Maybe Error, Term 0 n)
+      compare0Inner ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
           let Val n = ctx.termLen
-          Element e' ne <- whnf defs ctx e.loc e
-          Element f' nf <- whnf defs ctx f.loc f
-
-          -- [todo] share the work of this computeElimTypeE and the return value
-          -- of compare0' somehow?????
-          ty <- computeElimTypeE defs ctx e'
+          Element e ne <- whnf defs ctx e.loc e
+          Element f nf <- whnf defs ctx f.loc f
+          (err, ty) <- compare0' ctx e f ne nf
           if !(isSubSing defs ctx ty)
-             then pure ty
-             else compare0' ctx e' f' ne nf
+             then pure (Nothing, ty)
+             else pure (err, ty)
+
+      private
+      try_ : Eff EqualInner () -> Eff EqualInner (Maybe Error)
+      try_ act = lift $ catch (pure . Just) $ act $> Nothing
+
+      private
+      lookupFree : EqContext n -> Name -> Universe -> Loc ->
+                   Eff EqualInner (Term 0 n)
+      lookupFree ctx x u loc =
+        let Val n = ctx.termLen in
+        maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $
+        lookup x defs
 
       private covering
       compare0' : EqContext n ->
                   (e, f : Elim 0 n) ->
                   (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
-                  Eff EqualInner (Term 0 n)
+                  Eff EqualInner (Maybe Error, Term 0 n)
 
-      compare0' ctx e@(F x u loc) f@(F y v _) _ _ =
-        if x == y && u == v
-           then do let Val n    = ctx.termLen
-                   let Just def = lookup x defs
-                     | Nothing => throw $ NotInScope loc x
-                   pure def.type
-           else clashE e.loc ctx e f
+      compare0' ctx e@(F x u loc) f@(F y v _) _ _ = do
+        pure (guard (x /= y || u /= v) $> ClashE loc ctx !mode e f,
+              !(lookupFree ctx x u loc))
       compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f
 
-      compare0' ctx e@(B i _) f@(B j _) _ _ =
-        if i == j
-           then pure $ ctx.tctx !! i
-           else clashE e.loc ctx e f
+      compare0' ctx e@(B i loc) f@(B j _) _ _ =
+        pure (guard (i /= j) $> ClashE loc ctx !mode e f,
+              ctx.tctx !! i)
       compare0' ctx e@(B {}) f _ _ = clashE e.loc ctx e f
 
       --  Ψ | Γ ⊢ e = f ⇒ π.(x : A) → B
@@ -403,10 +414,10 @@ parameters (defs : Definitions)
       --  Ψ | Γ ⊢ e s = f t ⇒ B[s∷A/x]
       compare0' ctx (App e s eloc) (App f t floc) ne nf =
         local_ Equal $ do
-          ety <- compare0 ctx e f
+          (err1, ety) <- compare0Inner ctx e f
           (_, arg, res) <- expectPi defs ctx eloc ety
-          Term.compare0 ctx arg s t
-          pure $ sub1 res (Ann s arg s.loc)
+          err2 <- try_ $ Term.compare0 ctx arg s t
+          pure (err1 <|> err2, sub1 res $ Ann s arg s.loc)
       compare0' ctx e@(App {}) f _ _ = clashE e.loc ctx e f
 
       --  Ψ | Γ ⊢ e = f ⇒ (x : A) × B
@@ -418,15 +429,16 @@ parameters (defs : Definitions)
       compare0' ctx (CasePair epi e eret ebody eloc)
                     (CasePair fpi f fret fbody {}) ne nf =
         local_ Equal $ do
-          ety <- compare0 ctx e f
+          (err1, ety) <- compare0Inner ctx e f
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           (fst, snd) <- expectSig defs ctx eloc ety
           let [< x, y] = ebody.names
-          Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
-                        (substCasePairRet ebody.names ety eret)
-                        ebody.term fbody.term
-          expectEqualQ e.loc epi fpi
-          pure $ sub1 eret e
+          err2 <- try_ $
+            Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
+                          (substCasePairRet ebody.names ety eret)
+                          ebody.term fbody.term
+          err3 <- try_ $ expectEqualQ e.loc epi fpi
+          pure (concat [err1, err2, err3], sub1 eret e)
       compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
 
       --  Ψ | Γ ⊢ e = f ⇒ {𝐚s}
@@ -438,14 +450,17 @@ parameters (defs : Definitions)
       compare0' ctx (CaseEnum epi e eret earms eloc)
                     (CaseEnum fpi f fret farms floc) ne nf =
         local_ Equal $ do
-          ety <- compare0 ctx e f
-          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          for_ !(expectEnum defs ctx eloc ety) $ \t => do
+          (err1, ety) <- compare0Inner ctx e f
+          err2 <- try_ $
+            compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
+          cases <- SortedSet.toList <$> expectEnum defs ctx eloc ety
+          exs <- for cases $ \t => do
             l <- lookupArm eloc t earms
             r <- lookupArm floc t farms
-            compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
-          expectEqualQ eloc epi fpi
-          pure $ sub1 eret e
+            try_ $
+              Term.compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
+          err3 <- try_ $ expectEqualQ eloc epi fpi
+          pure (concat $ [err1, err2, err3] ++ exs, sub1 eret e)
         where
           lookupArm : Loc -> TagVal -> CaseEnumArms d n ->
                       Eff EqualInner (Term d n)
@@ -465,18 +480,21 @@ parameters (defs : Definitions)
       compare0' ctx (CaseNat epi epi' e eret ezer esuc eloc)
                     (CaseNat fpi fpi' f fret fzer fsuc floc) ne nf =
         local_ Equal $ do
-          ety <- compare0 ctx e f
-          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          compare0 ctx
-            (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
-            ezer fzer
+          (err1, ety) <- compare0Inner ctx e f
+          err2 <- try_ $
+            compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
+          err3 <- try_ $
+            Term.compare0 ctx
+              (sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
+              ezer fzer
           let [< p, ih] = esuc.names
-          compare0
-            (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
-            (substCaseSuccRet esuc.names eret) esuc.term fsuc.term
-          expectEqualQ e.loc epi  fpi
-          expectEqualQ e.loc epi' fpi'
-          pure $ sub1 eret e
+          err4 <- try_ $
+            Term.compare0
+              (extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx)
+              (substCaseSuccRet esuc.names eret) esuc.term fsuc.term
+          err5 <- try_ $ expectEqualQ e.loc epi  fpi
+          err6 <- try_ $ expectEqualQ e.loc epi' fpi'
+          pure (concat [err1, err2, err3, err4, err5, err6], sub1 eret e)
       compare0' ctx e@(CaseNat {}) f _ _ = clashE e.loc ctx e f
 
       --  Ψ | Γ ⊢ e = f ⇒ [ρ. A]
@@ -488,14 +506,16 @@ parameters (defs : Definitions)
       compare0' ctx (CaseBox epi e eret ebody eloc)
                     (CaseBox fpi f fret fbody floc) ne nf =
         local_ Equal $ do
-          ety <- compare0 ctx e f
-          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
+          (err1, ety) <- compare0Inner ctx e f
+          err2 <- try_ $
+            compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           (q, ty) <- expectBOX defs ctx eloc ety
-          compare0 (extendTy (epi * q) ebody.name ty ctx)
-            (substCaseBoxRet ebody.name ety eret)
-            ebody.term fbody.term
-          expectEqualQ eloc epi fpi
-          pure $ sub1 eret e
+          err3 <- try_ $
+            Term.compare0 (extendTy (epi * q) ebody.name ty ctx)
+              (substCaseBoxRet ebody.name ety eret)
+              ebody.term fbody.term
+          err4 <- try_ $ expectEqualQ eloc epi fpi
+          pure (concat [err1, err2, err3, err4], sub1 eret e)
       compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
 
       -- all dim apps replaced with ends by whnf
@@ -509,8 +529,8 @@ parameters (defs : Definitions)
       -- and similar for :> and A
       compare0' ctx (Ann s a _) (Ann t b _) _ _ = do
         ty <- bigger a b
-        Term.compare0 ctx ty s t
-        pure ty
+        err <- try_ $ Term.compare0 ctx ty s t
+        pure (err, ty)
 
       --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
       --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
@@ -522,11 +542,11 @@ parameters (defs : Definitions)
                     (Coe ty2 p2 q2 val2 _) ne nf = do
         let ty1p = dsub1 ty1 p1; ty2p = dsub1 ty2 p2
             ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
-        compareType ctx ty1p ty2p
-        compareType ctx ty1q ty2q
+        err1 <- try_ $ compareType ctx ty1p ty2p
+        err2 <- try_ $ compareType ctx ty1q ty2q
         (ty_p, ty_q) <- bigger (ty1p, ty1q) (ty2p, ty2q)
-        Term.compare0 ctx ty_p val1 val2
-        pure ty_q
+        err3 <- try_ $ Term.compare0 ctx ty_p val1 val2
+        pure (concat [err1, err2, err3], ty_q)
       compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
 
       -- (no neutral compositions in a closed dctx)
@@ -538,14 +558,16 @@ parameters (defs : Definitions)
       compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc)
                     (TypeCase ty2 ret2 arms2 def2 floc) ne _ =
         local_ Equal $ do
-          ety <- compare0 ctx ty1 ty2
-          u   <- expectTYPE defs ctx eloc ety
-          compareType ctx ret1 ret2
-          compareType ctx def1 def2
-          for_ allKinds $ \k =>
-            compareArm ctx k ret1 u
-              (lookupPrecise k arms1) (lookupPrecise k arms2) def1
-          pure ret1
+          -- try
+          (err1, ety) <- compare0Inner ctx ty1 ty2
+          u    <- expectTYPE defs ctx eloc ety
+          err2 <- try_ $ compareType ctx ret1 ret2
+          err3 <- try_ $ compareType ctx def1 def2
+          exs  <- for allKinds $ \k =>
+            try_ $
+              compareArm ctx k ret1 u
+                (lookupPrecise k arms1) (lookupPrecise k arms2) def1
+          pure (concat $ [err1, err2, err3] ++ exs, ret1)
       compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f
 
       --     Ψ | Γ ⊢ s <: f ⇐ A
@@ -553,10 +575,12 @@ parameters (defs : Definitions)
       --  Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
       --
       -- and vice versa
-      compare0' ctx (Ann s a _) f _ _ =
-        Term.compare0 ctx a s (E f) $> a
-      compare0' ctx e (Ann t b _) _ _ =
-        Term.compare0 ctx b (E e) t $> b
+      compare0' ctx (Ann s a _) f _ _ = do
+        err <- try_ $ Term.compare0 ctx a s (E f)
+        pure (err, a)
+      compare0' ctx e (Ann t b _) _ _ = do
+        err <- try_ $ Term.compare0 ctx b (E e) t
+        pure (err, b)
       compare0' ctx e@(Ann {}) f _ _ =
         clashE e.loc ctx e f