diff --git a/exe/CompileMonad.idr b/exe/CompileMonad.idr
index 3f20fc7..9bdc28a 100644
--- a/exe/CompileMonad.idr
+++ b/exe/CompileMonad.idr
@@ -146,7 +146,8 @@ liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
 liftErase defs act =
   runEff act
     [handleExcept $ \err => throw $ EraseError err,
-     handleStateIORef !(asksAt STATE suf)]
+     handleStateIORef !(asksAt STATE suf),
+     \g => send g]
 
 export %inline
 liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 83748af..796b6ff 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -2,9 +2,12 @@ module Quox.Equal
 
 import Quox.BoolExtra
 import public Quox.Typing
-import Data.Maybe
-import Quox.EffExtra
 import Quox.FreeVars
+import Quox.Pretty
+import Quox.EffExtra
+
+import Data.List1
+import Data.Maybe
 
 %default total
 
@@ -15,11 +18,11 @@ EqModeState = State EqMode
 
 public export
 Equal : List (Type -> Type)
-Equal = [ErrorEff, DefsReader, NameGen]
+Equal = [ErrorEff, DefsReader, NameGen, Log]
 
 public export
 EqualInner : List (Type -> Type)
-EqualInner = [ErrorEff, NameGen, EqModeState]
+EqualInner = [ErrorEff, NameGen, EqModeState, Log]
 
 
 export %inline
@@ -74,9 +77,25 @@ sameTyCon (E       {}) _            = False
 ||| * `[π.A]` is empty if `A` is.
 ||| * that's it.
 public export covering
-isEmpty : Definitions -> EqContext n -> SQty -> Term 0 n ->
-          Eff EqualInner Bool
-isEmpty defs ctx sg ty0 = do
+isEmpty :
+  {default 30 logLevel : Nat} -> (0 _ : So (isLogLevel logLevel)) =>
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+private covering
+isEmptyNoLog :
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+isEmpty defs ctx sg ty = do
+  sayMany "equal" ty.loc
+    [logLevel :> "isEmpty",
+     95       :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     95       :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
+  res <- isEmptyNoLog defs ctx sg ty
+  say "equal" logLevel ty.loc $ hsep ["isEmpty ⇝", pshow res]
+  pure res
+
+isEmptyNoLog defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
   let Left  y = choose $ isTyConE ty0
     | Right n => pure False
@@ -85,16 +104,17 @@ isEmpty defs ctx sg ty0 = do
     IOState {} => pure False
     Pi {arg, res, _} => pure False
     Sig {fst, snd, _} =>
-      isEmpty defs ctx sg fst `orM`
-      isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term
+      isEmpty defs ctx sg fst {logLevel = 90} `orM`
+      isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term {logLevel = 90}
     Enum {cases, _} =>
       pure $ null cases
     Eq {} => pure False
     NAT {} => pure False
     STRING {} => pure False
-    BOX {ty, _} => isEmpty defs ctx sg ty
+    BOX {ty, _} => isEmpty defs ctx sg ty {logLevel = 90}
     E _ => pure False
 
+
 ||| true if a type is known to be a subsingleton purely by its form.
 ||| a subsingleton is a type with only zero or one possible values.
 ||| equality/subtyping accepts immediately on values of subsingleton types.
@@ -106,27 +126,42 @@ isEmpty defs ctx sg ty0 = do
 ||| * an enum type is a subsingleton if it has zero or one tags.
 ||| * a box type is a subsingleton if its content is
 public export covering
-isSubSing : Definitions -> EqContext n -> SQty -> Term 0 n ->
-            Eff EqualInner Bool
-isSubSing defs ctx sg ty0 = do
+isSubSing :
+  {default 30 logLevel : Nat} -> (0 _ : So (isLogLevel logLevel)) =>
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+private covering
+isSubSingNoLog :
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+isSubSing defs ctx sg ty = do
+  sayMany "equal" ty.loc
+    [logLevel :> "isSubSing",
+     95       :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     95       :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
+  res <- isSubSingNoLog defs ctx sg ty
+  say "equal" logLevel ty.loc $ hsep ["isSubsing ⇝", pshow res]
+  pure res
+
+isSubSingNoLog defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
-  let Left  y = choose $ isTyConE ty0
-    | Right n => pure False
+  let Left y = choose $ isTyConE ty0 | _ => pure False
   case ty0 of
     TYPE {} => pure False
     IOState {} => pure False
     Pi {arg, res, _} =>
-      isEmpty defs ctx sg arg `orM`
-      isSubSing defs (extendTy0 res.name arg ctx) sg res.term
+      isEmpty defs ctx sg arg {logLevel = 90} `orM`
+      isSubSing defs (extendTy0 res.name arg ctx) sg res.term {logLevel = 90}
     Sig {fst, snd, _} =>
-      isSubSing defs ctx sg fst `andM`
-      isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term
+      isSubSing defs ctx sg fst {logLevel = 90} `andM`
+      isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term {logLevel = 90}
     Enum {cases, _} =>
       pure $ length (SortedSet.toList cases) <= 1
     Eq {} => pure True
     NAT {} => pure False
     STRING {} => pure False
-    BOX {ty, _} => isSubSing defs ctx sg ty
+    BOX {ty, _} => isSubSing defs ctx sg ty {logLevel = 90}
     E _ => pure False
 
 
@@ -137,12 +172,21 @@ bigger l r = gets $ \case Super => l; _ => r
 
 
 export
-ensureTyCon : Has ErrorEff fs =>
-              (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
-              Eff fs (So (isTyConE t))
-ensureTyCon loc ctx t = case nchoose $ isTyConE t of
-  Left  y => pure y
-  Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen)
+ensureTyCon, ensureTyConNoLog :
+  (Has Log fs, Has ErrorEff fs) =>
+  (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
+  Eff fs (So (isTyConE t))
+ensureTyConNoLog loc ctx ty = do
+  case nchoose $ isTyConE ty of
+    Left  y => pure y
+    Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen)
+
+ensureTyCon loc ctx ty = do
+  sayMany "equal" ty.loc
+    [60 :> "ensureTyCon",
+     95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     60 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
+  ensureTyConNoLog loc ctx ty
 
 
 namespace Term
@@ -750,7 +794,11 @@ namespace Elim
 
 
 namespace Term
-  compare0 defs ctx sg ty s t =
+  export covering %inline
+  compare0NoLog :
+    Definitions -> EqContext n -> SQty -> (ty, s, t : Term 0 n) ->
+    Eff EqualInner ()
+  compare0NoLog defs ctx sg ty s t =
     wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
       Element ty' _ <- whnf defs ctx SZero ty.loc ty
       Element s'  _ <- whnf defs ctx sg s.loc  s
@@ -758,20 +806,72 @@ namespace Term
       tty <- ensureTyCon ty.loc ctx ty'
       compare0' defs ctx sg ty' s' t'
 
+  compare0 defs ctx sg ty s t = do
+    sayMany "equal" s.loc
+      [30 :> "Term.compare0",
+       30 :> hsep ["mode =", pshow !mode],
+       95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+       95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+       31 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty],
+       30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s],
+       30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]]
+    compare0NoLog defs ctx sg ty s t
+
 namespace Elim
-  compare0 defs ctx sg e f = do
+  export covering %inline
+  compare0NoLog :
+    Definitions -> EqContext n -> SQty -> (e, f : Elim 0 n) ->
+    Eff EqualInner (Term 0 n)
+  compare0NoLog defs ctx sg e f = do
     (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f
     maybe (pure ty) throw err
 
-compareType defs ctx s t = do
+  compare0 defs ctx sg e f = do
+    sayMany "equal" e.loc
+      [30 :> "Elim.compare0",
+       30 :> hsep ["mode =", pshow !mode],
+       95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+       95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+       30 :> hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e],
+       30 :> hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]]
+    ty <- compare0NoLog defs ctx sg e f
+    say "equal" 31 e.loc $
+      hsep ["Elim.compare0 ⇝", runPretty $ prettyTerm [<] ctx.tnames ty]
+    pure ty
+
+export covering %inline
+compareTypeNoLog :
+  Definitions -> EqContext n -> (s, t : Term 0 n) -> Eff EqualInner ()
+compareTypeNoLog defs ctx s t = do
   Element s' _ <- whnf defs ctx SZero s.loc s
   Element t' _ <- whnf defs ctx SZero t.loc t
   ts <- ensureTyCon s.loc ctx s'
   tt <- ensureTyCon t.loc ctx t'
-  st <- either pure (const $ clashTy s.loc ctx s' t') $
-        nchoose $ sameTyCon s' t'
+  let Left _ = choose $ sameTyCon s' t' | _ => clashTy s.loc ctx s' t'
   compareType' defs ctx s' t'
 
+compareType defs ctx s t = do
+  sayMany "equal" s.loc
+    [30 :> "compareType",
+     30 :> hsep ["mode =", pshow !mode],
+     95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s],
+     30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]]
+  compareTypeNoLog defs ctx s t
+
+
+private
+getVars : TyContext d _ -> FreeVars d -> List BindName
+getVars ctx (FV fvs) = case ctx.dctx of
+  ZeroIsOne => []
+  C eqs     => toList $ getVars' ctx.dnames eqs fvs
+where
+  getVars' : BContext d' -> DimEq' d' -> FreeVars' d' -> SnocList BindName
+  getVars' (names :< name) (eqs :< eq) (fvs :< fv) =
+    let rest = getVars' names eqs fvs in
+    case eq of Nothing => rest :< name
+               Just _  => rest
+  getVars' [<] [<] [<] = [<]
 
 parameters (loc : Loc) (ctx : TyContext d n)
   parameters (mode : EqMode)
@@ -780,9 +880,11 @@ parameters (loc : Loc) (ctx : TyContext d n)
     fromInner = lift . map fst . runState mode
 
     private
-    eachFace : Applicative f => FreeVars d ->
-               (EqContext n -> DSubst d 0 -> f ()) -> f ()
-    eachFace fvs act =
+    eachCorner : Has Log fs => Loc -> FreeVars d ->
+                 (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs ()
+    eachCorner loc fvs act = do
+      say "equal" 50 loc $
+        hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs)
       for_ (splits loc ctx.dctx fvs) $ \th =>
         act (makeEqContext ctx th) th
 
@@ -792,31 +894,36 @@ parameters (loc : Loc) (ctx : TyContext d n)
       Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
 
     private
-    runCompare : FreeVars d -> CompareAction d n -> Eff Equal ()
-    runCompare fvs act = fromInner $ eachFace fvs $ act !(askAt DEFS)
+    runCompare : Loc -> FreeVars d -> CompareAction d n -> Eff Equal ()
+    runCompare loc fvs act = fromInner $ eachCorner loc fvs $ act !(askAt DEFS)
 
     private
-    fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
-    fdvAll = let Val d = ctx.dimLen in foldMap (fdvWith [|d|] ctx.termLen)
+    foldMap1 : Semigroup b => (a -> b) -> List1 a -> b
+    foldMap1 f = foldl1By (\x, y => x <+> f y) f
+
+    private
+    fdvAll : HasFreeDVars t => (xs : List (t d n)) -> (0 _ : NonEmpty xs) =>
+             FreeVars d
+    fdvAll (x :: xs) = foldMap1 (fdvWith ctx.dimLen ctx.termLen) (x ::: xs)
 
     namespace Term
       export covering
       compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
-      compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
-        compare0 defs ectx sg (ty // th) (s // th) (t // th)
+      compare sg ty s t = runCompare s.loc (fdvAll [ty, s, t]) $
+        \defs, ectx, th => compare0 defs ectx sg (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term d n) -> Eff Equal ()
-      compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th =>
-        compareType defs ectx (s // th) (t // th)
+      compareType s t = runCompare s.loc (fdvAll [s, t]) $
+        \defs, ectx, th => 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
       compare : SQty -> (e, f : Elim d n) -> Eff Equal ()
-      compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
-        ignore $ compare0 defs ectx sg (e // th) (f // th)
+      compare sg e f = runCompare e.loc (fdvAll [e, f]) $
+        \defs, ectx, th => ignore $ compare0 defs ectx sg (e // th) (f // th)
 
   namespace Term
     export covering %inline
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index b49976d..8328272 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -331,6 +331,7 @@ liftTC : Eff TC a -> Eff FromParserPure a
 liftTC tc = runEff tc $ with Union.(::)
   [handleExcept $ \e => throw $ WrapTypeError e,
    handleReaderConst !(getAt DEFS),
+   \g => send g,
    \g => send g]
 
 private
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 020b947..a224641 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -59,10 +59,15 @@ Traversable (IfConsistent eqs) where
   traverse f Nothing  = pure Nothing
   traverse f (Just x) = Just <$> f x
 
+public export
+ifConsistentElse : Applicative f => (eqs : DimEq d) ->
+                   f a -> f () -> f (IfConsistent eqs a)
+ifConsistentElse ZeroIsOne yes no = Nothing <$  no
+ifConsistentElse (C _)     yes no = Just    <$> yes
+
 public export
 ifConsistent : Applicative f => (eqs : DimEq d) -> f a -> f (IfConsistent eqs a)
-ifConsistent ZeroIsOne act = pure Nothing
-ifConsistent (C _)     act = Just <$> act
+ifConsistent eqs act = ifConsistentElse eqs act (pure ())
 
 public export
 toMaybe : IfConsistent eqs a -> Maybe a
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 681aa7c..3892b27 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -3,6 +3,7 @@ module Quox.Typechecker
 import public Quox.Typing
 import public Quox.Equal
 import Quox.Displace
+import Quox.Pretty
 
 import Data.List
 import Data.SnocVect
@@ -14,7 +15,7 @@ import Quox.EffExtra
 
 public export
 0 TC : List (Type -> Type)
-TC = [ErrorEff, DefsReader, NameGen]
+TC = [ErrorEff, DefsReader, NameGen, Log]
 
 
 parameters (loc : Loc)
@@ -41,6 +42,24 @@ lubs ctx []        = zeroFor ctx
 lubs ctx (x :: xs) = lubs1 $ x ::: xs
 
 
+private
+prettyTermTC : {opts : LayoutOpts} ->
+               TyContext d n -> Term d n -> Eff Pretty (Doc opts)
+prettyTermTC ctx s = prettyTerm ctx.dnames ctx.tnames s
+
+
+private
+checkLogs : String -> TyContext d n -> SQty ->
+            Term d n -> Maybe (Term d n) -> Eff TC ()
+checkLogs fun ctx sg subj ty = do
+  let tyDoc = delay $ maybe (text "none") (runPretty . prettyTermTC ctx) ty
+  sayMany "check" subj.loc
+    [10 :> text fun,
+     95 :> hsep ["ctx =",  runPretty $ prettyTyContext ctx],
+     95 :> hsep ["sg =",   runPretty $ prettyQty sg.qty],
+     10 :> hsep ["subj =", runPretty $ prettyTermTC ctx subj],
+     10 :> hsep ["ty =",   tyDoc]]
+
 mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
   |||
@@ -53,7 +72,11 @@ mutual
   export covering %inline
   check : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
           Eff TC (CheckResult ctx.dctx n)
-  check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
+  check ctx sg subj ty =
+    ifConsistentElse ctx.dctx
+      (do checkLogs "check" ctx sg subj (Just ty)
+          checkC ctx sg subj ty)
+      (say "check" 20 subj.loc "check: 0=1")
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
   |||
@@ -84,7 +107,12 @@ mutual
   ||| universe doesn't matter, only that a term is _a_ type, so it is optional.
   export covering %inline
   checkType : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
-  checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
+  checkType ctx subj l = do
+    let univ = TYPE <$> l <*> pure noLoc
+    ignore $ ifConsistentElse ctx.dctx
+      (do checkLogs "checkType" ctx SZero subj univ
+          checkTypeC ctx subj l)
+      (say "check" 20 subj.loc "checkType: 0=1")
 
   export covering %inline
   checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
@@ -107,7 +135,11 @@ mutual
   export covering %inline
   infer : (ctx : TyContext d n) -> SQty -> Elim d n ->
           Eff TC (InferResult ctx.dctx d n)
-  infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
+  infer ctx sg subj = do
+    ifConsistentElse ctx.dctx
+      (do checkLogs "infer" ctx sg (E subj) Nothing
+          inferC ctx sg subj)
+      (say "check" 20 subj.loc "infer: 0=1")
 
   ||| `infer`, assuming the dimension context is consistent
   export covering %inline
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 46238b4..4b92a17 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -7,6 +7,7 @@ import public Quox.Typing.Error as Typing
 import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Whnf
+import public Quox.Pretty
 
 import Language.Reflection
 import Control.Eff
@@ -46,16 +47,15 @@ lookupFree x loc defs = maybe (throw $ NotInScope loc x) pure $ lookup x defs
 public export
 substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
 substCasePairRet [< x, y] dty retty =
-  let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
-      arg = Ann tm (dty // fromNat 2) tm.loc
-  in
+  let tm  = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
+      arg = Ann tm (dty // fromNat 2) tm.loc in
   retty.term // (arg ::: shift 2)
 
 public export
 substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet [< p, ih] retty =
-  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) $ p.loc `extendL` ih.loc
-  in
+  let loc = p.loc `extendL` ih.loc
+      arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) loc in
   retty.term // (arg ::: shift 2)
 
 public export
@@ -65,23 +65,31 @@ substCaseBoxRet x dty retty =
   retty.term // (arg ::: shift 1)
 
 
-parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
+private
+0 ExpectErrorConstructor : Type
+ExpectErrorConstructor =
+  forall d, n. Loc -> NameContexts d n -> Term d n -> Error
+
+parameters (defs : Definitions)
+           {auto _ : (Has ErrorEff fs, Has NameGen fs, Has Log fs)}
   namespace TyContext
    parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-           tm d n -> Eff fs (NonRedex tm d n defs ? sg)
+           tm d n -> Eff fs (NonRedex tm d n defs (toWhnfContext ctx) sg)
     whnf tm = do
       let Val n = ctx.termLen; Val d = ctx.dimLen
       res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 
     private covering %macro
-    expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> Error) ->
-             TTImp -> TTImp -> Elab (Term d n -> Eff fs a)
-    expect k l r = do
-      f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
-      pure $ \t => maybe (throw $ k loc ctx.names t) pure . f . fst =<< whnf t
+    expect : ExpectErrorConstructor -> TTImp -> TTImp ->
+             Elab (Term d n -> Eff fs a)
+    expect err pat rhs = Prelude.do
+      match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
+      pure $ \term => do
+        res <- whnf term
+        maybe (throw $ err loc ctx.names term) pure $ match $ fst res
 
     export covering %inline
     expectTYPE : Term d n -> Eff fs Universe
@@ -120,19 +128,20 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
    parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-           tm 0 n -> Eff fs (NonRedex tm 0 n defs ? sg)
+           tm 0 n -> Eff fs (NonRedex tm 0 n defs (toWhnfContext ctx) sg)
     whnf tm = do
       res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 
     private covering %macro
-    expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> Error) ->
-             TTImp -> TTImp -> Elab (Term 0 n -> Eff fs a)
-    expect k l r = do
-      f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
-      pure $ \t =>
-        let err = throw $ k loc ctx.names (t // shift0 ctx.dimLen) in
-        maybe err pure . f . fst =<< whnf t
+    expect : ExpectErrorConstructor -> TTImp -> TTImp ->
+             Elab (Term 0 n -> Eff fs a)
+    expect err pat rhs = do
+      match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
+      pure $ \term => do
+        res <- whnf term
+        let t0 = delay $ term // shift0 ctx.dimLen
+        maybe (throw $ err loc ctx.names t0) pure $ match $ fst res
 
     export covering %inline
     expectTYPE : Term 0 n -> Eff fs Universe
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 7b10046..fe8322c 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -339,9 +339,10 @@ namespace WhnfContext
 private
 prettyTContextElt : {opts : _} ->
                     BContext d -> BContext n ->
-                    Qty -> BindName -> LocalVar d n -> Eff Pretty (Doc opts)
+                    Doc opts -> BindName -> LocalVar d n ->
+                    Eff Pretty (Doc opts)
 prettyTContextElt dnames tnames q x s = do
-  q  <- prettyQty q;   dot <- dotD
+  dot <- dotD
   x  <- prettyTBind x; colon <- colonD
   ty <- withPrec Outer $ prettyTerm dnames tnames s.type; eq <- cstD
   tm <- traverse (withPrec Outer . prettyTerm dnames tnames) s.term
@@ -356,7 +357,7 @@ prettyTContextElt dnames tnames q x s = do
 
 private
 prettyTContext' : {opts : _} ->
-                  BContext d -> QContext n -> BContext n ->
+                  BContext d -> Context' (Doc opts) n -> BContext n ->
                   TContext d n -> Eff Pretty (SnocList (Doc opts))
 prettyTContext' _ [<] [<] [<] = pure [<]
 prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) =
@@ -369,6 +370,7 @@ prettyTContext : {opts : _} ->
                  TContext d n -> Eff Pretty (Doc opts)
 prettyTContext dnames qtys tnames tys = do
   comma <- commaD
+  qtys <- traverse prettyQty qtys
   sepSingle . exceptLast (<+> comma) . toList <$>
     prettyTContext' dnames qtys tnames tys
 
@@ -384,3 +386,10 @@ prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
 export
 prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)
 prettyEqContext ctx = prettyTyContext $ toTyContext ctx
+
+export
+prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts)
+prettyWhnfContext ctx =
+  let Val n = ctx.termLen in
+  separateTight !commaD <$>
+  prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx
diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr
index 34a1206..54062b4 100644
--- a/lib/Quox/Untyped/Erase.idr
+++ b/lib/Quox/Untyped/Erase.idr
@@ -88,7 +88,7 @@ parameters {opts : LayoutOpts} (showContext : Bool)
 
 public export
 Erase : List (Type -> Type)
-Erase = [Except Error, NameGen]
+Erase = [Except Error, NameGen, Log]
 
 export
 liftWhnf : Eff Whnf a -> Eff Erase a
diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr
index 87891ff..3661c12 100644
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/lib/Quox/Whnf/ComputeElimType.idr
@@ -2,6 +2,7 @@ module Quox.Whnf.ComputeElimType
 
 import Quox.Whnf.Interface
 import Quox.Displace
+import Quox.Pretty
 
 %default total
 
@@ -18,7 +19,6 @@ computeElimType :
   (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
   Eff Whnf (Term d n)
 
-
 ||| computes a type and then reduces it to whnf
 export covering
 computeWhnfElimType0 :
@@ -28,7 +28,16 @@ computeWhnfElimType0 :
   (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
   Eff Whnf (Term d n)
 
-computeElimType defs ctx sg e =
+
+private covering
+computeElimTypeNoLog, computeWhnfElimType0NoLog :
+  CanWhnf Term Interface.isRedexT =>
+  CanWhnf Elim Interface.isRedexE =>
+  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
+  Eff Whnf (Term d n)
+
+computeElimTypeNoLog defs ctx sg e =
   case e of
     F x u loc => do
       let Just def = lookup x defs
@@ -39,7 +48,7 @@ computeElimType defs ctx sg e =
       pure (ctx.tctx !! i).type
 
     App f s loc =>
-      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
         ty               => throw $ ExpectedPi loc ctx.names ty
 
@@ -47,12 +56,12 @@ computeElimType defs ctx sg e =
       pure $ sub1 ret pair
 
     Fst pair loc =>
-      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
         Sig {fst, _} => pure fst
         ty           => throw $ ExpectedSig loc ctx.names ty
 
     Snd pair loc =>
-      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
         Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
         ty           => throw $ ExpectedSig loc ctx.names ty
 
@@ -66,7 +75,7 @@ computeElimType defs ctx sg e =
       pure $ sub1 ret box
 
     DApp {fun = f, arg = p, loc} =>
-      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
         Eq {ty, _} => pure $ dsub1 ty p
         t          => throw $ ExpectedEq loc ctx.names t
 
@@ -82,5 +91,20 @@ computeElimType defs ctx sg e =
     TypeCase {ret, _} =>
       pure ret
 
+computeElimType defs ctx sg e {ne} = do
+  let Val n = ctx.termLen
+  sayMany "whnf" e.loc
+    [90 :> "computeElimType",
+     95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
+     90 :> hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]]
+  res <- computeElimTypeNoLog defs ctx sg e {ne}
+  say "whnf" 91 e.loc $
+    hsep ["computeElimType ⇝",
+          runPretty $ prettyTerm ctx.dnames ctx.tnames res]
+  pure res
+
 computeWhnfElimType0 defs ctx sg e =
   computeElimType defs ctx sg e >>= whnf0 defs ctx SZero
+
+computeWhnfElimType0NoLog defs ctx sg e {ne} =
+  computeElimTypeNoLog defs ctx sg e {ne} >>= whnf0 defs ctx SZero
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index 1fccefc..e516f62 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -1,6 +1,7 @@
 module Quox.Whnf.Interface
 
 import public Quox.No
+import public Quox.Log
 import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Typing.Context
@@ -13,7 +14,7 @@ import public Control.Eff
 
 public export
 Whnf : List (Type -> Type)
-Whnf = [Except Error, NameGen]
+Whnf = [Except Error, NameGen, Log]
 
 
 public export
@@ -24,17 +25,20 @@ RedexTest tm =
 public export
 interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
-  whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
-         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
+  whnf, whnfNoLog :
+    (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
+    tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
   -- having isRedex be part of the class header, and needing to be explicitly
   -- quantified on every use since idris can't infer its type, is a little ugly.
   -- but none of the alternatives i've thought of so far work. e.g. in some
   -- cases idris can't tell that `isRedex` and `isRedexT` are the same thing
 
 public export %inline
-whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-        Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
-whnf0 defs ctx q t = fst <$> whnf defs ctx q t
+whnf0, whnfNoLog0 :
+  {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
+  Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
+whnf0      defs ctx q t = fst <$> whnf defs ctx q t
+whnfNoLog0 defs ctx q t = fst <$> whnfNoLog defs ctx q t
 
 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 75a1248..1c3bcc4 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -4,6 +4,7 @@ import Quox.Whnf.Interface
 import Quox.Whnf.ComputeElimType
 import Quox.Whnf.TypeCase
 import Quox.Whnf.Coercion
+import Quox.Pretty
 import Quox.Displace
 import Data.SnocVect
 
@@ -14,19 +15,43 @@ export covering CanWhnf Term Interface.isRedexT
 export covering CanWhnf Elim Interface.isRedexE
 
 
+-- the String is what to call the "s" argument in logs (maybe "s", or "e")
+private %inline
+whnfDefault :
+  {0 isRedex : RedexTest tm} ->
+  (CanWhnf tm isRedex, Located2 tm) =>
+  String ->
+  (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) ->
+  (defs : Definitions) ->
+  (ctx : WhnfContext d n) ->
+  (sg : SQty) ->
+  (s : tm d n) ->
+  Eff Whnf (Subset (tm d n) (No . isRedex defs ctx sg))
+whnfDefault name ppr defs ctx sg s = do
+  sayMany "whnf" s.loc
+    [10 :> "whnf",
+     95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
+     95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     10 :> hsep [text name, "=", runPretty $ ppr ctx s]]
+  res <- whnfNoLog defs ctx sg s
+  say "whnf" 11 s.loc $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst]
+  pure res
+
 covering
 CanWhnf Elim Interface.isRedexE where
-  whnf defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
+  whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e
+
+  whnfNoLog defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
     _ | Just y  = whnf defs ctx sg $ setLoc loc $ injElim ctx y
     _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
 
-  whnf defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
+  whnfNoLog defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
     _ | l with (l.term) proof eq2
       _ | Just y  = whnf defs ctx sg $ Ann y l.type loc
       _ | Nothing = pure $ Element (B i loc) $ rewrite eq1 in rewrite eq2 in Ah
 
   -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
-  whnf defs ctx sg (App f s appLoc) = do
+  whnfNoLog defs ctx sg (App f s appLoc) = do
     Element f fnf <- whnf defs ctx sg f
     case nchoose $ isLamHead f of
       Left _ => case f of
@@ -41,7 +66,7 @@ CanWhnf Elim Interface.isRedexE where
   --
   -- 0 · case e return p ⇒ C of { (a, b) ⇒ u } ⇝
   -- u[fst e/a, snd e/b] ∷ C[e/p]
-  whnf defs ctx sg (CasePair pi pair ret body caseLoc) = do
+  whnfNoLog defs ctx sg (CasePair pi pair ret body caseLoc) = do
     Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
@@ -64,7 +89,7 @@ CanWhnf Elim Interface.isRedexE where
                            (pairnf `orNo` np `orNo` notYesNo n0)
 
   -- fst ((s, t) ∷ (x : A) × B) ⇝ s ∷ A
-  whnf defs ctx sg (Fst pair fstLoc) = do
+  whnfNoLog defs ctx sg (Fst pair fstLoc) = do
     Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
@@ -76,7 +101,7 @@ CanWhnf Elim Interface.isRedexE where
         pure $ Element (Fst pair fstLoc) (pairnf `orNo` np)
 
   -- snd ((s, t) ∷ (x : A) × B) ⇝ t ∷ B[(s ∷ A)/x]
-  whnf defs ctx sg (Snd pair sndLoc) = do
+  whnfNoLog defs ctx sg (Snd pair sndLoc) = do
     Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
@@ -89,7 +114,7 @@ CanWhnf Elim Interface.isRedexE where
 
   -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
   -- u ∷ C['a∷{a,…}/p]
-  whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
+  whnfNoLog defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
     Element tag tagnf <- whnf defs ctx sg tag
     case nchoose $ isTagHead tag of
       Left _ => case tag of
@@ -110,7 +135,7 @@ CanWhnf Elim Interface.isRedexE where
   --
   -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
   --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-  whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
+  whnfNoLog defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
     Element nat natnf <- whnf defs ctx sg nat
     case nchoose $ isNatHead nat of
       Left _ =>
@@ -137,7 +162,7 @@ CanWhnf Elim Interface.isRedexE where
 
   -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
   --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
-  whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
+  whnfNoLog defs ctx sg (CaseBox pi box ret body caseLoc) = do
     Element box boxnf <- whnf defs ctx sg box
     case nchoose $ isBoxHead box of
       Left _ => case box of
@@ -153,7 +178,7 @@ CanWhnf Elim Interface.isRedexE where
   -- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
   --
   -- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
-  whnf defs ctx sg (DApp f p appLoc) = do
+  whnfNoLog defs ctx sg (DApp f p appLoc) = do
     Element f fnf <- whnf defs ctx sg f
     case nchoose $ isDLamHead f of
       Left _ => case f of
@@ -173,7 +198,7 @@ CanWhnf Elim Interface.isRedexE where
         B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
 
   -- e ∷ A ⇝ e
-  whnf defs ctx sg (Ann s a annLoc) = do
+  whnfNoLog defs ctx sg (Ann s a annLoc) = do
     Element s snf <- whnf defs ctx sg s
     case nchoose $ isE s of
       Left  _  => let E e = s in pure $ Element e $ noOr2 snf
@@ -181,7 +206,7 @@ CanWhnf Elim Interface.isRedexE where
         Element a anf <- whnf defs ctx SZero a
         pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
 
-  whnf defs ctx sg (Coe sty p q val coeLoc) =
+  whnfNoLog defs ctx sg (Coe sty p q val coeLoc) =
     --   𝑖 ∉ fv(A)
     -- -------------------------------
     --   coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
@@ -201,7 +226,7 @@ CanWhnf Elim Interface.isRedexE where
       (_, Right ty) =>
         whnf defs ctx sg $ Ann val ty coeLoc
 
-  whnf defs ctx sg (Comp ty p q val r zero one compLoc) =
+  whnfNoLog defs ctx sg (Comp ty p q val r zero one compLoc) =
     case p `decEqv` q of
       -- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
       Yes y   => whnf defs ctx sg $ Ann val ty compLoc
@@ -213,7 +238,7 @@ CanWhnf Elim Interface.isRedexE where
         B {}     => pure $ Element (Comp ty p q val r zero one compLoc)
                                    (notYesNo npq `orNo` Ah)
 
-  whnf defs ctx sg (TypeCase ty ret arms def tcLoc) =
+  whnfNoLog defs ctx sg (TypeCase ty ret arms def tcLoc) =
     case sg `decEq` SZero of
       Yes Refl => do
         Element ty  tynf  <- whnf defs ctx SZero ty
@@ -226,48 +251,50 @@ CanWhnf Elim Interface.isRedexE where
       No _ =>
         throw $ ClashQ tcLoc sg.qty Zero
 
-  whnf defs ctx sg (CloE (Sub el th)) =
-    whnf defs ctx sg $ pushSubstsWith' id th el
-  whnf defs ctx sg (DCloE (Sub el th)) =
-    whnf defs ctx sg $ pushSubstsWith' th id el
+  whnfNoLog defs ctx sg (CloE (Sub el th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' id th el
+  whnfNoLog defs ctx sg (DCloE (Sub el th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' th id el
 
 covering
 CanWhnf Term Interface.isRedexT where
-  whnf _ _ _ t@(TYPE    {}) = pure $ nred t
-  whnf _ _ _ t@(IOState {}) = pure $ nred t
-  whnf _ _ _ t@(Pi      {}) = pure $ nred t
-  whnf _ _ _ t@(Lam     {}) = pure $ nred t
-  whnf _ _ _ t@(Sig     {}) = pure $ nred t
-  whnf _ _ _ t@(Pair    {}) = pure $ nred t
-  whnf _ _ _ t@(Enum    {}) = pure $ nred t
-  whnf _ _ _ t@(Tag     {}) = pure $ nred t
-  whnf _ _ _ t@(Eq      {}) = pure $ nred t
-  whnf _ _ _ t@(DLam    {}) = pure $ nred t
-  whnf _ _ _ t@(NAT     {}) = pure $ nred t
-  whnf _ _ _ t@(Nat     {}) = pure $ nred t
-  whnf _ _ _ t@(STRING  {}) = pure $ nred t
-  whnf _ _ _ t@(Str     {}) = pure $ nred t
-  whnf _ _ _ t@(BOX     {}) = pure $ nred t
-  whnf _ _ _ t@(Box     {}) = pure $ nred t
+  whnf = whnfDefault "e" $ \ctx, s => prettyTerm ctx.dnames ctx.tnames s
 
-  whnf _ _ _ (Succ p loc) =
+  whnfNoLog _ _ _ t@(TYPE    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(IOState {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Pi      {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Lam     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Sig     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Pair    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Enum    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Tag     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Eq      {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(DLam    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(NAT     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Nat     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(STRING  {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Str     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(BOX     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Box     {}) = pure $ nred t
+
+  whnfNoLog _ _ _ (Succ p loc) =
     case nchoose $ isNatConst p of
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
       Right nc => pure $ nred $ Succ p loc
 
-  whnf defs ctx sg (Let _ rhs body _) =
+  whnfNoLog defs ctx sg (Let _ rhs body _) =
     whnf defs ctx sg $ sub1 body rhs
 
   -- s ∷ A ⇝ s   (in term context)
-  whnf defs ctx sg (E e) = do
+  whnfNoLog defs ctx sg (E e) = do
     Element e enf <- whnf defs ctx sg e
     case nchoose $ isAnn e of
       Left  _  => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
       Right na => pure $ Element (E e) $ na `orNo` enf
 
-  whnf defs ctx sg (CloT (Sub tm th)) =
-    whnf defs ctx sg $ pushSubstsWith' id th tm
-  whnf defs ctx sg (DCloT (Sub tm th)) =
-    whnf defs ctx sg $ pushSubstsWith' th id tm
+  whnfNoLog defs ctx sg (CloT (Sub tm th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' id th tm
+  whnfNoLog defs ctx sg (DCloT (Sub tm th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' th id tm
diff --git a/tests/Tests/DimEq.idr b/tests/Tests/DimEq.idr
index f368991..c48729e 100644
--- a/tests/Tests/DimEq.idr
+++ b/tests/Tests/DimEq.idr
@@ -97,7 +97,7 @@ tests = "dimension constraints" :- [
     testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
     testPrettyD [<] new "" {label = "[empty output from empty context]"},
     testPrettyD ii new "𝑖",
-    testPrettyD iijj (fromGround [< "𝑖", "𝑗"] [< Zero, One])
+    testPrettyD iijj (fromGround iijj [< Zero, One])
       "𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
     testPrettyD iijj (C [< Just (^K Zero), Nothing])
       "𝑖, 𝑗, 𝑖 = 0",
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 40c071e..f566f07 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -15,7 +15,8 @@ import Control.Eff
 runWhnf : Eff Whnf a -> Either Error a
 runWhnf act = runSTErr $ do
   runEff act [handleExcept (\e => stLeft e),
-              handleStateSTRef !(liftST $ newSTRef 0)]
+              handleStateSTRef !(liftST $ newSTRef 0),
+              handleLogDiscard]
 
 parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
            {auto _ : (Eq (tm d n), Show (tm d n))}
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index 34c889a..80b2bbd 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -22,10 +22,11 @@ ToInfo Error where
 export
 runEqual : Definitions -> Eff Equal a -> Either Error a
 runEqual defs act = runSTErr $ do
-  runEff act
+  runEff act $ with Union.(::)
     [handleExcept (\e => stLeft e),
      handleReaderConst defs,
-     handleStateSTRef !(liftST $ newSTRef 0)]
+     handleStateSTRef !(liftST $ newSTRef 0),
+     handleLogDiscard]
 
 export
 runTC : Definitions -> Eff TC a -> Either Error a