From b666bc20cf5b502a8a388dde0a8cffe400ec25c4 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 18 Apr 2023 22:55:23 +0200
Subject: [PATCH] do scope checking in FromParser where it belongs

---
 lib/Quox/Definition.idr              |  27 +--
 lib/Quox/Equal.idr                   |  86 ++++---
 lib/Quox/Parser/FromParser.idr       |  83 ++++---
 lib/Quox/Parser/FromParser/Error.idr |  23 +-
 lib/Quox/Reduce.idr                  | 322 +++++++++++++--------------
 lib/Quox/Typechecker.idr             |  42 ++--
 lib/Quox/Typing.idr                  |  14 +-
 tests/Tests/Equal.idr                |   4 +-
 tests/Tests/FromPTerm.idr            |   9 +-
 tests/Tests/Reduce.idr               |   2 +-
 tests/Tests/Typechecker.idr          |   2 +-
 11 files changed, 305 insertions(+), 309 deletions(-)

diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index e71e9cf..45dd3e7 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -55,40 +55,21 @@ isZero g = g.qty.fst == Zero
 
 
 public export
-data DefEnvTag = NS | DEFS
+data DefEnvTag = DEFS
 
 public export
 Definitions : Type
 Definitions = SortedMap Name Definition
 
-public export
-0 CurNSReader : Type -> Type
-CurNSReader = ReaderL NS Mods
-
 public export
 0 DefsReader : Type -> Type
 DefsReader = ReaderL DEFS Definitions
 
-export
-ns : Has CurNSReader fs => Eff fs Mods
-ns = askAt NS
-
 export
 defs : Has DefsReader fs => Eff fs Definitions
 defs = askAt DEFS
 
 
-public export
-lookupNS : Mods -> Name -> Definitions -> Maybe Definition
-lookupNS [<]           x defs = lookup x defs
-lookupNS mms@(ms :< _) x defs =
-  lookup (addMods mms x) defs <|> lookupNS ms x defs
-
-parameters {d, n : Nat}
-  public export %inline
-  lookupElim : Name -> Definitions -> Maybe (Elim d n)
-  lookupElim x defs = toElim !(lookup x defs)
-
-  public export %inline
-  lookupElimNS : Mods -> Name -> Definitions -> Maybe (Elim d n)
-  lookupElimNS mods x defs = toElim !(lookupNS mods x defs)
+public export %inline
+lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)
+lookupElim x defs = toElim !(lookup x defs)
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 511813c..2db3e83 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -81,19 +81,19 @@ sameTyCon (E    {}) _         = False
 ||| * a box type is a subsingleton if its content is
 public export covering
 isSubSing : Has ErrorEff fs => {n : Nat} ->
-            Mods -> Definitions -> EqContext n -> Term 0 n -> Eff fs Bool
-isSubSing ns defs ctx ty0 = do
-  Element ty0 nc <- whnf ns defs ctx ty0
+            Definitions -> EqContext n -> Term 0 n -> Eff fs Bool
+isSubSing defs ctx ty0 = do
+  Element ty0 nc <- whnf defs ctx ty0
   case ty0 of
     TYPE _        => pure False
-    Pi _ arg res  => isSubSing ns defs (extendTy Zero res.name arg ctx) res.term
-    Sig  fst snd  => isSubSing ns defs ctx fst `andM`
-                     isSubSing ns defs (extendTy Zero snd.name fst ctx) snd.term
+    Pi _ arg res  => isSubSing defs (extendTy Zero res.name arg ctx) res.term
+    Sig  fst snd  => isSubSing defs ctx fst `andM`
+                     isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
     Enum tags     => pure $ length (SortedSet.toList tags) <= 1
     Eq   {}       => pure True
     Nat           => pure False
-    BOX  _ ty     => isSubSing ns defs ctx ty
-    E    (s :# _) => isSubSing ns defs ctx s
+    BOX  _ ty     => isSubSing defs ctx ty
+    E    (s :# _) => isSubSing defs ctx s
     E    _   => pure False
     Lam  _   => pure False
     Pair _ _ => pure False
@@ -116,14 +116,14 @@ ensureTyCon ctx t = case nchoose $ isTyConE t of
 |||
 ||| ⚠ **assumes the elim is already typechecked.** ⚠
 private covering
-computeElimTypeE : (ns : Mods) -> (defs : Definitions) -> EqContext n ->
-                   (e : Elim 0 n) -> (0 ne : NotRedex ns defs e) =>
+computeElimTypeE : (defs : Definitions) -> EqContext n ->
+                   (e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
                    Equal (Term 0 n)
-computeElimTypeE ns defs ectx e =
+computeElimTypeE defs ectx e =
   let Val n = ectx.termLen in
-  rethrow $ computeElimType ns defs (toWhnfContext ectx) e
+  rethrow $ computeElimType defs (toWhnfContext ectx) e
 
-parameters (ns : Mods) (defs : Definitions)
+parameters (defs : Definitions)
   mutual
     namespace Term
       ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
@@ -135,9 +135,9 @@ parameters (ns : Mods) (defs : Definitions)
       compare0 ctx ty s t =
         wrapErr (WhileComparingT ctx !mode ty s t) $ do
           let Val n = ctx.termLen
-          Element ty _ <- whnf ns defs ctx ty
-          Element s  _ <- whnf ns defs ctx s
-          Element t  _ <- whnf ns defs ctx t
+          Element ty _ <- whnf defs ctx ty
+          Element s  _ <- whnf defs ctx s
+          Element t  _ <- whnf defs ctx t
           tty <- ensureTyCon ctx ty
           compare0' ctx ty s t
 
@@ -150,8 +150,8 @@ parameters (ns : Mods) (defs : Definitions)
       private covering
       compare0' : EqContext n ->
                   (ty, s, t : Term 0 n) ->
-                  (0 _ : NotRedex ns defs ty) => (0 _ : So (isTyConE ty)) =>
-                  (0 _ : NotRedex ns defs s)  => (0 _ : NotRedex ns defs t) =>
+                  (0 _ : NotRedex defs ty) => (0 _ : So (isTyConE ty)) =>
+                  (0 _ : NotRedex defs s)  => (0 _ : NotRedex defs t) =>
                   Equal ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
 
@@ -275,8 +275,8 @@ parameters (ns : Mods) (defs : Definitions)
     compareType : EqContext n -> (s, t : Term 0 n) -> Equal ()
     compareType ctx s t = do
       let Val n = ctx.termLen
-      Element s _ <- whnf ns defs ctx s
-      Element t _ <- whnf ns defs ctx t
+      Element s _ <- whnf defs ctx s
+      Element t _ <- whnf defs ctx t
       ts <- ensureTyCon ctx s
       tt <- ensureTyCon ctx t
       st <- either pure (const $ clashTy ctx s t) $ nchoose $ sameTyCon s t
@@ -284,8 +284,8 @@ parameters (ns : Mods) (defs : Definitions)
 
     private covering
     compareType' : EqContext n -> (s, t : Term 0 n) ->
-                   (0 _ : NotRedex ns defs s) => (0 _ : So (isTyConE s)) =>
-                   (0 _ : NotRedex ns defs t) => (0 _ : So (isTyConE t)) =>
+                   (0 _ : NotRedex defs s) => (0 _ : So (isTyConE s)) =>
+                   (0 _ : NotRedex defs t) => (0 _ : So (isTyConE t)) =>
                    (0 _ : So (sameTyCon s t)) =>
                    Equal ()
     -- equality is the same as subtyping, except with the
@@ -349,10 +349,10 @@ parameters (ns : Mods) (defs : Definitions)
 
     private covering
     replaceEnd : EqContext n ->
-                 (e : Elim 0 n) -> DimConst -> (0 ne : NotRedex ns defs e) ->
+                 (e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
                  Equal (Elim 0 n)
     replaceEnd ctx e p ne = do
-      (ty, l, r) <- expectEq ns defs ctx !(computeElimTypeE ns defs ctx e)
+      (ty, l, r) <- expectEq defs ctx !(computeElimTypeE defs ctx e)
       pure $ ends l r p :# dsub1 ty (K p)
 
     namespace Elim
@@ -368,16 +368,16 @@ parameters (ns : Mods) (defs : Definitions)
       compare0 ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
           let Val n = ctx.termLen
-          Element e ne <- whnf ns defs ctx e
-          Element f nf <- whnf ns defs ctx f
+          Element e ne <- whnf defs ctx e
+          Element f nf <- whnf defs ctx f
           -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-          unless !(isSubSing ns defs ctx !(computeElimTypeE ns defs ctx e)) $
+          unless !(isSubSing defs ctx !(computeElimTypeE defs ctx e)) $
             compare0' ctx e f ne nf
 
       private covering
       compare0' : EqContext n ->
                   (e, f : Elim 0 n) ->
-                  (0 ne : NotRedex ns defs e) -> (0 nf : NotRedex ns defs f) ->
+                  (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
                   Equal ()
       -- replace applied equalities with the appropriate end first
       -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
@@ -397,8 +397,8 @@ parameters (ns : Mods) (defs : Definitions)
       compare0' ctx (e :@ s) (f :@ t) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          (_, arg, _) <- expectPi ns defs ctx =<<
-                         computeElimTypeE ns defs ctx e @{noOr1 ne}
+          (_, arg, _) <- expectPi defs ctx =<<
+                         computeElimTypeE defs ctx e @{noOr1 ne}
           Term.compare0 ctx arg s t
       compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f
 
@@ -406,9 +406,9 @@ parameters (ns : Mods) (defs : Definitions)
                     (CasePair fpi f fret fbody) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          (fst, snd) <- expectSig ns defs ctx ety
+          (fst, snd) <- expectSig defs ctx ety
           let [< x, y] = ebody.names
           Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
                         (substCasePairRet ety eret)
@@ -420,9 +420,9 @@ parameters (ns : Mods) (defs : Definitions)
                     (CaseEnum fpi f fret farms) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          for_ !(expectEnum ns defs ctx ety) $ \t =>
+          for_ !(expectEnum defs ctx ety) $ \t =>
             compare0 ctx (sub1 eret $ Tag t :# ety)
               !(lookupArm t earms) !(lookupArm t farms)
           expectEqualQ epi fpi
@@ -437,7 +437,7 @@ parameters (ns : Mods) (defs : Definitions)
                     (CaseNat fpi fpi' f fret fzer fsuc) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           compare0 ctx (sub1 eret (Zero :# Nat)) ezer fzer
           let [< p, ih] = esuc.names
@@ -452,9 +452,9 @@ parameters (ns : Mods) (defs : Definitions)
                     (CaseBox fpi f fret fbody) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          (q, ty) <- expectBOX ns defs ctx ety
+          (q, ty) <- expectBOX defs ctx ety
           compare0 (extendTy (epi * q) ebody.name ty ctx)
             (substCaseBoxRet ety eret)
             ebody.term fbody.term
@@ -480,8 +480,7 @@ parameters (ns : Mods) (defs : Definitions)
                     ne _ =
         local_ Equal $ do
           compare0 ctx ty1 ty2
-          u <- expectTYPE ns defs ctx =<<
-               computeElimTypeE ns defs ctx ty1 @{noOr1 ne}
+          u <- expectTYPE defs ctx =<< computeElimTypeE defs ctx ty1 @{noOr1 ne}
           compareType ctx ret1 ret2
           compareType ctx def1 def2
           for_ allKinds $ \k =>
@@ -550,8 +549,7 @@ parameters (ns : Mods) (defs : Definitions)
         compare0 ctx (weakT 1 ret) b1.term b1.term
 
 
-parameters {auto _ : (Has DefsReader fs, Has CurNSReader fs, Has ErrorEff fs)}
-           (ctx : TyContext d n)
+parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
   -- [todo] only split on the dvars that are actually used anywhere in
   -- the calls to `splits`
 
@@ -563,7 +561,7 @@ parameters {auto _ : (Has DefsReader fs, Has CurNSReader fs, Has ErrorEff fs)}
         map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            lift $ compare0 !ns !defs ectx (ty // th) (s // th) (t // th)
+            lift $ compare0 !defs ectx (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term d n) -> Eff fs ()
@@ -571,7 +569,7 @@ parameters {auto _ : (Has DefsReader fs, Has CurNSReader fs, Has ErrorEff fs)}
         map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            lift $ compareType !ns !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
@@ -582,7 +580,7 @@ parameters {auto _ : (Has DefsReader fs, Has CurNSReader fs, Has ErrorEff fs)}
         map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            lift $ compare0 !ns !defs ectx (e // th) (f // th)
+            lift $ compare0 !defs ectx (e // th) (f // th)
 
   namespace Term
     export covering %inline
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 97639ba..f6a0b99 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -20,8 +20,6 @@ import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
 %hide Typing.Error
 %hide Lexer.Error
 %hide Parser.Error
-%hide Definition.DEFS
-%hide Definition.NS
 
 
 public export
@@ -38,7 +36,12 @@ SeenFiles = SortedSet String
 
 
 public export
-data StateTag = DEFS | NS | SEEN
+data StateTag = NS | SEEN
+
+public export
+0 FromParserPure : List (Type -> Type)
+FromParserPure =
+  [Except Error, StateL DEFS Definitions, StateL NS Mods]
 
 public export
 0 FromParserEff : List (Type -> Type)
@@ -70,16 +73,25 @@ fromPDimWith ds (V i) =
 
 private
 avoidDim : Has (Except Error) fs =>
-           Context' BName d -> PName -> Eff fs (Term d n)
+           Context' BName d -> PName -> Eff fs Name
 avoidDim ds x =
-  fromName (const $ throw $ DimNameInTerm x.base) (pure . FT . fromPName) ds x
+  fromName (const $ throw $ DimNameInTerm x.base) (pure . fromPName) ds x
 
+private
+resolveName : Mods -> Name -> Eff FromParserPure (Term d n)
+resolveName ns x =
+  let here = addMods ns x in
+  if isJust $ lookup here !(getAt DEFS) then
+    pure $ FT here
+  else do
+    let ns :< _ = ns
+      | _ => throw $ TermNotInScope x
+    resolveName ns x
 
 mutual
   export
-  fromPTermWith : Has (Except Error) fs =>
-                  Context' BName d -> Context' BName n ->
-                  PTerm -> Eff fs (Term d n)
+  fromPTermWith : Context' BName d -> Context' BName n ->
+                  PTerm -> Eff FromParserPure (Term d n)
   fromPTermWith ds ns t0 = case t0 of
     TYPE k =>
       pure $ TYPE $ k
@@ -154,7 +166,7 @@ mutual
       map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
 
     V x =>
-      fromName (pure . E . B) (avoidDim ds) ns x
+      fromName (pure . E . B) (resolveName !(getAt NS) <=< avoidDim ds) ns x
 
     s :# a =>
       map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
@@ -177,27 +189,29 @@ mutual
         <*> fromPTermDScope ds ns [< j1] val1
 
   private
-  fromPTermEnumArms : Has (Except Error) fs =>
-                      Context' BName d -> Context' BName n ->
-                      List (TagVal, PTerm) -> Eff fs (CaseEnumArms d n)
+  fromPTermEnumArms : Context' BName d -> Context' BName n ->
+                      List (TagVal, PTerm) ->
+                      Eff FromParserPure (CaseEnumArms d n)
   fromPTermEnumArms ds ns =
     map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
 
   private
-  fromPTermElim : Has (Except Error) fs =>
-                  Context' BName d -> Context' BName n ->
-                  PTerm -> Eff fs (Elim d n)
+  fromPTermElim : Context' BName d -> Context' BName n ->
+                  PTerm -> Eff FromParserPure (Elim d n)
   fromPTermElim ds ns e =
     case !(fromPTermWith ds ns e) of
       E e => pure e
-      _   => throw $ AnnotationNeeded e
+      t   => let ctx = MkNameContexts (map name ds) (map name ns) in
+             throw $ AnnotationNeeded ctx t
+  where
+    name : BName -> BaseName
+    name = maybe Unused UN
 
   -- [todo] use SN if the var is named but still unused
   private
-  fromPTermTScope : {s : Nat} -> Has (Except Error) fs =>
-                    Context' BName d -> Context' BName n ->
-                    SnocVect s BName ->
-                    PTerm -> Eff fs (ScopeTermN s d n)
+  fromPTermTScope : {s : Nat} -> Context' BName d -> Context' BName n ->
+                    SnocVect s BName -> PTerm ->
+                    Eff FromParserPure (ScopeTermN s d n)
   fromPTermTScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
@@ -206,10 +220,9 @@ mutual
         <$> fromPTermWith ds (ns ++ xs) t
 
   private
-  fromPTermDScope : {s : Nat} -> Has (Except Error) fs =>
-                    Context' BName d -> Context' BName n ->
-                    SnocVect s BName ->
-                    PTerm -> Eff fs (DScopeTermN s d n)
+  fromPTermDScope : {s : Nat} -> Context' BName d -> Context' BName n ->
+                    SnocVect s BName -> PTerm ->
+                    Eff FromParserPure (DScopeTermN s d n)
   fromPTermDScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
@@ -219,7 +232,7 @@ mutual
 
 
 export %inline
-fromPTerm : Has (Except Error) fs => PTerm -> Eff fs (Term 0 0)
+fromPTerm : PTerm -> Eff FromParserPure (Term 0 0)
 fromPTerm = fromPTermWith [<] [<]
 
 
@@ -236,10 +249,9 @@ fromPNameNS : Has (StateL NS Mods) fs => PName -> Eff fs Name
 fromPNameNS name = pure $ addMods !(getAt NS) $ fromPName name
 
 private
-injTC : (Has (StateL DEFS Definitions) fs, Has (StateL NS Mods) fs,
-         Has (Except Error) fs) =>
+injTC : (Has (StateL DEFS Definitions) fs, Has (Except Error) fs) =>
         TC a -> Eff fs a
-injTC act = rethrow $ mapFst TypeError $ runTC !(getAt NS) !(getAt DEFS) act
+injTC act = rethrow $ mapFst TypeError $ runTC !(getAt DEFS) act
 
 export covering
 fromPDef : (Has (StateL DEFS Definitions) fs,
@@ -251,8 +263,8 @@ fromPDef (MkPDef qty pname ptype pterm) = do
   qtyGlobal <- globalPQty qty
   let gqty = Element qty qtyGlobal
   let sqty = globalToSubj gqty
-  type <- traverse fromPTerm ptype
-  term <- fromPTerm pterm
+  type <- lift $ traverse fromPTerm ptype
+  term <- lift $ fromPTerm pterm
   case type of
     Just type => do
       injTC $ checkTypeC empty type Nothing
@@ -261,7 +273,7 @@ fromPDef (MkPDef qty pname ptype pterm) = do
       modifyAt DEFS $ insert name def
       pure (name, def)
     Nothing => do
-      let E elim = term | _ => throw $ AnnotationNeeded pterm
+      let E elim = term | t => throw $ AnnotationNeeded empty t
       res <- injTC $ inferC empty sqty elim
       let def = mkDef gqty res.type term
       modifyAt DEFS $ insert name def
@@ -315,6 +327,15 @@ parameters {auto _ : (Has IO fs,
   fromPTopLevel (PD    decl) = fromPDecl decl
   fromPTopLevel (PLoad file) = loadProcessFile file
 
+export
+fromParserPure : Definitions ->
+                 Eff FromParserPure a ->
+                 Either Error (a, Definitions)
+fromParserPure defs act =
+  extract $
+  runExcept $
+  evalStateAt NS [<] $
+  runStateAt DEFS defs act
 
 export
 fromParserIO : (MonadRec io, HasIO io) =>
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index d4d20ec..52d3f0a 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -9,8 +9,9 @@ import Quox.Pretty
 
 public export
 data Error =
-    AnnotationNeeded PTerm
+    AnnotationNeeded (NameContexts d n) (Term d n)
   | DuplicatesInEnum (List TagVal)
+  | TermNotInScope Name
   | DimNotInScope PBaseName
   | QtyNotGlobal Qty
   | DimNameInTerm PBaseName
@@ -25,17 +26,19 @@ data Error =
 parameters (unicode, showContext : Bool)
   export
   prettyError : Error -> Doc HL
-  prettyError (AnnotationNeeded tm) =
-    sep ["the term", "«PTerm»", -- pretty0 unicode tm,
+  prettyError (AnnotationNeeded ctx tm) =
+    sep ["the term", prettyTerm unicode ctx.dnames ctx.tnames tm,
          "needs a type annotation"]
+    -- [todo] print the original PTerm instead
 
   prettyError (DuplicatesInEnum tags) =
-    sep ["duplicate tags in enum type",
-         braces $ fillSep $ map pretty tags]
+    sep ["duplicate tags in enum type", braces $ fillSep $ map pretty tags]
 
   prettyError (DimNotInScope i) =
-    sep ["dimension", pretty0 unicode $ DV $ fromString i,
-         "not in scope"]
+    sep ["dimension", pretty0 unicode $ DV $ fromString i, "not in scope"]
+
+  prettyError (TermNotInScope x) =
+    sep ["term variable", pretty0 unicode $ F x {d = 0, n = 0}, "not in scope"]
 
   prettyError (QtyNotGlobal pi) =
     sep ["quantity", pretty0 unicode pi,
@@ -46,12 +49,10 @@ parameters (unicode, showContext : Bool)
          "used in a term context"]
 
   prettyError (TypeError err) =
-    Typing.prettyError unicode showContext $
-    trimContext 2 err
+    Typing.prettyError unicode showContext $ trimContext 2 err
 
   prettyError (LoadError str err) =
-    vsep [hsep ["couldn't load file", pretty str],
-          "«FileError»"]
+    vsep [hsep ["couldn't load file", pretty str], fromString $ show err]
 
   prettyError (ParseError err) =
     pretty $ show err
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index d9499d0..baa1306 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -14,37 +14,36 @@ import Data.List
 
 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = {d, n : Nat} -> Mods -> Definitions -> tm d n -> Bool
+RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
 
 public export
 interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
-  whnf : {d, n : Nat} -> (ns : Mods) -> (defs : Definitions) ->
+  whnf : {d, n : Nat} -> (defs : Definitions) ->
          (ctx : WhnfContext d n) ->
-         tm d n -> Either Error (Subset (tm d n) (No . isRedex ns defs))
+         tm d n -> Either Error (Subset (tm d n) (No . isRedex defs))
 
 public export %inline
 whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-        (ns : Mods) -> (defs : Definitions) ->
+        (defs : Definitions) ->
         WhnfContext d n -> tm d n -> Either Error (tm d n)
-whnf0 ns defs ctx t = fst <$> whnf ns defs ctx t
+whnf0 defs ctx t = fst <$> whnf defs ctx t
 
 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
-                      Mods -> Definitions -> Pred (tm d n)
-IsRedex  ns defs = So . isRedex ns defs
-NotRedex ns defs = No . isRedex ns defs
+                      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) ->
-             (ns : Mods) -> (defs : Definitions) -> Type
-NonRedex tm d n ns defs = Subset (tm d n) (NotRedex ns defs)
+             (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) =>
-       (t : tm d n) -> (0 nr : NotRedex ns defs t) =>
-       NonRedex tm d n ns defs
+       (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
 nred t = Element t nr
 
 
@@ -136,38 +135,38 @@ isK _     = False
 mutual
   public export
   isRedexE : RedexTest Elim
-  isRedexE ns defs (F x) {d, n} =
-    isJust $ lookupElimNS ns x defs {d, n}
-  isRedexE _ _ (B _) = False
-  isRedexE ns defs (f :@ _) =
-    isRedexE ns defs f || isLamHead f
-  isRedexE ns defs (CasePair {pair, _}) =
-    isRedexE ns defs pair || isPairHead pair
-  isRedexE ns defs (CaseEnum {tag, _}) =
-    isRedexE ns defs tag || isTagHead tag
-  isRedexE ns defs (CaseNat {nat, _}) =
-    isRedexE ns defs nat || isNatHead nat
-  isRedexE ns defs (CaseBox {box, _}) =
-    isRedexE ns defs box || isBoxHead box
-  isRedexE ns defs (f :% p) =
-    isRedexE ns defs f || isDLamHead f || isK p
-  isRedexE ns defs (t :# a) =
-    isE t || isRedexT ns defs t || isRedexT ns defs a
-  isRedexE ns defs (Coe {val, _}) =
-    isRedexT ns defs val || not (isE val)
-  isRedexE ns defs (Comp {ty, r, _}) =
-    isRedexT ns defs ty || isK r
-  isRedexE ns defs (TypeCase {ty, ret, _}) =
-    isRedexE ns defs ty || isRedexT ns defs ret || isAnnTyCon ty
-  isRedexE _ _ (CloE  {}) = True
-  isRedexE _ _ (DCloE {}) = True
+  isRedexE defs (F x) {d, n} =
+    isJust $ lookupElim x defs {d, n}
+  isRedexE _ (B _) = False
+  isRedexE defs (f :@ _) =
+    isRedexE defs f || isLamHead f
+  isRedexE defs (CasePair {pair, _}) =
+    isRedexE defs pair || isPairHead pair
+  isRedexE defs (CaseEnum {tag, _}) =
+    isRedexE defs tag || isTagHead tag
+  isRedexE defs (CaseNat {nat, _}) =
+    isRedexE defs nat || isNatHead nat
+  isRedexE defs (CaseBox {box, _}) =
+    isRedexE defs box || isBoxHead box
+  isRedexE defs (f :% p) =
+    isRedexE defs f || isDLamHead f || isK p
+  isRedexE defs (t :# a) =
+    isE t || isRedexT defs t || isRedexT defs a
+  isRedexE defs (Coe {val, _}) =
+    isRedexT defs val || not (isE val)
+  isRedexE defs (Comp {ty, r, _}) =
+    isRedexT defs ty || isK r
+  isRedexE defs (TypeCase {ty, ret, _}) =
+    isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
+  isRedexE _ (CloE  {}) = True
+  isRedexE _ (DCloE {}) = True
 
   public export
   isRedexT : RedexTest Term
-  isRedexT _  _    (CloT  {}) = True
-  isRedexT _  _    (DCloT {}) = True
-  isRedexT ns defs (E e)      = isAnn e || isRedexE ns defs e
-  isRedexT _  _    _          = False
+  isRedexT _    (CloT  {}) = True
+  isRedexT _    (DCloT {}) = True
+  isRedexT defs (E e)      = isAnn e || isRedexE defs e
+  isRedexT _    _          = False
 
 
 public export
@@ -213,23 +212,21 @@ coeScoped ty p q (S names (N body)) =
 
 
 mutual
-  parameters {d, n : Nat} (ns : Mods) (defs : Definitions)
-             (ctx : WhnfContext d n)
+  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     ||| performs the minimum work required to recompute the type of an elim.
     |||
     ||| ⚠ **assumes the elim is already typechecked.** ⚠
     export covering
-    computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE ns defs e)) =>
+    computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
                       Either Error (Term d n)
     computeElimType (F x) = do
-      let Just def = lookupNS ns x defs | Nothing => Left $ NotInScope x
+      let Just def = lookup x defs | Nothing => Left $ NotInScope x
       pure $ def.type
     computeElimType (B i) = pure $ ctx.tctx !! i
     computeElimType (f :@ s) {ne} = do
       -- can't use `expectPi` (or `expectEq` below) without making this
       -- mutual block from hell even worse lol
-      Pi {arg, res, _} <- whnf0 ns defs ctx =<<
-                          computeElimType f {ne = noOr1 ne}
+      Pi {arg, res, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
         | t => Left $ ExpectedPi ctx.names t
       pure $ sub1 res (s :# arg)
     computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
@@ -237,7 +234,7 @@ mutual
     computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
     computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
     computeElimType (f :% p) {ne} = do
-      Eq {ty, _} <- whnf0 ns defs ctx =<< computeElimType f {ne = noOr1 ne}
+      Eq {ty, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
         | t => Left $ ExpectedEq ctx.names t
       pure $ dsub1 ty p
     computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q
@@ -245,17 +242,16 @@ mutual
     computeElimType (TypeCase {ret, _}) = pure ret
     computeElimType (_ :# ty) = pure ty
 
-  parameters {d, n : Nat} (ns : Mods) (defs : Definitions)
-             (ctx : WhnfContext (S d) n)
+  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
     ||| for π.(x : A) → B, returns (A, B);
     ||| for an elim returns a pair of type-cases that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
+    tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
                Either Error (Term (S d) n, ScopeTerm (S d) n)
     tycasePi (Pi {arg, res, _}) = pure (arg, res)
     tycasePi (E e) {tnf} = do
-      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
+      ty <- computeElimType defs ctx e @{noOr2 tnf}
       let arg  = E $ typeCase1Y e ty KPi [< "Arg", "Ret"] (BVT 1)
           res' = typeCase1Y e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
           res  = SY [< "Arg"] $ E $ weakE 1 res' :@ BVT 0
@@ -266,11 +262,11 @@ mutual
     ||| for an elim returns a pair of type-cases that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
+    tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
                 Either Error (Term (S d) n, ScopeTerm (S d) n)
     tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
     tycaseSig (E e) {tnf} = do
-      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
+      ty <- computeElimType defs ctx e @{noOr2 tnf}
       let fst  = E $ typeCase1Y e ty KSig [< "Fst", "Snd"] (BVT 1)
           snd' = typeCase1Y e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
           snd  = SY [< "Fst"] $ E $ weakE 1 snd' :@ BVT 0
@@ -281,11 +277,11 @@ mutual
     ||| for an elim returns a type-case that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
+    tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
                 Either Error (Term (S d) n)
     tycaseBOX (BOX _ a) = pure a
     tycaseBOX (E e) {tnf} = do
-      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
+      ty <- computeElimType defs ctx e @{noOr2 tnf}
       pure $ E $ typeCase1Y e ty KBOX [< "Ty"] (BVT 0)
     tycaseBOX t = Left $ ExpectedBOX ctx.names t
 
@@ -293,12 +289,12 @@ mutual
     ||| for an elim returns five type-cases that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
+    tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
                Either Error (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 ns defs ctx e @{noOr2 tnf}
+      ty <- computeElimType defs ctx e @{noOr2 tnf}
       let names = [< "A0", "A1", "A", "L", "R"]
           a0 = E $ typeCase1Y e ty KEq names (BVT 4)
           a1 = E $ typeCase1Y e ty KEq names (BVT 3)
@@ -311,12 +307,11 @@ mutual
 
   -- new block because the functions below might pass a different ctx
   -- into the ones above
-  parameters {d, n : Nat} (ns : Mods) (defs : Definitions)
-             (ctx : WhnfContext d n)
+  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     ||| reduce a function application `Coe ty p q val :@ s`
     private covering
     piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val, s : Term d n) ->
-            Either Error (Subset (Elim d n) (No . isRedexE ns defs))
+            Either Error (Subset (Elim d n) (No . isRedexE defs))
     piCoe sty@(S [< i] ty) p q val s = do
       -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
       -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@@ -324,20 +319,20 @@ mutual
       --
       -- type-case is used to expose A,B if the type is neutral
       let ctx1 = extendDim i ctx
-      Element ty tynf <- whnf ns defs ctx1 ty.term
-      (arg, res) <- tycasePi ns defs ctx1 ty
+      Element ty tynf <- whnf defs ctx1 ty.term
+      (arg, res) <- tycasePi defs ctx1 ty
       let s0   = CoeT i arg q p s
           body = E $ (val :# (ty // one p)) :@ E s0
           s1   = CoeT i (arg // (BV 0 ::: shift 2)) (weakD 1 q) (BV 0)
                       (s // shift 1)
-      whnf ns defs ctx $ CoeT i (sub1 res s1) p q body
+      whnf defs ctx $ CoeT i (sub1 res s1) p q body
 
     ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body`
     private covering
     sigCoe : (qty : Qty) ->
              (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
              (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) ->
-             Either Error (Subset (Elim d n) (No . isRedexE ns defs))
+             Either Error (Subset (Elim d n) (No . isRedexE defs))
     sigCoe qty sty@(S [< i] ty) p q val ret body = do
       -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
       -- ⇝
@@ -348,101 +343,101 @@ mutual
       --
       -- type-case is used to expose A,B if the type is neutral
       let ctx1 = extendDim i ctx
-      Element ty tynf <- whnf ns defs ctx1 ty.term
-      (tfst, tsnd) <- tycaseSig ns defs ctx1 ty
+      Element ty tynf <- whnf defs ctx1 ty.term
+      (tfst, tsnd) <- tycaseSig defs ctx1 ty
       let a' = CoeT i (weakT 2 tfst) p q (BVT 1)
           tsnd' = tsnd.term //
             (CoeT i (weakT 2 $ tfst // (BV 0 ::: shift 2))
               (weakD 1 p) (BV 0) (BVT 1) ::: shift 2)
           b' = CoeT i tsnd' p q (BVT 0)
-      whnf ns defs ctx $ CasePair qty (val :# (ty // one p)) ret $
+      whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $
         ST body.names $ body.term // (a' ::: b' ::: shift 2)
 
     ||| reduce a dimension application `Coe ty p q val :% r`
     private covering
     eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
             (r : Dim d) ->
-            Either Error (Subset (Elim d n) (No . isRedexE ns defs))
+            Either Error (Subset (Elim d n) (No . isRedexE defs))
     eqCoe sty@(S [< j] ty) p q val r = do
       -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
       -- ⇝
       -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
       --   { (r=0) j ⇒ L; (r=1) j ⇒ R }
       let ctx1 = extendDim j ctx
-      Element ty tynf <- whnf ns defs ctx1 ty.term
-      (a0, a1, a, s, t) <- tycaseEq ns defs ctx1 ty
+      Element ty tynf <- whnf defs ctx1 ty.term
+      (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
       let a'   = dsub1 a (weakD 1 r)
           val' = E $ (val :# (ty // one p)) :% r
-      whnf ns defs ctx $ CompH j a' p q val' r j s j t
+      whnf defs ctx $ CompH j a' p q val' r j s j t
 
     ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
     private covering
     boxCoe : (qty : Qty) ->
              (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
              (ret : ScopeTerm d n) -> (body : ScopeTerm d n) ->
-             Either Error (Subset (Elim d n) (No . isRedexE ns defs))
+             Either Error (Subset (Elim d n) (No . isRedexE defs))
     boxCoe qty sty@(S [< i] ty) p q val ret body = do
       -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
       -- ⇝
       -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C
       -- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
       let ctx1 = extendDim i ctx
-      Element ty tynf <- whnf ns defs ctx1 ty.term
-      ta <- tycaseBOX ns defs ctx1 ty
+      Element ty tynf <- whnf defs ctx1 ty.term
+      ta <- tycaseBOX defs ctx1 ty
       let a' = CoeT i (weakT 1 ta) p q $ BVT 0
-      whnf ns defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
+      whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
         ST body.names $ body.term // (a' ::: shift 1)
 
 
   export covering
   Whnf Elim Reduce.isRedexE where
-    whnf ns defs ctx (F x) with (lookupElimNS ns x defs) proof eq
-      _ | Just y  = whnf ns defs ctx y
+    whnf defs ctx (F x) with (lookupElim x defs) proof eq
+      _ | Just y  = whnf defs ctx y
       _ | Nothing = pure $ Element (F x) $ rewrite eq in Ah
 
-    whnf _ _ _ (B i) = pure $ nred $ B i
+    whnf _ _ (B i) = pure $ nred $ B i
 
     -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
-    whnf ns defs ctx (f :@ s) = do
-      Element f fnf <- whnf ns defs ctx f
+    whnf defs ctx (f :@ s) = do
+      Element f fnf <- whnf defs ctx f
       case nchoose $ isLamHead f of
         Left _ => case f of
           Lam body :# Pi {arg, res, _} =>
             let s = s :# arg in
-            whnf ns defs ctx $ sub1 body s :# sub1 res s
-          Coe ty p q val => piCoe ns defs ctx ty p q val s
+            whnf defs ctx $ sub1 body s :# sub1 res s
+          Coe ty p q val => piCoe defs ctx ty p q val s
         Right nlh => pure $ Element (f :@ s) $ fnf `orNo` nlh
 
     -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
     -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
-    whnf ns defs ctx (CasePair pi pair ret body) = do
-      Element pair pairnf <- whnf ns defs ctx pair
+    whnf defs ctx (CasePair pi pair ret body) = do
+      Element pair pairnf <- whnf defs ctx pair
       case nchoose $ isPairHead pair of
         Left _ => case pair of
           Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} =>
             let fst = fst :# tfst
                 snd = snd :# sub1 tsnd fst
             in
-            whnf ns defs ctx $ subN body [< fst, snd] :# sub1 ret pair
+            whnf defs ctx $ subN body [< fst, snd] :# sub1 ret pair
           Coe ty p q val => do
-            sigCoe ns defs ctx pi ty p q val ret body
+            sigCoe defs ctx pi ty p q val ret body
         Right np =>
           pure $ Element (CasePair pi pair ret body) $ pairnf `orNo` np
 
     -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
     -- u ∷ C['a∷{a,…}/p]
-    whnf ns defs ctx (CaseEnum pi tag ret arms) = do
-      Element tag tagnf <- whnf ns defs ctx tag
+    whnf defs ctx (CaseEnum pi tag ret arms) = do
+      Element tag tagnf <- whnf defs ctx tag
       case nchoose $ isTagHead tag of
         Left t => case tag of
           Tag t :# Enum ts =>
             let ty = sub1 ret tag in
             case lookup t arms of
-              Just arm => whnf ns defs ctx $ arm :# ty
+              Just arm => whnf defs ctx $ arm :# ty
               Nothing  => Left $ MissingEnumArm t (keys arms)
           Coe ty p q val =>
             -- there is nowhere an equality can be hiding inside an Enum
-            whnf ns defs ctx $ CaseEnum pi (val :# dsub1 ty q) ret arms
+            whnf defs ctx $ CaseEnum pi (val :# dsub1 ty q) ret arms
         Right nt =>
           pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
 
@@ -451,35 +446,35 @@ mutual
     --
     -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
     --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-    whnf ns defs ctx (CaseNat pi piIH nat ret zer suc) = do
-      Element nat natnf <- whnf ns defs ctx nat
+    whnf defs ctx (CaseNat pi piIH nat ret zer suc) = do
+      Element nat natnf <- whnf defs ctx nat
       case nchoose $ isNatHead nat of
         Left _ =>
           let ty = sub1 ret nat in
           case nat of
-            Zero :# Nat => whnf ns defs ctx (zer :# ty)
+            Zero :# Nat => whnf defs ctx (zer :# ty)
             Succ n :# Nat =>
               let nn = n :# Nat
                   tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc]
               in
-              whnf ns defs ctx $ tm :# ty
+              whnf defs ctx $ tm :# ty
             Coe ty p q val =>
               -- same deal as Enum
-              whnf ns defs ctx $ CaseNat pi piIH (val :# dsub1 ty q) ret zer suc
+              whnf defs ctx $ CaseNat pi piIH (val :# dsub1 ty q) ret zer suc
         Right nn =>
           pure $ Element (CaseNat pi piIH nat ret zer suc) $ natnf `orNo` nn
 
     -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
     --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
-    whnf ns defs ctx (CaseBox pi box ret body) = do
-      Element box boxnf <- whnf ns defs ctx box
+    whnf defs ctx (CaseBox pi box ret body) = do
+      Element box boxnf <- whnf defs ctx box
       case nchoose $ isBoxHead box of
         Left _ => case box of
           Box val :# BOX q bty =>
             let ty = sub1 ret box in
-            whnf ns defs ctx $ sub1 body (val :# bty) :# ty
+            whnf defs ctx $ sub1 body (val :# bty) :# ty
           Coe ty p q val =>
-            boxCoe ns defs ctx pi ty p q val ret body
+            boxCoe defs ctx pi ty p q val ret body
         Right nb =>
           pure $ Element (CaseBox pi box ret body) $ boxnf `orNo` nb
 
@@ -487,104 +482,102 @@ mutual
     -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗›
     -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
     --   (if 𝑘 is a variable)
-    whnf ns defs ctx (f :% p) = do
-      Element f fnf <- whnf ns defs ctx f
+    whnf defs ctx (f :% p) = do
+      Element f fnf <- whnf defs ctx f
       case nchoose $ isDLamHead f of
         Left _ => case f of
           DLam body :# Eq {ty = ty, l, r, _} =>
             let body = endsOr l r (dsub1 body p) p in
-            whnf ns defs ctx $ body :# dsub1 ty p
+            whnf defs ctx $ body :# dsub1 ty p
           Coe ty p' q' val =>
-            eqCoe ns defs ctx ty p' q' val p
+            eqCoe defs ctx ty p' q' val p
         Right ndlh => case p of
           K e => do
-            Eq {l, r, ty, _} <- whnf0 ns defs ctx =<<
-                                computeElimType ns defs ctx f
+            Eq {l, r, ty, _} <- whnf0 defs ctx =<< computeElimType defs ctx f
               | ty => Left $ ExpectedEq ctx.names ty
-            whnf ns defs ctx $ ends (l :# ty.zero) (r :# ty.one) e
+            whnf defs ctx $ ends (l :# ty.zero) (r :# ty.one) e
           B _ => pure $ Element (f :% p) $ fnf `orNo` ndlh `orNo` Ah
 
     -- e ∷ A ⇝ e
-    whnf ns defs ctx (s :# a) = do
-      Element s snf <- whnf ns defs ctx s
+    whnf defs ctx (s :# a) = do
+      Element s snf <- whnf defs ctx s
       case nchoose $ isE s of
         Left  _  => let E e = s in pure $ Element e $ noOr2 snf
         Right ne => do
-          Element a anf <- whnf ns defs ctx a
+          Element a anf <- whnf defs ctx a
           pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf
 
-    whnf ns defs ctx (Coe (S _ (N ty)) _ _ val) =
-      whnf ns defs ctx $ val :# ty
-    whnf ns defs ctx (Coe (S [< i] ty) p q val) = do
-      Element ty  tynf  <- whnf ns defs (extendDim i ctx) ty.term
-      Element val valnf <- whnf ns defs ctx val
-      pushCoe ns defs ctx i ty p q val
+    whnf defs ctx (Coe (S _ (N ty)) _ _ val) =
+      whnf defs ctx $ val :# ty
+    whnf defs ctx (Coe (S [< i] ty) p q val) = do
+      Element ty  tynf  <- whnf defs (extendDim i ctx) ty.term
+      Element val valnf <- whnf defs ctx val
+      pushCoe defs ctx i ty p q val
 
-    whnf ns defs ctx (Comp ty p q val r zero one) =
+    whnf defs ctx (Comp ty p q val r zero one) =
       -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
-      if p == q then whnf ns defs ctx $ val :# ty else
+      if p == q then whnf defs ctx $ val :# ty else
       case nchoose (isK r) of
         -- comp [A] @p @q s { (0=0) j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
         -- comp [A] @p @q s { (1=1) j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
         Left y => case r of
-          K Zero => whnf ns defs ctx $ dsub1 zero q :# ty
-          K One  => whnf ns defs ctx $ dsub1 one  q :# ty
+          K Zero => whnf defs ctx $ dsub1 zero q :# ty
+          K One  => whnf defs ctx $ dsub1 one  q :# ty
         Right nk => do
-          Element ty tynf <- whnf ns defs ctx ty
+          Element ty tynf <- whnf defs ctx ty
           pure $ Element (Comp ty p q val r zero one) $ tynf `orNo` nk
       -- [todo] anything other than just the boundaries??
 
-    whnf ns defs ctx (TypeCase ty ret arms def) = do
-      Element ty  tynf  <- whnf ns defs ctx ty
-      Element ret retnf <- whnf ns defs ctx ret
+    whnf defs ctx (TypeCase ty ret arms def) = do
+      Element ty  tynf  <- whnf defs ctx ty
+      Element ret retnf <- whnf defs ctx ret
       case nchoose $ isAnnTyCon ty of
         Left  y  => let ty :# TYPE u = ty in
-                    reduceTypeCase ns defs ctx ty u ret arms def
+                    reduceTypeCase defs ctx ty u ret arms def
         Right nt => pure $ Element (TypeCase ty ret arms def) $
                              tynf `orNo` retnf `orNo` nt
 
-    whnf ns defs ctx (CloE  el th) = whnf ns defs ctx $ pushSubstsWith' id th el
-    whnf ns defs ctx (DCloE el th) = whnf ns defs ctx $ pushSubstsWith' th id el
+    whnf defs ctx (CloE  el th) = whnf defs ctx $ pushSubstsWith' id th el
+    whnf defs ctx (DCloE el th) = whnf defs ctx $ pushSubstsWith' th id el
 
   export covering
   Whnf Term Reduce.isRedexT where
-    whnf _ _ _ t@(TYPE {}) = 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 _ _ _    Nat      = pure $ nred Nat
-    whnf _ _ _    Zero     = pure $ nred Zero
-    whnf _ _ _ t@(Succ {}) = pure $ nred t
-    whnf _ _ _ t@(BOX  {}) = pure $ nred t
-    whnf _ _ _ t@(Box  {}) = pure $ nred t
+    whnf _ _ t@(TYPE {}) = 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 _ _    Nat      = pure $ nred Nat
+    whnf _ _    Zero     = pure $ nred Zero
+    whnf _ _ t@(Succ {}) = pure $ nred t
+    whnf _ _ t@(BOX  {}) = pure $ nred t
+    whnf _ _ t@(Box  {}) = pure $ nred t
 
     -- s ∷ A ⇝ s   (in term context)
-    whnf ns defs ctx (E e) = do
-      Element e enf <- whnf ns defs ctx e
+    whnf defs ctx (E e) = do
+      Element e enf <- whnf defs ctx e
       case nchoose $ isAnn e of
         Left  _  => let tm :# _ = e in pure $ Element tm $ noOr1 $ noOr2 enf
         Right na => pure $ Element (E e) $ na `orNo` enf
 
-    whnf ns defs ctx (CloT  tm th) = whnf ns defs ctx $ pushSubstsWith' id th tm
-    whnf ns defs ctx (DCloT tm th) = whnf ns defs ctx $ pushSubstsWith' th id tm
+    whnf defs ctx (CloT  tm th) = whnf defs ctx $ pushSubstsWith' id th tm
+    whnf defs ctx (DCloT tm th) = whnf defs ctx $ pushSubstsWith' th id tm
 
   ||| reduce a type-case applied to a type constructor
   private covering
-  reduceTypeCase : {d, n : Nat} -> (ns : Mods) -> (defs : Definitions) ->
-                   WhnfContext d n ->
+  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)) =>
-                   Either Error (Subset (Elim d n) (No . isRedexE ns defs))
-  reduceTypeCase ns defs ctx ty u ret arms def = case ty of
+                   Either Error (Subset (Elim d n) (No . isRedexE defs))
+  reduceTypeCase defs ctx ty u ret arms def = case ty of
     -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
     TYPE _ =>
-      whnf ns defs ctx $ tycaseRhsDef0 def KTYPE arms :# ret
+      whnf defs ctx $ tycaseRhsDef0 def KTYPE arms :# ret
 
     -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
@@ -592,7 +585,7 @@ mutual
       let arg = arg :# TYPE u
           res = Lam res :# Arr Zero (TYPE u) (TYPE u)
       in
-      whnf ns defs ctx $ subN (tycaseRhsDef def KPi arms) [< arg, res] :# ret
+      whnf defs ctx $ subN (tycaseRhsDef def KPi arms) [< arg, res] :# ret
 
     -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
@@ -600,11 +593,11 @@ mutual
       let fst = fst :# TYPE u
           snd = Lam snd :# Arr Zero (TYPE u) (TYPE u)
       in
-      whnf ns defs ctx $ subN (tycaseRhsDef def KSig arms) [< fst, snd] :# ret
+      whnf defs ctx $ subN (tycaseRhsDef def KSig arms) [< fst, snd] :# ret
 
     -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
     Enum _ =>
-      whnf ns defs ctx $ tycaseRhsDef0 def KEnum arms :# ret
+      whnf defs ctx $ tycaseRhsDef0 def KEnum arms :# ret
 
     -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
     --  of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
@@ -613,7 +606,7 @@ mutual
     --   (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
     Eq a l r =>
       let a0 = a.zero; a1 = a.one in
-      whnf ns defs ctx $
+      whnf defs ctx $
         subN (tycaseRhsDef def KEq arms)
           [< a0 :# TYPE u, a1 :# TYPE u,
              DLam a :# Eq0 (TYPE u) a0 a1, l :# a0, r :# a1]
@@ -621,23 +614,22 @@ mutual
 
     -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
     Nat =>
-      whnf ns defs ctx $ tycaseRhsDef0 def KNat arms :# ret
+      whnf defs ctx $ tycaseRhsDef0 def KNat arms :# ret
 
     -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
     BOX _ s =>
-      whnf ns defs ctx $ sub1 (tycaseRhsDef def KBOX arms) (s :# TYPE u) :# ret
+      whnf defs ctx $ sub1 (tycaseRhsDef def KBOX arms) (s :# TYPE u) :# ret
 
   ||| pushes a coercion inside a whnf-ed term
   private covering
-  pushCoe : {n, d : Nat} -> (ns : Mods) -> (defs : Definitions) ->
-            WhnfContext d n ->
+  pushCoe : {n, d : Nat} -> (defs : Definitions) -> WhnfContext d n ->
             BaseName ->
-            (ty : Term (S d) n) -> (0 tynf : No (isRedexT ns defs ty)) =>
+            (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
             Dim d -> Dim d ->
-            (s : Term d n) -> (0 snf : No (isRedexT ns defs s)) =>
-            Either Error (NonRedex Elim d n ns defs)
-  pushCoe ns defs ctx i ty p q s =
-    if p == q then whnf ns defs ctx $ s :# (ty // one q) else
+            (s : Term d n) -> (0 snf : No (isRedexT defs s)) =>
+            Either Error (NonRedex Elim d n defs)
+  pushCoe defs ctx i ty p q s =
+    if p == q then whnf defs ctx $ s :# (ty // one q) else
     case s of
       -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
       TYPE {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
@@ -654,7 +646,7 @@ mutual
         let body' = CoeT i ty p q $ Lam body
             term' = [< "y"] :\\ E (weakE 1 body' :@ BVT 0)
             type' = ty // one q
-        whnf ns defs ctx $ term' :# type'
+        whnf defs ctx $ term' :# type'
 
       {-
       -- maybe:
@@ -692,7 +684,7 @@ mutual
         let body' = CoeT i ty p q $ DLam body
             term' = [< "j"] :\\% E (dweakE 1 body' :% BV 0)
             type' = ty // one q
-        whnf ns defs ctx $ term' :# type'
+        whnf defs ctx $ term' :# type'
 
       -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
       Tag tag => do
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 4b12aa0..6a1a418 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -13,16 +13,16 @@ import Quox.EffExtra
 
 public export
 0 TCEff : List (Type -> Type)
-TCEff = [ErrorEff, DefsReader, CurNSReader]
+TCEff = [ErrorEff, DefsReader]
 
 public export
 0 TC : Type -> Type
 TC = Eff TCEff
 
 export
-runTC : Mods -> Definitions -> TC a -> Either Error a
-runTC ns defs =
-  extract . runExcept . runReaderAt DEFS defs . runReaderAt NS ns
+runTC : Definitions -> TC a -> Either Error a
+runTC defs =
+  extract . runExcept . runReaderAt DEFS defs
 
 
 export
@@ -149,7 +149,7 @@ mutual
                 (subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
                 TC (CheckResult' n)
   toCheckType ctx sg t ty = do
-    u <- expectTYPE !ns !defs ctx ty
+    u <- expectTYPE !defs ctx ty
     expectEqualQ Zero sg.fst
     checkTypeNoWrap ctx t (Just u)
     pure $ zeroFor ctx
@@ -164,7 +164,7 @@ mutual
   check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Lam body) ty = do
-    (qty, arg, res) <- expectPi !ns !defs ctx ty
+    (qty, arg, res) <- expectPi !defs ctx ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
     let qty' = sg.fst * qty
@@ -175,7 +175,7 @@ mutual
   check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Pair fst snd) ty = do
-    (tfst, tsnd) <- expectSig !ns !defs ctx ty
+    (tfst, tsnd) <- expectSig !defs ctx ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
     qfst <- checkC ctx sg fst tfst
     let tsnd = sub1 tsnd (fst :# tfst)
@@ -187,7 +187,7 @@ mutual
   check' ctx sg t@(Enum _) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Tag t) ty = do
-    tags <- expectEnum !ns !defs ctx ty
+    tags <- expectEnum !defs ctx ty
     -- if t ∈ ts
     unless (t `elem` tags) $ throw $ TagNotIn t tags
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
@@ -196,7 +196,7 @@ mutual
   check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (DLam body) ty = do
-    (ty, l, r) <- expectEq !ns !defs ctx ty
+    (ty, l, r) <- expectEq !defs ctx ty
     let ctx' = extendDim body.name ctx
         ty   = ty.term
         body = body.term
@@ -212,17 +212,17 @@ mutual
   check' ctx sg Nat ty = toCheckType ctx sg Nat ty
 
   check' ctx sg Zero ty = do
-    expectNat !ns !defs ctx ty
+    expectNat !defs ctx ty
     pure $ zeroFor ctx
 
   check' ctx sg (Succ n) ty = do
-    expectNat !ns !defs ctx ty
+    expectNat !defs ctx ty
     checkC ctx sg n Nat
 
   check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Box val) ty = do
-    (q, ty) <- expectBOX !ns !defs ctx ty
+    (q, ty) <- expectBOX !defs ctx ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     valout <- checkC ctx sg val ty
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
@@ -301,7 +301,7 @@ mutual
     case u of
       Just u  => subtype ctx infres.type (TYPE u)
       Nothing => ignore $
-        expectTYPE !ns !defs ctx infres.type
+        expectTYPE !defs ctx infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
   private covering
@@ -338,7 +338,7 @@ mutual
 
   infer' ctx sg (F x) = do
     -- if π·x : A {≔ s} in global context
-    g <- lookupFree !ns x !defs
+    g <- lookupFree x !defs
     -- if σ ≤ π
     expectCompatQ sg.fst g.qty.fst
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
@@ -360,7 +360,7 @@ mutual
   infer' ctx sg (fun :@ arg) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- inferC ctx sg fun
-    (qty, argty, res) <- expectPi !ns !defs ctx funres.type
+    (qty, argty, res) <- expectPi !defs ctx funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
     argout <- checkC ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
@@ -377,7 +377,7 @@ mutual
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
     checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
-    (tfst, tsnd) <- expectSig !ns !defs ctx pairres.type
+    (tfst, tsnd) <- expectSig !defs ctx pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
@@ -395,7 +395,7 @@ mutual
   infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
-    ttags <- expectEnum !ns !defs ctx tres.type
+    ttags <- expectEnum !defs ctx tres.type
     -- if 1 ≤ π, OR there is only zero or one option
     unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ One pi
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
@@ -421,7 +421,7 @@ mutual
     expectCompatQ One pi
     -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
     nres <- inferC ctx sg n
-    expectNat !ns !defs ctx nres.type
+    expectNat !defs ctx nres.type
     -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
     checkTypeC (extendTy Zero ret.name Nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@@ -445,7 +445,7 @@ mutual
   infer' ctx sg (CaseBox pi box ret body) = do
     -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
     boxres <- inferC ctx sg box
-    (q, ty) <- expectBOX !ns !defs ctx boxres.type
+    (q, ty) <- expectBOX !defs ctx boxres.type
     -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
     checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
     -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
@@ -463,7 +463,7 @@ mutual
   infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
-    ty <- fst <$> expectEq !ns !defs ctx type
+    ty <- fst <$> expectEq !defs ctx type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
@@ -496,7 +496,7 @@ mutual
     -- if σ = 0
     expectEqualQ Zero sg.fst
     -- if Ψ, Γ ⊢₀ e ⇒ Type u
-    u <- expectTYPE !ns !defs ctx . type =<< inferC ctx szero ty
+    u <- expectTYPE !defs ctx . type =<< inferC ctx szero ty
     -- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
     checkTypeC ctx ret Nothing
     -- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 622909c..6e27e9b 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -39,8 +39,8 @@ InferResult eqs d n = IfConsistent eqs $ InferResult' d n
 
 
 export
-lookupFree : Has ErrorEff fs => Mods -> Name -> Definitions -> Eff fs Definition
-lookupFree ns x defs = maybe (throw $ NotInScope x) pure $ lookupNS ns x defs
+lookupFree : Has ErrorEff fs => Name -> Definitions -> Eff fs Definition
+lookupFree x defs = maybe (throw $ NotInScope x) pure $ lookup x defs
 
 
 public export
@@ -59,14 +59,14 @@ substCaseBoxRet dty retty =
   retty.term // (Box (BVT 0) :# weakT 1 dty ::: shift 1)
 
 
-parameters (ns : Mods) (defs : Definitions) {auto _ : Has ErrorEff fs}
+parameters (defs : Definitions) {auto _ : Has ErrorEff fs}
   namespace TyContext
    parameters (ctx : TyContext d n)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-           tm d n -> Eff fs (NonRedex tm d n ns defs)
+           tm d n -> Eff fs (NonRedex tm d n defs)
     whnf = let Val n = ctx.termLen; Val d = ctx.dimLen in
-           rethrow . whnf ns defs (toWhnfContext ctx)
+           rethrow . whnf defs (toWhnfContext ctx)
 
     private covering %macro
     expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
@@ -108,8 +108,8 @@ parameters (ns : Mods) (defs : Definitions) {auto _ : Has ErrorEff fs}
    parameters (ctx : EqContext n)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-           tm 0 n -> Eff fs (NonRedex tm 0 n ns defs)
-    whnf = let Val n = ctx.termLen in rethrow . whnf ns defs (toWhnfContext ctx)
+           tm 0 n -> Eff fs (NonRedex tm 0 n defs)
+    whnf = let Val n = ctx.termLen in rethrow . whnf defs (toWhnfContext ctx)
 
     private covering %macro
     expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 52ff442..edb2eae 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -21,10 +21,10 @@ defGlobals = fromList
 parameters (label : String) (act : Lazy (TC ()))
            {default defGlobals globals : Definitions}
   testEq : Test
-  testEq = test label $ runTC [<] globals act
+  testEq = test label $ runTC globals act
 
   testNeq : Test
-  testNeq = testThrows label (const True) $ runTC [<] globals act $> "()"
+  testNeq = testThrows label (const True) $ runTC globals act $> "()"
 
 
 parameters (0 d : Nat) (ctx : TyContext d n)
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index 05b65fe..0507a8e 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -61,8 +61,9 @@ parameters {c : Bool} {auto _ : Show b}
 
 FromString BName where fromString = Just . fromString
 
-runFromParser : Eff [Except FromParser.Error] a -> Either FromParser.Error a
-runFromParser = extract . runExcept
+runFromParser : {default empty defs : Definitions} ->
+                Eff FromParserPure a -> Either FromParser.Error a
+runFromParser = map fst . fromParserPure defs
 
 export
 tests : Test
@@ -79,7 +80,9 @@ tests = "PTerm → Term" :- [
   ],
 
   "terms" :-
-  let fromPTerm = runFromParser .
+  let defs = fromList [("f", mkDef gany Nat Zero)]
+        -- doesn't have to be well typed yet, just well scoped
+      fromPTerm = runFromParser {defs} .
                   fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]
   in [
     note "dim ctx: [𝑖, 𝑗]; term ctx: [A, x, y, z]",
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 1597dd6..09a15fd 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -13,7 +13,7 @@ parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex} {d, n : Nat}
   private
   testWhnf : String -> WhnfContext d n -> tm d n -> tm d n -> Test
   testWhnf label ctx from to = test "\{label}  (whnf)" $ do
-    result <- bimap toInfo fst $ whnf [<] defs ctx from
+    result <- bimap toInfo fst $ whnf defs ctx from
     unless (result == to) $ Left [("exp", show to), ("got", show result)]
 
   private
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index ab5aca7..9894b1f 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -28,7 +28,7 @@ ToInfo Error' where
 M = Eff [Except Error', DefsReader]
 
 inj : TC a -> M a
-inj = rethrow . mapFst TCError <=< lift . runExcept . runReaderAt NS [<]
+inj = rethrow . mapFst TCError <=< lift . runExcept
 
 
 reflTy : Term d n