diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 67151c0..4363ab8 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -16,15 +16,15 @@ import Control.Eff
 
 -- [fixme] rename this to Whnf and the interface to CanWhnf
 public export
-WhnfM : Type -> Type
-WhnfM = Eff [NameGen, Except Error]
+Whnf : List (Type -> Type)
+Whnf = [NameGen, Except Error]
 
 export
-runWhnfWith : NameSuf -> WhnfM a -> (Either Error a, NameSuf)
+runWhnfWith : NameSuf -> Eff Whnf a -> (Either Error a, NameSuf)
 runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act
 
 export
-runWhnf : WhnfM a -> Either Error a
+runWhnf : Eff Whnf a -> Either Error a
 runWhnf = fst . runWhnfWith 0
 
 
@@ -33,30 +33,30 @@ public export
 RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
 
 public export
-interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
+interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
   whnf : {d, n : Nat} -> (defs : Definitions) ->
          (ctx : WhnfContext d n) ->
-         tm d n -> WhnfM (Subset (tm d n) (No . isRedex defs))
+         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
 
 public export %inline
-whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-        (defs : Definitions) -> WhnfContext d n -> tm d n -> WhnfM (tm d n)
+whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
+        (defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n)
 whnf0 defs ctx t = fst <$> whnf defs ctx t
 
 public export
-0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
+0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
                       Definitions -> Pred (tm d n)
 IsRedex  defs = So . isRedex defs
 NotRedex defs = No . isRedex defs
 
 public export
 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
-             Whnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
+             CanWhnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
 NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
 
 public export %inline
-nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
+nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
        (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
 nred t = Element t nr
 
@@ -226,10 +226,10 @@ coeScoped ty p q loc (S names (N body)) =
 
 
 export covering
-Whnf Term Reduce.isRedexT
+CanWhnf Term Reduce.isRedexT
 
 export covering
-Whnf Elim Reduce.isRedexE
+CanWhnf Elim Reduce.isRedexE
 
 parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   ||| performs the minimum work required to recompute the type of an elim.
@@ -237,7 +237,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   ||| ⚠ **assumes the elim is already typechecked.** ⚠
   export covering
   computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
-                    WhnfM (Term d n)
+                    Eff Whnf (Term d n)
   computeElimType (F {x, u, loc}) = do
     let Just def = lookup x defs | Nothing => throw $ NotInScope loc x
     pure $ displace u def.type
@@ -265,7 +265,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for other intro forms error
   private covering
   tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-             WhnfM (Term (S d) n, ScopeTerm (S d) n)
+             Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
   tycasePi (Pi {arg, res, _}) = pure (arg, res)
   tycasePi (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -283,7 +283,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for other intro forms error
   private covering
   tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-              WhnfM (Term (S d) n, ScopeTerm (S d) n)
+              Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
   tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
   tycaseSig (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -301,7 +301,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for other intro forms error
   private covering
   tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-              WhnfM (Term (S d) n)
+              Eff Whnf (Term (S d) n)
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -313,8 +313,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   ||| for other intro forms error
   private covering
   tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
-             WhnfM (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
-                           Term (S d) n, Term (S d) n)
+             Eff Whnf (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
+                       Term (S d) n, Term (S d) n)
   tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
   tycaseEq (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
@@ -336,7 +336,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   private covering
   piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
           (val, s : Term d n) -> Loc ->
-          WhnfM (Subset (Elim d n) (No . isRedexE defs))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   piCoe sty@(S [< i] ty) p q val s loc = do
     -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
     -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@@ -357,7 +357,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   sigCoe : (qty : Qty) ->
            (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
-           WhnfM (Subset (Elim d n) (No . isRedexE defs))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
     -- ⇝
@@ -383,7 +383,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   private covering
   eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
           (r : Dim d) -> Loc ->
-          WhnfM (Subset (Elim d n) (No . isRedexE defs))
+          Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   eqCoe sty@(S [< j] ty) p q val r loc = do
     -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
     -- ⇝
@@ -401,7 +401,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
   boxCoe : (qty : Qty) ->
            (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
-           WhnfM (Subset (Elim d n) (No . isRedexE defs))
+           Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
     -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
     -- ⇝
@@ -421,7 +421,7 @@ reduceTypeCase : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
                  (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
                  (arms : TypeCaseArms d n) -> (def : Term d n) ->
                  (0 _ : So (isTyCon ty)) => Loc ->
-                 WhnfM (Subset (Elim d n) (No . isRedexE defs))
+                 Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
 reduceTypeCase defs ctx ty u ret arms def loc = case ty of
   -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
   TYPE {} =>
@@ -483,7 +483,7 @@ pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
           (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
           Dim d -> Dim d ->
           (s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc ->
-          WhnfM (NonRedex Elim d n defs)
+          Eff Whnf (NonRedex Elim d n defs)
 pushCoe defs ctx i ty p q s loc =
   if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
   case s of
@@ -562,13 +562,13 @@ pushCoe defs ctx i ty p q s loc =
 
     E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah)
 where
-  unwrapTYPE : Term (S d) n -> WhnfM Universe
+  unwrapTYPE : Term (S d) n -> Eff Whnf Universe
   unwrapTYPE (TYPE {l, _}) = pure l
   unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty
 
 
 export covering
-Whnf Elim Reduce.isRedexE where
+CanWhnf Elim Reduce.isRedexE where
   whnf defs ctx (F x u loc) with (lookupElim x defs) proof eq
     _ | Just y  = whnf defs ctx $ setLoc loc $ displace u y
     _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
@@ -725,7 +725,7 @@ Whnf Elim Reduce.isRedexE where
   whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el
 
 export covering
-Whnf Term Reduce.isRedexT where
+CanWhnf Term Reduce.isRedexT where
   whnf _ _ t@(TYPE {}) = pure $ nred t
   whnf _ _ t@(Pi   {}) = pure $ nred t
   whnf _ _ t@(Lam  {}) = pure $ nred t
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 4314c3c..2d0a215 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -69,7 +69,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
   namespace TyContext
    parameters (ctx : TyContext d n) (loc : Loc)
     export covering
-    whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
+    whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
            tm d n -> Eff fs (NonRedex tm d n defs)
     whnf tm = do
       let Val n = ctx.termLen; Val d = ctx.dimLen
@@ -115,7 +115,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
   namespace EqContext
    parameters (ctx : EqContext n) (loc : Loc)
     export covering
-    whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
+    whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
            tm 0 n -> Eff fs (NonRedex tm 0 n defs)
     whnf tm = do
       let Val n = ctx.termLen