From 0e481a80981b61c8f636364a59cb6534050ca65a Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 22 Feb 2023 07:40:19 +0100
Subject: [PATCH] new representation for scopes

---
 lib/Quox/Equal.idr              |  39 +++++----
 lib/Quox/Name.idr               |   4 +
 lib/Quox/Pretty.idr             |  16 ++--
 lib/Quox/Reduce.idr             |  30 +++----
 lib/Quox/Syntax/Term/Base.idr   |  66 +++++++--------
 lib/Quox/Syntax/Term/Pretty.idr | 131 +++++++++++++++--------------
 lib/Quox/Syntax/Term/Split.idr  |  36 ++++----
 lib/Quox/Syntax/Term/Subst.idr  | 143 ++++++++++++++++++--------------
 lib/Quox/Typechecker.idr        |  60 ++++++--------
 lib/Quox/Typing.idr             |   6 +-
 tests/TermImpls.idr             |  28 +++----
 tests/Tests/Equal.idr           |  18 ++--
 tests/Tests/Reduce.idr          | 115 ++++++++++++-------------
 tests/Tests/Typechecker.idr     |  48 +++++------
 14 files changed, 376 insertions(+), 364 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 8a4d109..5515e3d 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -83,15 +83,15 @@ parameters (defs : Definitions' q g)
   isSubSing ty =
     let Element ty nc = whnf defs ty in
     case ty of
-      TYPE _             => False
-      Pi   {res, _}      => isSubSing res.term
-      Lam  {}            => False
-      Sig  {fst, snd, _} => isSubSing fst && isSubSing snd.term
-      Pair {}            => False
-      Eq   {}            => True
-      DLam {}            => False
-      E    (s :# _)      => isSubSing s
-      E    _             => False
+      TYPE _          => False
+      Pi   {res, _}   => isSubSing res.term
+      Lam  {}         => False
+      Sig  {fst, snd} => isSubSing fst && isSubSing snd.term
+      Pair {}         => False
+      Eq   {}         => True
+      DLam {}         => False
+      E    (s :# _)   => isSubSing s
+      E    _          => False
 
 
 parameters {auto _ : HasErr q m}
@@ -141,13 +141,13 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           --          Γ, x : A ⊢ s = t : B
           -- -----------------------------------------
           --  Γ ⊢ (λx ⇒ s) = (λx ⇒ t) : (π·x : A) → B
-          (Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
+          (Lam b1, Lam b2) => compare0 ctx' res.term b1.term b2.term
 
           --       Γ, x : A ⊢ s = e x : B
           -- ----------------------------------
           --  Γ ⊢ (λx ⇒ s) = e : (π·x : A) → B
-          (E e,     Lam _ b)  => eta e b
-          (Lam _ b, E e)      => eta e b
+          (E e,   Lam b) => eta e b
+          (Lam b, E e)   => eta e b
 
           (E e, E f) => Elim.compare0 ctx e f
           _ => throwError $ WrongType ty s t
@@ -156,8 +156,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           ctx' = ctx :< arg
 
           eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
-          eta e (TUsed   b) = compare0 ctx' res.term (toLamBody e) b
-          eta e (TUnused _) = clashT ty s t
+          eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
+          eta e (S _ (N _)) = clashT ty s t
 
       compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
         case (s, t) of
@@ -322,8 +322,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           Term.compare0 ctx arg s t
       compare0' _ e@(_ :@ _) f _ _ = clashE e f
 
-      compare0' ctx (CasePair epi e _ eret _ _ ebody)
-                    (CasePair fpi f _ fret _ _ fbody) ne nf =
+      compare0' ctx (CasePair epi e eret ebody)
+                    (CasePair fpi f fret fbody) ne nf =
         local {mode := Equal} $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
@@ -334,7 +334,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           unless (epi == fpi) $ throwError $ ClashQ epi fpi
       compare0' _ e@(CasePair {}) f _ _ = clashE e f
 
-      compare0' ctx   (s :# a) (t :# _) _ _ = Term.compare0 ctx a s t
+      compare0' ctx (s :# a) (t :# b) _ _ =
+          Term.compare0 ctx !(bigger a b) s t
+        where
+          bigger : forall a. a -> a -> m a
+          bigger l r = asks mode <&> \case Super => l; _ => r
+
       compare0' ctx   (s :# a) f        _ _ = Term.compare0 ctx a s (E f)
       compare0' ctx e          (t :# b) _ _ = Term.compare0 ctx b (E e) t
       compare0' _   e@(_ :# _) f        _ _ = clashE e f
diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr
index a1b8c91..5524fa3 100644
--- a/lib/Quox/Name.idr
+++ b/lib/Quox/Name.idr
@@ -45,6 +45,10 @@ export
 FromString Name where
   fromString x = MakeName [<] (fromString x)
 
+public export %inline
+unq : BaseName -> Name
+unq = MakeName [<]
+
 
 export
 toDots : Name -> String
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 07f8ca8..3a1dc8e 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -40,8 +40,8 @@ data HL
 public export
 data PPrec
 = Outer
-| Ann  -- right of "::"
-| AnnL -- left  of "::"
+| Ann  -- right of "∷"
+| AnnL -- left  of "∷"
 | Eq   -- "_ ≡ _ : _"
 | InEq -- arguments of ≡
   -- ...
@@ -153,12 +153,12 @@ withPrec d = local {prec := d}
 public export data BinderSort = T | D
 
 export %inline
-unders : HasEnv m => BinderSort -> List Name -> m a -> m a
-unders T xs = local {prec := Outer, tnames $= (xs ++)}
-unders D xs = local {prec := Outer, dnames $= (xs ++)}
+unders : HasEnv m => BinderSort -> List BaseName -> m a -> m a
+unders T xs = local {prec := Outer, tnames $= (map unq xs ++)}
+unders D xs = local {prec := Outer, dnames $= (map unq xs ++)}
 
 export %inline
-under : HasEnv m => BinderSort -> Name -> m a -> m a
+under : HasEnv m => BinderSort -> BaseName -> m a -> m a
 under t x = unders t [x]
 
 
@@ -237,9 +237,9 @@ a </> b = cat [a, b]
 
 
 ||| wrapper for names that pretty-prints highlighted as a `TVar`.
-public export data TVarName = TV Name
+public export data TVarName = TV BaseName
 export %inline PrettyHL TVarName where prettyM (TV x) = hlF TVar $ prettyM x
 
 ||| wrapper for names that pretty-prints highlighted as a `DVar`.
-public export data DVarName = DV Name
+public export data DVarName = DV BaseName
 export %inline PrettyHL DVarName where prettyM (DV x) = hlF DVar $ prettyM x
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 9e53bf5..3ad7a68 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -63,18 +63,18 @@ mutual
   PushSubsts Term Reduce.isCloT where
     pushSubstsWith th ph (TYPE l) =
       nclo $ TYPE l
-    pushSubstsWith th ph (Pi qty x a body) =
-      nclo $ Pi qty x (a // th // ph) (body // th // ph)
-    pushSubstsWith th ph (Lam x body) =
-      nclo $ Lam x $ body // th // ph
-    pushSubstsWith th ph (Sig x a b) =
-      nclo $ Sig x (a // th // ph) (b // th // ph)
+    pushSubstsWith th ph (Pi qty a body) =
+      nclo $ Pi qty (a // th // ph) (body // th // ph)
+    pushSubstsWith th ph (Lam body) =
+      nclo $ Lam (body // th // ph)
+    pushSubstsWith th ph (Sig a b) =
+      nclo $ Sig (a // th // ph) (b // th // ph)
     pushSubstsWith th ph (Pair s t) =
       nclo $ Pair (s // th // ph) (t // th // ph)
-    pushSubstsWith th ph (Eq i ty l r) =
-      nclo $ Eq i (ty // th // ph) (l // th // ph) (r // th // ph)
-    pushSubstsWith th ph (DLam i body) =
-      nclo $ DLam i $ body // th // ph
+    pushSubstsWith th ph (Eq ty l r) =
+      nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph)
+    pushSubstsWith th ph (DLam body) =
+      nclo $ DLam (body // th // ph)
     pushSubstsWith th ph (E e) =
       let Element e nc = pushSubstsWith th ph e in nclo $ E e
     pushSubstsWith th ph (CloT s ps) =
@@ -93,8 +93,8 @@ mutual
         Right no  => Element res no
     pushSubstsWith th ph (f :@ s) =
       nclo $ (f // th // ph) :@ (s // th // ph)
-    pushSubstsWith th ph (CasePair pi p x r y z b) =
-      nclo $ CasePair pi (p // th // ph) x (r // th // ph) y z (b // th // ph)
+    pushSubstsWith th ph (CasePair pi p r b) =
+      nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph)
     pushSubstsWith th ph (f :% d) =
       nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =
@@ -197,13 +197,13 @@ mutual
       let Element f fnf = whnf defs f in
       case nchoose $ isLamHead f of
         Left _ =>
-          let Lam {body, _} :# Pi {arg, res, _} = f
+          let Lam body :# Pi {arg, res, _} = f
               s = s :# arg
           in
           whnf defs $ sub1 body s :# sub1 res s
         Right nlh => Element (f :@ s) $ fnf `orNo` nlh
 
-    whnf defs (CasePair pi pair r ret x y body) =
+    whnf defs (CasePair pi pair ret body) =
       let Element pair pairnf = whnf defs pair in
       case nchoose $ isPairHead pair of
         Left _ =>
@@ -219,7 +219,7 @@ mutual
       let Element f fnf = whnf defs f in
       case nchoose $ isDLamHead f of
         Left _ =>
-          let DLam {body, _} :# Eq {ty, l, r, _} = f
+          let DLam body :# Eq {ty = ty, l, r, _} = f
               body = endsOr l r (dsub1 body p) p
           in
           whnf defs $ body :# dsub1 ty p
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 1550c3a..42ce032 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -47,22 +47,20 @@ mutual
     TYPE : (l : Universe) -> Term q d n
 
     ||| function type
-    Pi  : (qty : q) -> (x : Name) ->
-          (arg : Term q d n) -> (res : ScopeTerm q d n) -> Term q d n
+    Pi  : (qty : q) -> (arg : Term q d n) ->
+          (res : ScopeTerm q d n) -> Term q d n
     ||| function term
-    Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
+    Lam : (body : ScopeTerm q d n) -> Term q d n
 
     ||| pair type
-    Sig : (x : Name) -> (fst : Term q d n) -> (snd : ScopeTerm q d n) ->
-          Term q d n
+    Sig : (fst : Term q d n) -> (snd : ScopeTerm q d n) -> Term q d n
     ||| pair value
     Pair : (fst, snd : Term q d n) -> Term q d n
 
     ||| equality type
-    Eq : (i : Name) -> (ty : DScopeTerm q d n) -> (l, r : Term q d n) ->
-         Term q d n
+    Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> Term q d n
     ||| equality term
-    DLam : (i : Name) -> (body : DScopeTerm q d n) -> Term q d n
+    DLam : (body : DScopeTerm q d n) -> Term q d n
 
     ||| elimination
     E : (e : Elim q d n) -> Term q d n
@@ -87,11 +85,11 @@ mutual
 
     ||| pair destruction
     |||
-    ||| `CasePair 𝜋 𝑒 𝑟 𝐴 𝑥 𝑦 𝑡` is
+    ||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
     ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
     CasePair : (qty : q) -> (pair : Elim q d n) ->
-               (r : Name) -> (ret : ScopeTerm q d n) ->
-               (x, y : Name) -> (body : ScopeTermN 2 q d n) ->
+               (ret : ScopeTerm q d n) ->
+               (body : ScopeTermN 2 q d n) ->
                Elim q d n
 
     ||| dim application
@@ -107,49 +105,51 @@ mutual
     DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
             Elim q dto n
 
-  ||| a scope with some more bound term variables
   public export
-  data ScopeTermN : Nat -> TermLike where
-    ||| at least some variables are used
-    TUsed : (body : Term q d (s + n)) -> ScopeTermN s q d n
-    ||| all variables are unused
-    TUnused : (body : Term q d n) -> ScopeTermN s q d n
+  0 CaseEnumArms : TermLike
+  CaseEnumArms q d n = SortedMap TagVal (Term q d n)
+
+  ||| a scoped term with names
+  public export
+  record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
+    constructor S
+    names : Vect s BaseName
+    body  : ScopedBody s f n
 
   public export
-  0 ScopeTerm : TermLike
-  ScopeTerm = ScopeTermN 1
-
-  ||| a scope with some more bound dimension variable
-  public export
-  data DScopeTermN : Nat -> TermLike where
-    ||| at least some variables are used
-    DUsed : (body : Term q (s + d) n) -> DScopeTermN s q d n
-    ||| all variables are unused
-    DUnused : (body : Term q d n) -> DScopeTermN s q d n
+  data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
+    Y : (body : f (s + n)) -> ScopedBody s f n
+    N : (body : f n)       -> ScopedBody s f n
 
   public export
-  0 DScopeTerm : TermLike
+  0 ScopeTermN, DScopeTermN : Nat -> TermLike
+  ScopeTermN  s q d n = Scoped s (Term q d) n
+  DScopeTermN s q d n = Scoped s (\d => Term q d n) d
+
+  public export
+  0 ScopeTerm, DScopeTerm : TermLike
+  ScopeTerm  = ScopeTermN 1
   DScopeTerm = DScopeTermN 1
 
 %name Term s, t, r
 %name Elim e, f
-%name ScopeTermN body
-%name DScopeTermN body
+%name Scoped body
+%name ScopedBody body
 
 ||| non dependent function type
 public export %inline
 Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
-Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
+Arr {qty, arg, res} = Pi {qty, arg, res = S ["_"] $ N res}
 
 ||| non dependent equality type
 public export %inline
 Eq0 : (ty, l, r : Term q d n) -> Term q d n
-Eq0 {ty, l, r} = Eq {i = "_", ty = DUnused ty, l, r}
+Eq0 {ty, l, r} = Eq {ty = S ["_"] $ N ty, l, r}
 
 ||| non dependent pair type
 public export %inline
 And : (fst, snd : Term q d n) -> Term q d n
-And {fst, snd} = Sig {x = "_", fst, snd = TUnused snd}
+And {fst, snd} = Sig {fst, snd = S ["_"] $ N snd}
 
 ||| same as `F` but as a term
 public export %inline
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 76a4d36..d6581ee 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -32,25 +32,80 @@ ofD     = hl Syntax "of"
 returnD = hl Syntax "return"
 
 
+export covering
+prettyBindType : Pretty.HasEnv m =>
+                 PrettyHL q => PrettyHL a => PrettyHL b =>
+                 List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
+prettyBindType qtys x s arr t =
+    parensIfM Outer $ hang 2 $
+      parens !(prettyQtyBinds qtys $ TV x) <++> arr
+        <//> !(under T x $ prettyM t)
+
+export covering
+prettyLams : Pretty.HasEnv m => PrettyHL a =>
+             BinderSort -> List BaseName -> a -> m (Doc HL)
+prettyLams sort names body = do
+  lam    <- case sort of T => lamD; D => dlamD
+  header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [darrowD]
+  body   <- unders sort names $ prettyM body
+  parensIfM Outer $ sep (lam :: header) <//> body
+
+export covering
+prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
+             f -> List a -> m (Doc HL)
+prettyApps fun args =
+  parensIfM App =<< withPrec Arg
+    [|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
+
+export covering
+prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL)
+prettyTuple = map (parens . align . separate commaD) . traverse prettyM
+
+export covering
+prettyArm : Pretty.HasEnv m => PrettyHL a =>
+            (List BaseName, Doc HL, a) -> m (Doc HL)
+prettyArm (xs, pat, body) =
+  pure $ hang 2 $ sep
+    [hsep [pat, !darrowD],
+     !(withPrec Outer $ unders T xs $ prettyM body)]
+
+export covering
+prettyArms : Pretty.HasEnv m => PrettyHL a =>
+             List (List BaseName, Doc HL, a) -> m (Doc HL)
+prettyArms = map (braces . align . sep) . traverse prettyArm
+
+export covering
+prettyCase : Pretty.HasEnv m =>
+             PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c =>
+             q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) ->
+             m (Doc HL)
+prettyCase pi elim r ret arms =
+  pure $ align $ sep $
+    [hsep [caseD,   !(prettyQtyBinds [pi] elim)],
+     hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
+     hsep [ofD,     !(prettyArms arms)]]
+
+
 mutual
   export covering
   PrettyHL q => PrettyHL (Term q d n) where
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
-    prettyM (Pi qty x s t) =
+    prettyM (Pi qty s (S [x] t)) =
       prettyBindType [qty] x s !arrowD t
-    prettyM (Lam x t) =
-      let GotLams {names, body, _} = getLams' [x] t.term Refl in
+    prettyM (Lam (S x t)) =
+      let GotLams {names, body, _} = getLams' x t.term Refl in
       prettyLams T (toList names) body
-    prettyM (Sig x s t) =
-      prettyBindType [] x s !timesD t
+    prettyM (Sig s (S [x] t)) =
+      prettyBindType {q} [] x s !timesD t
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs t in
       prettyTuple $ s :: init ++ [last]
-    prettyM (Eq _ (DUnused ty) l r) =
+    prettyM (Eq (S _ (N ty)) l r) =
       parensIfM Eq !(withPrec InEq $ pure $
-        sep [!(prettyM l) <++> !eqndD, !(prettyM r) <++> colonD, !(prettyM ty)])
-    prettyM (Eq i (DUsed ty) l r) =
+        sep [!(prettyM l) <++> !eqndD,
+             !(prettyM r) <++> colonD, !(prettyM ty)])
+    prettyM (Eq (S [i] (Y ty)) l r) =
       parensIfM App $
         eqD <++>
         sep [bracks !(withPrec Outer $ pure $ hang 2 $
@@ -58,8 +113,8 @@ mutual
                     !(under D i $ prettyM ty)]),
              !(withPrec Arg $ prettyM l),
              !(withPrec Arg $ prettyM r)]
-    prettyM (DLam i t) =
-      let GotDLams {names, body, _} = getDLams' [i] t.term Refl in
+    prettyM (DLam (S i t)) =
+      let GotDLams {names, body, _} = getDLams' i t.term Refl in
       prettyLams D (toList names) body
     prettyM (E e) = bracks <$> prettyM e
     prettyM (CloT s th) =
@@ -78,7 +133,7 @@ mutual
     prettyM (e :@ s) =
       let GotArgs {fun, args, _} = getArgs' e [s] in
       prettyApps fun args
-    prettyM (CasePair pi p r ret x y body) = do
+    prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
       pat <- (parens . separate commaD . map (hl TVar)) <$>
              traverse prettyM [x, y]
       prettyCase pi p r ret [([x, y], pat, body)]
@@ -97,62 +152,10 @@ mutual
         [|withPrec SApp (prettyM e) </> prettyDSubst th|]
 
   export covering
-  {s : Nat} -> PrettyHL q => PrettyHL (ScopeTermN s q d n) where
+  {s : Nat} -> PrettyHL q => PrettyHL (ScopedBody s (Term q d) n) where
     prettyM body = prettyM body.term
 
   export covering
   prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
                  TSubst q d from to -> m (Doc HL)
   prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
-
-  export covering
-  prettyBindType : Pretty.HasEnv m => PrettyHL q =>
-                   List q -> Name -> Term q d n -> Doc HL ->
-                   ScopeTerm q d n -> m (Doc HL)
-  prettyBindType qtys x s arr t =
-      parensIfM Outer $ hang 2 $
-        parens !(prettyQtyBinds qtys $ TV x) <++> arr
-          <//> !(under T x $ prettyM t)
-
-  export covering
-  prettyLams : Pretty.HasEnv m => PrettyHL q =>
-               BinderSort -> List Name -> Term q _ _ -> m (Doc HL)
-  prettyLams sort names body = do
-    lam    <- case sort of T => lamD; D => dlamD
-    header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [darrowD]
-    body   <- unders sort names $ prettyM body
-    parensIfM Outer $ sep (lam :: header) <//> body
-
-  export covering
-  prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
-               f -> List a -> m (Doc HL)
-  prettyApps fun args =
-    parensIfM App =<< withPrec Arg
-      [|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
-
-  export covering
-  prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL)
-  prettyTuple = map (parens . align . separate commaD) . traverse prettyM
-
-  export covering
-  prettyArm : Pretty.HasEnv m => PrettyHL a =>
-              (List Name, Doc HL, a) -> m (Doc HL)
-  prettyArm (xs, pat, body) =
-    pure $ hang 2 $ sep
-      [hsep [pat, !darrowD],
-       !(withPrec Outer $ unders T xs $ prettyM body)]
-
-  export covering
-  prettyArms : Pretty.HasEnv m => PrettyHL a =>
-               List (List Name, Doc HL, a) -> m (Doc HL)
-  prettyArms = map (braces . align . sep) . traverse prettyArm
-
-  export covering
-  prettyCase : Pretty.HasEnv m =>
-               PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c =>
-               q -> a -> Name -> b -> List (List Name, Doc HL, c) -> m (Doc HL)
-  prettyCase pi elim r ret arms =
-    pure $ align $ sep $
-      [hsep [caseD,   !(prettyQtyBinds [pi] elim)],
-       hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
-       hsep [ofD,     !(prettyArms arms)]]
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
index 85f9941..8c943da 100644
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@@ -11,8 +11,8 @@ import public Data.Vect
 
 public export %inline
 isLam : Term {} -> Bool
-isLam (Lam {}) = True
-isLam _        = False
+isLam (Lam _) = True
+isLam _       = False
 
 public export
 0 NotLam : Pred $ Term {}
@@ -21,8 +21,8 @@ NotLam = No . isLam
 
 public export %inline
 isDLam : Term {} -> Bool
-isDLam (DLam {}) = True
-isDLam _         = False
+isDLam (DLam _) = True
+isDLam _        = False
 
 public export
 0 NotDLam : Pred $ Term {}
@@ -113,25 +113,25 @@ getDArgs e = getDArgs' e []
 
 infixr 1 :\\
 public export
-absN : Vect m Name -> Term q d (m + n) -> Term q d n
+absN : Vect m BaseName -> Term q d (m + n) -> Term q d n
 absN {m = 0}   []        s = s
-absN {m = S m} (x :: xs) s = Lam x $ TUsed $ absN xs $
-                             rewrite sym $ plusSuccRightSucc m n in s
+absN {m = S m} (x :: xs) s =
+  Lam $ S [x] $ Y $ absN xs $ rewrite sym $ plusSuccRightSucc m n in s
 
 public export %inline
-(:\\) : Vect m Name -> Term q d (m + n) -> Term q d n
+(:\\) : Vect m BaseName -> Term q d (m + n) -> Term q d n
 (:\\) = absN
 
 
 infixr 1 :\\%
 public export
-dabsN : Vect m Name -> Term q (m + d) n -> Term q d n
+dabsN : Vect m BaseName -> Term q (m + d) n -> Term q d n
 dabsN {m = 0}   []        s = s
-dabsN {m = S m} (x :: xs) s = DLam x $ DUsed $ dabsN xs $
-                              rewrite sym $ plusSuccRightSucc m d in s
+dabsN {m = S m} (x :: xs) s =
+  DLam $ S [x] $ Y $ dabsN xs $ rewrite sym $ plusSuccRightSucc m d in s
 
 public export %inline
-(:\\%) : Vect m Name -> Term q (m + d) n -> Term q d n
+(:\\%) : Vect m BaseName -> Term q (m + d) n -> Term q d n
 (:\\%) = dabsN
 
 
@@ -139,17 +139,17 @@ public export
 record GetLams q d n where
   constructor GotLams
   {0 lams, rest : Nat}
-  names    : Vect lams Name
+  names    : Vect lams BaseName
   body     : Term q d rest
   0 eq     : lams + n = rest
   0 notLam : NotLam body
 
 export
 getLams' : forall lams, rest.
-           Vect lams Name -> Term q d rest -> (0 eq : lams + n = rest) ->
+           Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) ->
            GetLams q d n
 getLams' xs s Refl = case nchoose $ isLam s of
-  Left  y => let Lam x body = s in
+  Left  y => let Lam (S [x] body) = s in
              getLams' (x :: xs) (assert_smaller s body.term) Refl
   Right n => GotLams xs s Refl n
 
@@ -162,17 +162,17 @@ public export
 record GetDLams q d n where
   constructor GotDLams
   {0 lams, rest : Nat}
-  names     : Vect lams Name
+  names     : Vect lams BaseName
   body      : Term q rest n
   0 eq      : lams + d = rest
   0 notDLam : NotDLam body
 
 export
 getDLams' : forall lams, rest.
-            Vect lams Name -> Term q rest n -> (0 eq : lams + d = rest) ->
+            Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) ->
             GetDLams q d n
 getDLams' is s Refl = case nchoose $ isDLam s of
-  Left  y => let DLam i body = s in
+  Left  y => let DLam (S [i] body) = s in
              getDLams' (i :: is) (assert_smaller s body.term) Refl
   Right n => GotDLams is s Refl n
 
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 56cf5c8..786daec 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -10,49 +10,53 @@ namespace CanDSubst
   interface CanDSubst (0 tm : Nat -> Nat -> Type) where
     (//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
 
-mutual
-  ||| does the minimal reasonable work:
-  ||| - deletes the closure around an atomic constant like `TYPE`
-  ||| - deletes an identity substitution
-  ||| - composes (lazily) with an existing top-level dim-closure
-  ||| - otherwise, wraps in a new closure
-  export
-  CanDSubst (Term q) where
-    s          // Shift SZ = s
-    TYPE l     // _        = TYPE l
-    DCloT s ph // th       = DCloT s $ ph . th
-    s          // th       = DCloT s th
+||| does the minimal reasonable work:
+||| - deletes the closure around an atomic constant like `TYPE`
+||| - deletes an identity substitution
+||| - composes (lazily) with an existing top-level dim-closure
+||| - otherwise, wraps in a new closure
+export
+CanDSubst (Term q) where
+  s          // Shift SZ = s
+  TYPE l     // _        = TYPE l
+  DCloT s ph // th       = DCloT s $ ph . th
+  s          // th       = DCloT s th
 
-  private
-  subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
-  subDArgs (f :% d) th = subDArgs f th :% (d // th)
-  subDArgs e        th = DCloE e th
+private
+subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
+subDArgs (f :% d) th = subDArgs f th :% (d // th)
+subDArgs e        th = DCloE e th
 
-  ||| does the minimal reasonable work:
-  ||| - deletes the closure around a term variable
-  ||| - deletes an identity substitution
-  ||| - composes (lazily) with an existing top-level dim-closure
-  ||| - immediately looks up bound variables in a
-  |||   top-level sequence of dimension applications
-  ||| - otherwise, wraps in a new closure
-  export
-  CanDSubst (Elim q) where
-    e          // Shift SZ = e
-    F x        // _        = F x
-    B i        // _        = B i
-    f :% d     // th       = subDArgs (f :% d) th
-    DCloE e ph // th       = DCloE e $ ph . th
-    e          // th       = DCloE e th
+||| does the minimal reasonable work:
+||| - deletes the closure around a term variable
+||| - deletes an identity substitution
+||| - composes (lazily) with an existing top-level dim-closure
+||| - immediately looks up bound variables in a
+|||   top-level sequence of dimension applications
+||| - otherwise, wraps in a new closure
+export
+CanDSubst (Elim q) where
+  e          // Shift SZ = e
+  F x        // _        = F x
+  B i        // _        = B i
+  f :% d     // th       = subDArgs (f :% d) th
+  DCloE e ph // th       = DCloE e $ ph . th
+  e          // th       = DCloE e th
 
-  export
-  CanDSubst (ScopeTermN s q) where
-    TUsed   body // th = TUsed   $ body // th
-    TUnused body // th = TUnused $ body // th
+namespace DSubst.ScopeTermN
+  export %inline
+  (//) : ScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
+         ScopeTermN s q dto n
+  S ns (Y body) // th = S ns $ Y $ body // th
+  S ns (N body) // th = S ns $ N $ body // th
 
-  export
-  {s : Nat} -> CanDSubst (DScopeTermN s q) where
-    DUsed   body // th = DUsed   $ body // pushN s th
-    DUnused body // th = DUnused $ body // th
+namespace DSubst.DScopeTermN
+  export %inline
+  (//) : {s : Nat} ->
+         DScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
+         DScopeTermN s q dto n
+  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (N body) // th = S ns $ N $ body // th
 
 
 export %inline FromVar (Elim q d) where fromVar = B
@@ -94,15 +98,21 @@ CanTSubst Term where
                          Shift SZ => s
                          th       => CloT s th
 
-export %inline
-{s : Nat} -> CanTSubst (ScopeTermN s) where
-  TUsed   body // th = TUsed   $ body // pushN s th
-  TUnused body // th = TUnused $ body // th
+namespace ScopeTermN
+  export %inline
+  (//) : {s : Nat} ->
+         ScopeTermN s q d from -> Lazy (TSubst q d from to) ->
+         ScopeTermN s q d to
+  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (N body) // th = S ns $ N $ body // th
 
-export %inline
-{s : Nat} -> CanTSubst (DScopeTermN s) where
-  DUsed   body // th = DUsed   $ body // map (// shift s) th
-  DUnused body // th = DUnused $ body // th
+namespace DScopeTermN
+  export %inline
+  (//) : {s : Nat} ->
+         DScopeTermN s q d from -> Lazy (TSubst q d from to) ->
+         DScopeTermN s q d to
+  S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
+  S ns (N body) // th = S ns $ N $ body // th
 
 export %inline CanShift (Term q d) where s // by = s // Shift by
 export %inline CanShift (Elim q d) where e // by = e // Shift by
@@ -136,23 +146,34 @@ weakE : {default 1 by : Nat} -> Elim q d n -> Elim q d (by + n)
 weakE t = t // shift by
 
 
-namespace ScopeTermN
-  export %inline
-  (.term) : {s : Nat} -> ScopeTermN s q d n -> Term q d (s + n)
-  (TUsed   body).term = body
-  (TUnused body).term = weakT body {by = s}
+parameters {s : Nat}
+  namespace ScopeTermBody
+    export %inline
+    (.term) : ScopedBody s (Term q d) n -> Term q d (s + n)
+    (Y b).term = b
+    (N b).term = weakT b {by = s}
 
-namespace DScopeTermN
-  export %inline
-  (.term) : {s : Nat} -> DScopeTermN s q d n -> Term q (s + d) n
-  (DUsed   body).term = body
-  (DUnused body).term = dweakT body {by = s}
+  namespace ScopeTermN
+    export %inline
+    (.term) : ScopeTermN s q d n -> Term q d (s + n)
+    t.term = t.body.term
+
+  namespace DScopeTermBody
+    export %inline
+    (.term) : ScopedBody s (\d => Term q d n) d -> Term q (s + d) n
+    (Y b).term = b
+    (N b).term = dweakT b {by = s}
+
+  namespace DScopeTermN
+    export %inline
+    (.term) : DScopeTermN s q d n -> Term q (s + d) n
+    t.term = t.body.term
 
 
 export %inline
 subN : ScopeTermN s q d n -> Vect s (Elim q d n) -> Term q d n
-subN (TUsed   body) es = body // fromVect es
-subN (TUnused body) _  = body
+subN (S _ (Y body)) es = body // fromVect es
+subN (S _ (N body)) _  = body
 
 export %inline
 sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
@@ -160,8 +181,8 @@ sub1 t e = subN t [e]
 
 export %inline
 dsubN : DScopeTermN s q d n -> Vect s (Dim d) -> Term q d n
-dsubN (DUsed   body) ps = body // fromVect ps
-dsubN (DUnused body) _  = body
+dsubN (S _ (Y body)) ps = body // fromVect ps
+dsubN (S _ (N body)) _  = body
 
 export %inline
 dsub1 : DScopeTerm q d n -> Dim d -> Term q d n
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index d574728..a416ce9 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -28,29 +28,9 @@ popQ pi = popQs [< pi]
 
 
 
-private %inline
-weakI : IsQty q => InferResult' q d n -> InferResult' q d (S n)
-weakI = {type $= weakT, qout $= (:< zero)}
-
-private
-lookupBound : IsQty q => q -> Var n -> TContext q d n -> InferResult' q d n
-lookupBound pi VZ (ctx :< ty) =
-  InfRes {type = weakT ty, qout = (zero <$ ctx) :< pi}
-lookupBound pi (VS i) (ctx :< _) =
-  weakI $ lookupBound pi i ctx
-
-private %inline
-lookupFree : CanTC' q g m => Name -> m (Definition' q g)
-lookupFree x = lookupFree' !ask x
-
 
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
-  -- [todo] it seems like the options here for dealing with substitutions are
-  -- to either push them or parametrise the whole typechecker over ambient
-  -- substitutions. both of them seem like the same amount of work for the
-  -- computer but pushing is less work for the me
-
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
   |||
   ||| `check ctx sg subj ty` checks that in the context `ctx`, the term
@@ -116,19 +96,19 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     unless (k < l) $ throwError $ BadUniverse k l
     pure $ zeroFor ctx
 
-  check' ctx sg (Pi qty _ arg res) ty = do
+  check' ctx sg (Pi qty arg res) ty = do
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     check0 ctx arg (TYPE l)
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
-    case res of
-      TUsed   res => check0 (extendTy arg ctx) res (TYPE l)
-      TUnused res => check0 ctx res (TYPE l)
+    case res.body of
+      Y res => check0 (extendTy arg ctx) res (TYPE l)
+      N res => check0 ctx res (TYPE l)
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
     pure $ zeroFor ctx
 
-  check' ctx sg (Lam _ body) ty = do
+  check' ctx sg (Lam body) ty = do
     (qty, arg, res) <- expectPi !ask ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
@@ -137,15 +117,15 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ qty' qout
 
-  check' ctx sg (Sig _ fst snd) ty = do
+  check' ctx sg (Sig fst snd) ty = do
     l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     check0 ctx fst (TYPE l)
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
-    case snd of
-      TUsed   snd => check0 (extendTy fst ctx) snd (TYPE l)
-      TUnused snd => check0 ctx snd (TYPE l)
+    case snd.body of
+      Y snd => check0 (extendTy fst ctx) snd (TYPE l)
+      N snd => check0 ctx snd (TYPE l)
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
     pure $ zeroFor ctx
 
@@ -159,13 +139,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
     pure $ qfst + qsnd
 
-  check' ctx sg (Eq _ t l r) ty = do
+  check' ctx sg (Eq t l r) ty = do
     u <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
-    case t of
-      DUsed   t => check0 (extendDim ctx) t (TYPE u)
-      DUnused t => check0 ctx t (TYPE u)
+    case t.body of
+      Y t => check0 (extendDim ctx) t (TYPE u)
+      N t => check0 ctx t (TYPE u)
     -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
     check0 ctx t.zero l
     -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
@@ -173,7 +153,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
     pure $ zeroFor ctx
 
-  check' ctx sg (DLam _ body) ty = do
+  check' ctx sg (DLam body) ty = do
     (ty, l, r) <- expectEq !ask ty
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
     qout <- checkC (extendDim ctx) sg body.term ty.term
@@ -204,11 +184,21 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     expectCompatQ sg.fst g.qty
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
     pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
+   where
+    lookupFree : Name -> m (Definition q)
+    lookupFree x = lookupFree' !ask x
 
   infer' ctx sg (B i) =
     -- if x : A ∈ Γ
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
     pure $ lookupBound sg.fst i ctx.tctx
+   where
+    lookupBound : q -> Var n -> TContext q d n -> InferResult' q d n
+    lookupBound pi VZ (ctx :< ty) =
+      InfRes {type = weakT ty, qout = zeroFor ctx :< pi}
+    lookupBound pi (VS i) (ctx :< _) =
+      let InfRes {type, qout} = lookupBound pi i ctx in
+      InfRes {type = weakT type, qout = qout :< zero}
 
   infer' ctx sg (fun :@ arg) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
@@ -222,7 +212,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       qout = funres.qout + argout
     }
 
-  infer' ctx sg (CasePair pi pair _ ret _ _ body) = do
+  infer' ctx sg (CasePair pi pair ret body) = do
     -- if 1 ≤ π
     expectCompatQ one pi
     -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 89b40b0..c2c9b9c 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -40,6 +40,10 @@ namespace TContext
   pushD : TContext q d n -> TContext q (S d) n
   pushD tel = map (// shift 1) tel
 
+  export %inline
+  zeroFor : IsQty q => Context tm n -> QOutput q n
+  zeroFor ctx = zero <$ ctx
+
 namespace TyContext
   public export %inline
   empty : {d : Nat} -> TyContext q d 0
@@ -75,7 +79,7 @@ namespace QOutput
 
     export %inline
     zeroFor : TyContext q _ n -> QOutput q n
-    zeroFor ctx = zero <$ ctx.tctx
+    zeroFor ctx = zeroFor ctx.tctx
 
 
 public export
diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
index d96aed7..dae6186 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -24,24 +24,24 @@ mutual
     TYPE k == TYPE l = k == l
     TYPE _ == _ = False
 
-    Pi qty1 _ arg1 res1 == Pi qty2 _ arg2 res2 =
+    Pi qty1 arg1 res1 == Pi qty2 arg2 res2 =
       qty1 == qty2 && arg1 == arg2 && res1 == res2
     Pi {} == _ = False
 
-    Lam _ body1 == Lam _ body2 = body1 == body2
+    Lam body1 == Lam body2 = body1 == body2
     Lam {} == _ = False
 
-    Sig _ fst1 snd1 == Sig _ fst2 snd2 = fst1 == fst2 && snd1 == snd2
+    Sig fst1 snd1 == Sig fst2 snd2 = fst1 == fst2 && snd1 == snd2
     Sig {} == _ = False
 
     Pair fst1 snd1 == Pair fst2 snd2 = fst1 == fst2 && snd1 == snd2
     Pair {} == _ = False
 
-    Eq _ ty1 l1 r1 == Eq _ ty2 l2 r2 =
+    Eq ty1 l1 r1 == Eq ty2 l2 r2 =
       ty1 == ty2 && l1 == l2 && r1 == r2
     Eq {} == _ = False
 
-    DLam _ body1 == DLam _ body2 = body1 == body2
+    DLam body1 == DLam body2 = body1 == body2
     DLam {} == _ = False
 
     E e == E f = e == f
@@ -70,7 +70,7 @@ mutual
     (fun1 :@ arg1) == (fun2 :@ arg2) = fun1 == fun2 && arg1 == arg2
     (_ :@ _) == _ = False
 
-    CasePair q1 p1 _ r1 _ _ b1 == CasePair q2 p2 _ r2 _ _ b2 =
+    CasePair q1 p1 r1 b1 == CasePair q2 p2 r2 b2 =
       q1 == q2 && p1 == p2 && r1 == r2 && b1 == b2
     CasePair {} == _ = False
 
@@ -93,18 +93,14 @@ mutual
     DCloE {} == _ = False
 
   export covering
-  Eq q => Eq (ScopeTermN s q d n) where
-    TUsed   s == TUsed   t = s == t
-    TUnused s == TUnused t = s == t
-    TUsed   _ == TUnused _ = False
-    TUnused _ == TUsed   _ = False
+  (forall n. Eq (f n)) => Eq (ScopedBody s f n) where
+    Y x == Y y = x == y
+    N x == N y = x == y
+    _   == _   = False
 
   export covering
-  Eq q => Eq (DScopeTermN s q d n) where
-    DUsed   s == DUsed   t = s == t
-    DUnused s == DUnused t = s == t
-    DUsed   _ == DUnused _ = False
-    DUnused _ == DUsed   _ = False
+  (forall n. Eq (f n)) => Eq (Scoped s f n) where
+    S _ x == S _ y = x == y
 
 export covering
 PrettyHL q => Show (Term q d n) where
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 32e27b2..0fb43b9 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -141,10 +141,10 @@ tests = "equality & subtyping" :- [
       equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
         (["x", "y"] :\\ BVT 1)
         (["x", "y"] :\\ BVT 0),
-    testEq "λ x ⇒ [a] = λ x ⇒ [a]  (TUsed vs TUnused)" $
+    testEq "λ x ⇒ [a] = λ x ⇒ [a]  (Y vs N)" $
       equalT empty (Arr Zero (FT "B") (FT "A"))
-        (Lam "x" $ TUsed   $ FT "a")
-        (Lam "x" $ TUnused $ FT "a"),
+        (Lam $ S ["x"] $ Y $ FT "a")
+        (Lam $ S ["x"] $ N $ FT "a"),
     testEq "λ x ⇒ [f [x]] = [f]  (η)" $
       equalT empty (Arr One (FT "A") (FT "A"))
         (["x"] :\\ E (F "f" :@ BVT 0))
@@ -164,7 +164,7 @@ tests = "equality & subtyping" :- [
 
   "equalities and uip" :-
   let refl : Term q d n -> Term q d n -> Elim q d n
-      refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x)
+      refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
   in
   [
     note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
@@ -208,7 +208,7 @@ tests = "equality & subtyping" :- [
            {globals = defGlobals `mergeLeft` fromList
               [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
       let ty :  forall n. Term Three 0 n
-             := Sig "_" (FT "E") $ TUnused $ FT "E" in
+             := Sig (FT "E") $ S ["_"] $ N $ FT "E" in
       equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ x = y"
@@ -235,11 +235,11 @@ tests = "equality & subtyping" :- [
       equalT empty (FT "A")
         (CloT (BVT 1) (F "a" ::: F "b" ::: id))
         (FT "b"),
-    testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A  (TUnused)" $
+    testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A  (N)" $
       equalT empty (Arr Zero (FT "B") (FT "A"))
-        (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
-        (Lam "y" $ TUnused $ FT "a"),
-    testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A  (TUsed)" $
+        (CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
+        (Lam $ S ["y"] $ N $ FT "a"),
+    testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A  (Y)" $
       equalT empty (Arr Zero (FT "B") (FT "A"))
         (CloT (["y"] :\\ BVT 1) (F "a" ::: id))
         (["y"] :\\ FT "a")
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 59e8348..3cd0ef5 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -4,124 +4,113 @@ import Quox.Syntax as Lib
 import Quox.Syntax.Qty.Three
 import Quox.Equal
 import TermImpls
+import TypingImpls
 import TAP
 
 
-testWhnf : Eq b => Show b => (a -> (Subset b _)) -> String -> a -> b -> Test
-testWhnf whnf label from to = test "\{label}  (whnf)" $ do
-  let result = fst (whnf from)
-  unless (result == to) $
-    Left [("exp", to), ("got", result)] {a = List (String, b)}
+parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex err}
+           {auto _ : ToInfo err}
+           {auto _ : forall d, n. Eq   (tm Three d n)}
+           {auto _ : forall d, n. Show (tm Three d n)}
+           {default empty defs : Definitions Three}
+           {default 0 d, n : Nat}
+  testWhnf : String -> tm Three d n -> tm Three d n -> Test
+  testWhnf label from to = test "\{label}  (whnf)" $ do
+    result <- bimap toInfo fst $ whnf defs from
+    unless (result == to) $ Left [("exp", show to), ("got", show result)]
 
-testNoStep : Eq a => Show a => (a -> (Subset a _)) -> String -> a -> Test
-testNoStep whnf label e = test "\{label}  (no step)" $ do
-  let result = fst (whnf e)
-  unless (result == e) $ Left [("reduced", result)] {a = List (String, a)}
-
-
-
-parameters {default empty defs : Definitions Three} {default 0 d, n : Nat}
-  testWhnfT : String -> Term Three d n -> Term Three d n -> Test
-  testWhnfT = testWhnf (whnf defs)
-
-  testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
-  testWhnfE = testWhnf (whnf defs)
-
-  testNoStepE : String -> Elim Three d n -> Test
-  testNoStepE = testNoStep (whnf defs)
-
-  testNoStepT : String -> Term Three d n -> Test
-  testNoStepT = testNoStep (whnf defs)
+  testNoStep : String -> tm Three d n -> Test
+  testNoStep label e = testWhnf label e e
 
 
 tests = "whnf" :- [
   "head constructors" :- [
-    testNoStepT "★₀" $ TYPE 0,
-    testNoStepT "[A] ⊸ [B]" $
+    testNoStep "★₀" $ TYPE 0,
+    testNoStep "[A] ⊸ [B]" $
       Arr One (FT "A") (FT "B"),
-    testNoStepT "(x: [A]) ⊸ [B [x]]" $
-      Pi One "x" (FT "A") (TUsed $ E $ F "B" :@ BVT 0),
-    testNoStepT "λx. [x]" $
-      Lam "x" $ TUsed $ BVT 0,
-    testNoStepT "[f [a]]" $
+    testNoStep "(x: [A]) ⊸ [B [x]]" $
+      Pi One (FT "A") (S ["x"] $ Y $ E $ F "B" :@ BVT 0),
+    testNoStep "λx. [x]" $
+      Lam $ S ["x"] $ Y $ BVT 0,
+    testNoStep "[f [a]]" $
       E $ F "f" :@ FT "a"
   ],
 
+
   "neutrals" :- [
-    testNoStepE "x" {n = 1} $ BV 0,
-    testNoStepE "a"         $ F "a",
-    testNoStepE "f [a]"     $ F "f" :@ FT "a",
-    testNoStepE "★₀ ∷ ★₁"   $ TYPE 0 :# TYPE 1
+    testNoStep "x" {n = 1} $ BV 0,
+    testNoStep "a"         $ F "a",
+    testNoStep "f [a]"     $ F "f" :@ FT "a",
+    testNoStep "★₀ ∷ ★₁"   $ TYPE 0 :# TYPE 1
   ],
 
   "redexes" :- [
-    testWhnfE "[a] ∷ [A]"
+    testWhnf "[a] ∷ [A]"
       (FT "a" :# FT "A")
       (F "a"),
-    testWhnfT "[★₁ ∷ ★₃]"
+    testWhnf "[★₁ ∷ ★₃]"
       (E (TYPE 1 :# TYPE 3))
       (TYPE 1),
-    testWhnfE "(λx. [x] ∷ [A] ⊸ [A]) [a]"
-      ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+    testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]"
+      (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
       (F "a")
   ],
 
   "definitions" :- [
-    testWhnfE "a  (transparent)"
+    testWhnf "a  (transparent)"
       {defs = fromList [("a", mkDef Zero (TYPE 1) (TYPE 0))]}
       (F "a") (TYPE 0 :# TYPE 1)
   ],
 
   "elim closure" :- [
-    testWhnfE "x{}" {n = 1}
+    testWhnf "x{}" {n = 1}
       (CloE (BV 0) id)
       (BV 0),
-    testWhnfE "x{a/x}"
+    testWhnf "x{a/x}"
       (CloE (BV 0) (F "a" ::: id))
       (F "a"),
-    testWhnfE "x{x/x,a/y}" {n = 1}
+    testWhnf "x{x/x,a/y}" {n = 1}
       (CloE (BV 0) (BV 0 ::: F "a" ::: id))
       (BV 0),
-    testWhnfE "x{(y{a/y})/x}"
+    testWhnf "x{(y{a/y})/x}"
       (CloE (BV 0) ((CloE (BV 0) (F "a" ::: id)) ::: id))
       (F "a"),
-    testWhnfE "(x y){f/x,a/y}"
+    testWhnf "(x y){f/x,a/y}"
       (CloE (BV 0 :@ BVT 1) (F "f" ::: F "a" ::: id))
       (F "f" :@ FT "a"),
-    testWhnfE "([y] ∷ [x]){A/x}" {n = 1}
+    testWhnf "([y] ∷ [x]){A/x}" {n = 1}
       (CloE (BVT 1 :# BVT 0) (F "A" ::: id))
       (BV 0),
-    testWhnfE "([y] ∷ [x]){A/x,a/y}"
+    testWhnf "([y] ∷ [x]){A/x,a/y}"
       (CloE (BVT 1 :# BVT 0) (F "A" ::: F "a" ::: id))
       (F "a")
   ],
 
   "term closure" :- [
-    testWhnfT "(λy. x){a/x}"
-      (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
-      (Lam "y" $ TUnused $ FT "a"),
-    testWhnfT "(λy. y){a/x}"
-      (CloT (Lam "y" $ TUsed $ BVT 0) (F "a" ::: id))
-      (Lam "y" $ TUsed $ BVT 0)
+    testWhnf "(λy. x){a/x}"
+      (CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
+      (Lam $ S ["y"] $ N $ FT "a"),
+    testWhnf "(λy. y){a/x}"
+      (CloT (["y"] :\\ BVT 0) (F "a" ::: id))
+      (["y"] :\\ BVT 0)
   ],
 
   "looking inside […]" :- [
-    testWhnfT "[(λx. x ∷ A ⊸ A) [a]]"
-      (E $ (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+    testWhnf "[(λx. x ∷ A ⊸ A) [a]]"
+      (E $ ((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
       (FT "a")
   ],
 
   "nested redex" :- [
     note "whnf only looks at top level redexes",
-    testNoStepT "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
-      Lam "y" $ TUsed $ E $
-        (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0,
-    testNoStepE "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
+    testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
+      ["y"] :\\ E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
+    testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
       F "a" :@
-      E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
-    testNoStepT "λx. [y [x]]{x/x,a/y}" {n = 1} $
-      Lam "x" $ TUsed $ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
-    testNoStepE "f ([y [x]]{x/x,a/y})" {n = 1} $
+      E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
+    testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $
+      ["x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
+    testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $
       F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
   ]
 ]
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index cb3633b..2f44ef2 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -36,8 +36,8 @@ inj act = do
 
 reflTy : IsQty q => Term q d n
 reflTy =
-  Pi zero "A" (TYPE 0) $ TUsed $
-  Pi one  "x" (BVT 0)  $ TUsed $
+  Pi zero (TYPE 0) $ S ["A"] $ Y $
+  Pi one  (BVT 0)  $ S ["x"] $ Y $
   Eq0 (BVT 1) (BVT 0) (BVT 0)
 
 reflDef : IsQty q => Term q d n
@@ -56,8 +56,8 @@ defGlobals = fromList
    ("f",  mkAbstract Any  $ Arr One (FT "A") (FT "A")),
    ("g",  mkAbstract Any  $ Arr One (FT "A") (FT "B")),
    ("f2", mkAbstract Any  $ Arr One (FT "A") $ Arr One (FT "A") (FT "A")),
-   ("p",  mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
-   ("q",  mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
+   ("p",  mkAbstract Any  $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0),
+   ("q",  mkAbstract Any  $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0),
    ("refl", mkDef Any reflTy reflDef)]
 
 parameters (label : String) (act : Lazy (M ()))
@@ -139,7 +139,7 @@ tests = "typechecker" :- [
       check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0),
     testTC "0 · (1·x : A) → P x ⇐ ★₀" $
       check_ (ctx [<]) szero
-        (Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
+        (Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0)
         (TYPE 0),
     testTCFail "0 · A ⊸ P ⇍ ★₀" $
       check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0),
@@ -207,21 +207,20 @@ tests = "typechecker" :- [
 
   "equalities" :- [
     testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
-      check_ (ctx [<]) sone (DLam "i" $ DUnused $ FT "a")
+      check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a")
         (Eq0 (FT "A") (FT "a") (FT "a")),
     testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ (ctx [<]) szero
-        (Lam "p" $ TUsed $ Lam "q" $ TUnused $
-         DLam "i" $ DUnused $ BVT 0)
-        (Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
-         Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
+        (Lam $ S ["p"] $ Y $ Lam $ S ["q"] $ N $ DLam $ S ["i"] $ N $ BVT 0)
+        (Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $
+         Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
     testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ (ctx [<]) szero
-        (Lam "p" $ TUnused $ Lam "q" $ TUsed $
-         DLam "i" $ DUnused $ BVT 0)
-        (Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
-         Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
+        (Lam $ S ["p"] $ N $ Lam $ S ["q"] $ Y $
+         DLam $ S ["i"] $ N $ BVT 0)
+        (Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $
+         Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
   ],
 
@@ -233,11 +232,11 @@ tests = "typechecker" :- [
     testTC "cong" $
       check_ (ctx [<]) sone
         (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
-        (Pi Zero "x"  (FT "A") $ TUsed $
-         Pi Zero "y"  (FT "A") $ TUsed $
-         Pi One  "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $ TUsed $
-         Eq "i" (DUsed $ E $ F "P" :@ E (BV 0 :% BV 0))
-                (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
+        (Pi Zero (FT "A") $ S ["x"] $ Y $
+         Pi Zero (FT "A") $ S ["y"] $ Y $
+         Pi One  (Eq0 (FT "A") (BVT 1) (BVT 0)) $ S ["xy"] $ Y $
+         Eq (S ["i"] $ Y $ E $ F "P" :@ E (BV 0 :% BV 0))
+            (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
     note "0·A : Type, 0·P : ω·A → Type,",
     note "ω·p q : (1·x : A) → P x",
     note "⊢",
@@ -246,11 +245,12 @@ tests = "typechecker" :- [
     testTC "funext" $
       check_ (ctx [<]) sone
         (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
-        (Pi One "eq"
-            (Pi One "x" (FT "A") $ TUsed $
+        (Pi One
+            (Pi One (FT "A") $ S ["x"] $ Y $
               Eq0 (E $ F "P" :@ BVT 0)
-                  (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $ TUsed $
-         Eq0 (Pi Any "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
-             (FT "p") (FT "q"))
+                  (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $
+            S ["eq"] $ Y $
+              Eq0 (Pi Any (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0)
+                  (FT "p") (FT "q"))
   ]
 ]