From 42798f243ffc4e9ea464a677b9a66ae98d4af0df Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 10 Feb 2023 21:40:44 +0100
Subject: [PATCH] typed equality

---
 lib/Quox/Definition.idr         |  12 +-
 lib/Quox/Equal.idr              | 357 ++++++++++++++++++++------------
 lib/Quox/Syntax/Term/Reduce.idr |   9 -
 lib/Quox/Syntax/Term/Subst.idr  |  22 +-
 lib/Quox/Typechecker.idr        |  24 +--
 lib/Quox/Typing.idr             |  22 +-
 tests/Tests/Equal.idr           | 206 +++++++++++-------
 tests/Tests/Reduce.idr          |   8 +-
 8 files changed, 410 insertions(+), 250 deletions(-)

diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index b8c55fe..87750df 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -35,6 +35,10 @@ mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
 mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
 
 
+public export %inline
+(.get0) : AnyTerm q -> Term q 0 0
+t.get0 = t.get
+
 public export %inline
 (.type0) : Definition' q _ -> Term q 0 0
 g.type0 = g.type.get
@@ -117,10 +121,10 @@ NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs)
 parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
   namespace Term
     export %inline
-    whnf : Term q d n -> NonRedexTerm q d n defs
-    whnf = whnf $ \x => lookupElim x defs
+    whnfD : Term q d n -> NonRedexTerm q d n defs
+    whnfD = whnf $ \x => lookupElim x defs
 
   namespace Elim
     export %inline
-    whnf : Elim q d n -> NonRedexElim q d n defs
-    whnf = whnf $ \x => lookupElim x defs
+    whnfD : Elim q d n -> NonRedexElim q d n defs
+    whnfD = whnf $ \x => lookupElim x defs
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 56ec958..852558d 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -9,8 +9,8 @@ import Data.Maybe
 
 
 private %inline
-ClashE : EqMode -> Elim q d n -> Elim q d n -> Error q
-ClashE mode = ClashT mode `on` E
+ClashE : EqMode -> Term q d n -> Elim q d n -> Elim q d n -> Error q
+ClashE mode ty = ClashT mode ty `on` E
 
 
 public export
@@ -34,179 +34,262 @@ mode : HasEnv m => m EqMode
 mode = asks mode
 
 private %inline
-clashT : CanEqual q m => Term q d n -> Term q d n -> m a
-clashT s t = throwError $ ClashT !mode s t
+clashT : CanEqual q m => Term q d n -> Term q d n -> Term q d n -> m a
+clashT ty s t = throwError $ ClashT !mode ty s t
 
 private %inline
 clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a
 clashE e f = throwError $ ClashE !mode e f
 
 
-parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
+public export %inline
+isType : (t : Term {}) -> Bool
+isType (TYPE  {}) = True
+isType (Pi    {}) = True
+isType (Lam   {}) = False
+isType (Sig   {}) = True
+isType (Pair  {}) = False
+isType (Eq    {}) = True
+isType (DLam  {}) = False
+isType (E     {}) = True
+isType (CloT  {}) = False
+isType (DCloT {}) = False
+
+
+parameters {auto _ : HasErr q m}
+  export %inline
+  ensure : (a -> Error q) -> (p : a -> Bool) -> (t : a) -> m (So (p t))
+  ensure e p t = case nchoose $ p t of
+    Left y  => pure y
+    Right n => throwError $ e t
+
+  export %inline
+  ensureType : (t : Term q d n) -> m (So (isType t))
+  ensureType = ensure NotType isType
+
+parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
   mutual
+    -- [todo] remove cumulativity & subtyping, it's too much of a pain
+    -- mugen might be good
     namespace Term
-      export covering
-      compareN' : CanEqual q m => Eq q =>
-                  (s, t : Term q 0 n) ->
-                  (0 _ : NotRedex defs s) -> (0 _ : NotRedex defs t) ->
+      export covering %inline
+      compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
+      compare0 ctx ty s t = do
+        let Element ty nty = whnfD defs ty
+            Element s  ns  = whnfD defs s
+            Element t  nt  = whnfD defs t
+        tty <- ensureType ty
+        compare0' ctx ty s t
+
+      private %inline
+      toLamBody : Elim q d n -> Term q d (S n)
+      toLamBody e = E $ weakE e :@ BVT 0
+
+      private covering
+      compare0' : TContext q 0 n ->
+                  (ty, s, t : Term q 0 n) ->
+                  (0 nty : NotRedex defs ty) => (0 tty : So (isType ty)) =>
+                  (0 ns  : NotRedex defs s)  => (0 nt  : NotRedex defs t) =>
                   m ()
+      compare0' ctx (TYPE _) s t = compareType ctx s t
 
-      compareN' (TYPE k) (TYPE l) _ _ = expectModeU !mode k l
-      compareN' s@(TYPE _) t _ _ = clashT s t
+      compare0' ctx ty@(Pi {arg, res, _}) s t = local {mode := Equal} $
+        let ctx' = ctx :< arg
+            eta : Elim q 0 ? -> ScopeTerm q 0 ? -> m ()
+            eta e (TUsed   b) = compare0 ctx' res.term (toLamBody e) b
+            eta e (TUnused _) = clashT ty s t
+        in
+        case (s, t) of
+          (Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
+          (E e,      Lam _ b)  => eta e b
+          (Lam _ b,  E e)      => eta e b
+          (E e,      E f)      => ignore $ compare0 ctx e f
+          _ => throwError $ WrongType ty s t
 
-      compareN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
-        expectEqualQ qty1 qty2
-        compare0 arg2 arg1 -- reversed for contravariant domain
-        compare0 res1 res2
-      compareN' s@(Pi {}) t _ _ = clashT s t
+      compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
+        -- no η (no fst/snd for π ≱ 0), so…
+        -- [todo] η for π ≥ 0 maybe
+        case (s, t) of
+          (Pair sFst sSnd, Pair tFst tSnd) => do
+            compare0 ctx fst sFst tFst
+            compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
+          _ => throwError $ WrongType ty s t
 
-      -- [todo] eta
-      compareN' (Lam _ body1) (Lam _ body2) _ _ =
-        local {mode := Equal} $ compare0 body1 body2
-      compareN' s@(Lam {}) t _ _ = clashT s t
+      -- ✨ uip ✨
+      compare0' _ (Eq {}) _ _ = pure ()
 
-      compareN' (Sig _ fst1 snd1) (Sig _ fst2 snd2) _ _ = do
-        compare0 fst1 fst2
-        compare0 snd1 snd2
-      compareN' s@(Sig {}) t _ _ = clashT s t
+      compare0' ctx ty@(E _) s t = do
+        -- a neutral type can only be inhabited by neutral values
+        -- e.g. an abstract value in an abstract type, bound variables, …
+        E e <- pure s | _ => throwError $ WrongType ty s t
+        E f <- pure t | _ => throwError $ WrongType ty s t
+        ignore $ compare0 ctx e f
 
-      compareN' (Pair fst1 snd1) (Pair fst2 snd2) _ _ =
-        local {mode := Equal} $ do
-          compare0 fst1 fst2
-          compare0 snd1 snd2
-      compareN' s@(Pair {}) t _ _ = clashT s t
+    export covering
+    compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
+    compareType ctx s t = do
+      let Element s ns = whnfD defs s
+          Element t nt = whnfD defs t
+      sok <- ensureType s
+      tok <- ensureType t
+      compareType' ctx s t
 
-      compareN' (Eq _ ty1 l1 r1) (Eq _ ty2 l2 r2) _ _ = do
-        compare0 ty1 ty2
-        local {mode := Equal} $ do
-          compare0 l1 l2
-          compare0 r1 r2
-      compareN' s@(Eq {}) t _ _ = clashT s t
+    private covering
+    compareType' : TContext q 0 n -> (s, t : Term q 0 n) ->
+                   (0 ns : NotRedex defs s) => (0 ts : So (isType s)) =>
+                   (0 nt : NotRedex defs t) => (0 tt : So (isType t)) =>
+                   m ()
+    compareType' ctx s t = do
+      let err : m () = clashT (TYPE UAny) s t
+      case s of
+        TYPE k => do
+          TYPE l <- pure t | _ => err
+          expectModeU !mode k l
 
-      compareN' (DLam _ body1) (DLam _ body2) _ _ =
-        local {mode := Equal} $ do
-          compare0 body1 body2
-      compareN' s@(DLam {}) t _ _ = clashT s t
+        Pi {qty = sQty, arg = sArg, res = sRes, _} => do
+          Pi {qty = tQty, arg = tArg, res = tRes, _} <- pure t | _ => err
+          expectEqualQ sQty tQty
+          compareType ctx tArg sArg -- contra
+          -- [todo] is using sArg also ok for subtyping?
+          compareType (ctx :< sArg) sRes.term tRes.term
 
-      compareN' (E e) (E f) ne nf = compareN' e f (noOr2 ne) (noOr2 nf)
-      compareN' s@(E e) t _ _ = clashT s t
+        Sig {fst = sFst, snd = sSnd, _} => do
+          Sig {fst = tFst, snd = tSnd, _} <- pure t | _ => err
+          compareType ctx sFst tFst
+          compareType (ctx :< sFst) sSnd.term tSnd.term
+
+        Eq {ty = sTy, l = sl, r = sr, _} => do
+          Eq {ty = tTy, l = tl, r = tr, _} <- pure t | _ => err
+          compareType ctx sTy.zero tTy.zero
+          compareType ctx sTy.one  tTy.one
+          local {mode := Equal} $ do
+            compare0 ctx sTy.zero sl tl
+            compare0 ctx sTy.one  sr tr
+
+        E e => do
+          E f <- pure t | _ => err
+          -- no fanciness needed here cos anything other than a neutral
+          -- has been inlined by whnfD
+          ignore $ compare0 ctx e f
 
     namespace Elim
-      export covering
-      compareN' : CanEqual q m => Eq q =>
+      export covering %inline
+      compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m (Term q 0 n)
+      compare0 ctx e f =
+        let Element e ne = whnfD defs e
+            Element f nf = whnfD defs f
+        in
+        compare0' ctx e f
+
+      private
+      isSubSing : Term {} -> Bool
+      isSubSing (TYPE _)            = False
+      isSubSing (Pi {res, _})       = isSubSing res.term
+      isSubSing (Lam {})            = False
+      isSubSing (Sig {fst, snd, _}) = isSubSing fst && isSubSing snd.term
+      isSubSing (Pair {})           = False
+      isSubSing (Eq {})             = True
+      isSubSing (DLam {})           = False
+      isSubSing (E e)               = False
+      isSubSing (CloT tm th)        = False
+      isSubSing (DCloT tm th)       = False
+
+      private covering
+      compare0' : TContext q 0 n ->
                   (e, f : Elim q 0 n) ->
-                  (0 _ : NotRedex defs e) -> (0 _ : NotRedex defs f) ->
-                  m ()
+                  (0 ne : NotRedex defs e) => (0 nf : NotRedex defs f) =>
+                  m (Term q 0 n)
+      compare0' _ e@(F x) f@(F y) = do
+        d <- lookupFree' defs x
+        let ty = d.type
+        -- [fixme] there is a better way to do this for sure
+        unless (isSubSing ty.get0 || x == y) $ clashE e f
+        pure ty.get
+      compare0' _ e@(F _) f = clashE e f
 
-      compareN' e@(F x) f@(F y) _ _ =
-        unless (x == y) $ clashE e f
-      compareN' e@(F _) f _ _ = clashE e f
+      compare0' ctx e@(B i) f@(B j) = do
+        let ty = ctx !! i
+        -- [fixme] there is a better way to do this for sure
+        unless (isSubSing ty || i == j) $ clashE e f
+        pure ty
+      compare0' _ e@(B _) f = clashE e f
 
-      compareN' e@(B i) f@(B j) _ _ =
-        unless (i == j) $ clashE e f
-      compareN' e@(B _) f _ _ = clashE e f
+      compare0' ctx (e :@ s) (f :@ t) = local {mode := Equal} $ do
+        Pi {arg, res, _} <- compare0 ctx e f
+          | ty => throwError $ ExpectedPi ty
+        compare0 ctx arg s t
+        pure $ sub1 res (s :# arg)
+      compare0' _ e@(_ :@ _) f = clashE e f
 
-      -- [todo] tracking variance of functions? maybe???
-      -- probably not
-      compareN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
+      compare0' ctx (CasePair epi e _ eret _ _ ebody)
+                    (CasePair fpi f _ fret _ _ fbody) =
         local {mode := Equal} $ do
-          compare0 fun1 fun2
-          compare0 arg1 arg2
-      compareN' e@(_ :@ _) f _ _ = clashE e f
+          ty@(Sig {fst, snd, _}) <- compare0 ctx e f
+            | ty => throwError $ ExpectedSig ty
+          unless (epi == fpi) $ throwError $ ClashQ epi fpi
+          compareType (ctx :< ty) eret.term fret.term
+          compare0 (ctx :< fst :< snd.term) (substCasePairRet ty eret)
+            ebody.term fbody.term
+          pure $ sub1 eret e
+      compare0' _ e@(CasePair {}) f = clashE e f
 
-      compareN' (CasePair pi1 pair1 _ ret1 _ _ body1)
-                (CasePair pi2 pair2 _ ret2 _ _ body2) _ _ =
-        local {mode := Equal} $ do
-          expectEqualQ pi1 pi2
-          compare0 pair1 pair2
-          compare0 ret1  ret2
-          compare0 body1 body2
-      compareN' e@(CasePair {}) f _ _ = clashE e f
+      compare0' ctx (e :% p) (f :% q) = local {mode := Equal} $ do
+        Eq {ty, _} <- compare0 ctx e f
+          | ty => throwError $ ExpectedEq ty
+        unless (p == q) $ throwError $ ClashD p q
+        pure $ dsub1 ty p
+      compare0' _ e@(_ :% _) f = clashE e f
 
-      -- retain the mode unlike above because dimensions can't do
-      -- anything that would mess up variance
-      compareN' (fun1 :% dim1) (fun2 :% dim2) _ _ = do
-        compare0 fun1 fun2
-        expectEqualD dim1 dim2
-      compareN' e@(_ :% _) f _ _ = clashE e f
-
-      -- using the same mode for the type allows, e.g.
-      -- A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B
-      -- which, since A : ★₁ implies A : ★₃, should be fine
-      compareN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
-        compare0 tm1 tm2
-        compare0 ty1 ty2
-      compareN' e@(_ :# _) f _ _ = clashE e f
+      compare0' ctx (s :# a) (t :# b) = do
+        compareType ctx a b
+        compare0 ctx a s t
+        pure b
+      compare0' _ e@(_ :# _) f = clashE e f
 
 
+parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)}
+           (eq : DimEq d) (ctx : TContext q d n)
+  parameters (mode : EqMode)
     namespace Term
-      export covering %inline
-      compareN : CanEqual q m => Eq q =>
-                 NonRedexTerm q 0 n defs -> NonRedexTerm q 0 n defs -> m ()
-      compareN s t = compareN' s.fst t.fst s.snd t.snd
+      export covering
+      compare : (ty, s, t : Term q d n) -> m ()
+      compare ty s t = do
+        defs <- ask
+        runReaderT {m} (MakeEnv {mode}) $
+          for_ (splits eq) $ \th =>
+            compare0 defs (map (/// th) ctx) (ty /// th) (s /// th) (t /// th)
 
-      export covering %inline
-      compare : CanEqual q m => Eq q =>
-                DimEq d -> Term q d n -> Term q d n -> m ()
-      compare eqs s t =
-        for_ (splits eqs) $ \th => compare0 (s /// th) (t /// th)
-
-      export covering %inline
-      compare0 : CanEqual q m => Eq q => Term q 0 n -> Term q 0 n -> m ()
-      compare0 s t = compareN (whnf defs s) (whnf defs t)
+      export covering
+      compareType : (s, t : Term q d n) -> m ()
+      compareType s t = do
+        defs <- ask
+        runReaderT {m} (MakeEnv {mode}) $
+          for_ (splits eq) $ \th =>
+            compareType defs (map (/// th) ctx) (s /// th) (t /// th)
 
     namespace Elim
-      covering %inline
-      compareN : CanEqual q m => Eq q =>
-                 NonRedexElim q 0 n defs -> NonRedexElim q 0 n defs -> m ()
-      compareN e f = compareN' e.fst f.fst e.snd f.snd
-
+      -- can't return the type since it might be different in each dsubst ☹
       export covering %inline
-      compare : CanEqual q m => Eq q =>
-                DimEq d -> Elim q d n -> Elim q d n -> m ()
-      compare eqs e f =
-        for_ (splits eqs) $ \th => compare0 (e /// th) (f /// th)
-
-      export covering %inline
-      compare0 : CanEqual q m => Eq q => Elim q 0 n -> Elim q 0 n -> m ()
-      compare0 e f = compareN (whnf defs e) (whnf defs f)
-
-    namespace ScopeTermN
-      export covering %inline
-      compare0 : {s : Nat} -> CanEqual q m => Eq q =>
-                 ScopeTermN s q 0 n -> ScopeTermN s q 0 n -> m ()
-      compare0 (TUnused body0) (TUnused body1) = compare0 body0 body1
-      compare0 body0 body1 = compare0 body0.term body1.term
-
-    -- [todo] extend to multi-var scopes
-    namespace DScopeTerm
-      export covering %inline
-      compare0 : CanEqual q m => Eq q =>
-                 DScopeTerm q 0 n -> DScopeTerm q 0 n -> m ()
-      compare0 (DUnused body0) (DUnused body1) = compare0 body0 body1
-      compare0 body0 body1 = do
-        compare0 body0.zero body1.zero
-        compare0 body0.one  body1.one
-
+      compare : (e, f : Elim q d n) -> m ()
+      compare e f = do
+        defs <- ask
+        runReaderT {m} (MakeEnv {mode}) $
+          for_ (splits eq) $ \th =>
+            ignore $ compare0 defs (map (/// th) ctx) (e /// th) (f /// th)
 
   namespace Term
     export covering %inline
-    equal : HasErr q m => Eq q =>
-            DimEq d -> Term q d n -> Term q d n -> m ()
-    equal eqs s t {m} = runReaderT {m} (MakeEnv Equal) $ compare eqs s t
+    equal, sub : (ty, s, t : Term q d n) -> m ()
+    equal = compare Equal
+    sub   = compare Sub
 
     export covering %inline
-    sub : HasErr q m => HasDefs' q _ m => Eq q =>
-          DimEq d -> Term q d n -> Term q d n -> m ()
-    sub eqs s t {m} = runReaderT {m} (MakeEnv Sub) $ compare eqs s t
+    equalType, subtype : (s, t : Term q d n) -> m ()
+    equalType = compareType Equal
+    subtype   = compareType Sub
 
   namespace Elim
     export covering %inline
-    equal : HasErr q m => Eq q =>
-            DimEq d -> Elim q d n -> Elim q d n -> m ()
-    equal eqs e f {m} = runReaderT {m} (MakeEnv Equal) $ compare eqs e f
-
-    export covering %inline
-    sub : HasErr q m => HasDefs' q _ m => Eq q =>
-          DimEq d -> Elim q d n -> Elim q d n -> m ()
-    sub eqs e f {m} = runReaderT {m} (MakeEnv Sub) $ compare eqs e f
+    equal, sub : (e, f : Elim q d n) -> m ()
+    equal = compare Equal
+    sub   = compare Sub
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index 7ef6e33..b101dc8 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -125,15 +125,6 @@ parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
     pushSubstsWith' e = (pushSubstsWith th ph e).fst
 
 
-public export %inline
-weakT : Term q d n -> Term q d (S n)
-weakT t = t //. shift 1
-
-public export %inline
-weakE : Elim q d n -> Elim q d (S n)
-weakE t = t //. shift 1
-
-
 public export 0
 Lookup : TermLike
 Lookup q d n = Name -> Maybe $ Elim q d n
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index ea6c0dc..e7be95f 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -184,17 +184,35 @@ comp : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
 comp th ps ph = map (/// th) ps . ph
 
 
+public export %inline
+dweakT : {by : Nat} -> Term q d n -> Term q (by + d) n
+dweakT t = t /// shift by
+
+public export %inline
+dweakE : {by : Nat} -> Elim q d n -> Elim q (by + d) n
+dweakE t = t /// shift by
+
+
+public export %inline
+weakT : {default 1 by : Nat} -> Term q d n -> Term q d (by + n)
+weakT t = t //. shift by
+
+public export %inline
+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 = body //. shift s
+  (TUnused body).term = weakT body {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 = body /// shift s
+  (DUnused body).term = dweakT body {by = s}
 
 
 export %inline
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 5b39816..a8aa178 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -22,7 +22,7 @@ CanTC q = CanTC' q IsGlobal
 private covering %inline
 expectTYPE : CanTC' q _ m => Term q d n -> m Universe
 expectTYPE s =
-  case whnf !ask s of
+  case whnfD !ask s of
     Element (TYPE l) _ => pure l
     _ => throwError $ ExpectedTYPE s
 
@@ -30,7 +30,7 @@ private covering %inline
 expectPi : CanTC' q _ m => Term q d n ->
            m (q, Term q d n, ScopeTerm q d n)
 expectPi ty =
-  case whnf !ask ty of
+  case whnfD !ask ty of
     Element (Pi qty _ arg res) _ => pure (qty, arg, res)
     _ => throwError $ ExpectedPi ty
 
@@ -38,7 +38,7 @@ private covering %inline
 expectSig : CanTC' q _ m => Term q d n ->
             m (Term q d n, ScopeTerm q d n)
 expectSig ty =
-  case whnf !ask ty of
+  case whnfD !ask ty of
     Element (Sig _ arg res) _ => pure (arg, res)
     _ => throwError $ ExpectedSig ty
 
@@ -46,7 +46,7 @@ private covering %inline
 expectEq : CanTC' q _ m => Term q d n ->
            m (DScopeTerm q d n, Term q d n, Term q d n)
 expectEq ty =
-  case whnf !ask ty of
+  case whnfD !ask ty of
     Element (Eq _ ty l r) _ => pure (ty, l, r)
     _ => throwError $ ExpectedEq ty
 
@@ -80,11 +80,8 @@ lookupBound pi (VS i) ctx =
   weakI $ lookupBound pi i (tail ctx)
 
 private
-lookupFree : IsQty q => CanTC q m => Name -> m (Definition q)
-lookupFree x =
-  case lookup x !ask of
-    Just d  => pure d
-    Nothing => throwError $ NotInScope x
+lookupFree : CanTC' q g m => Name -> m (Definition' q g)
+lookupFree x = lookupFree' !ask x
 
 private %inline
 subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
@@ -202,9 +199,9 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     qout <- check (extendDim ctx) sg body.term ty.term
     let eqs = makeDimEq ctx.dctx
     -- if Ψ ⊢ t‹0› = l
-    equal !ask eqs body.zero l
+    equal eqs ctx.tctx ty.zero body.zero l
     -- if Ψ ⊢ t‹1› = r
-    equal !ask eqs body.one  r
+    equal eqs ctx.tctx ty.one  body.one  r
     -- then Ψ | Γ ⊢ (λᴰi ⇒ t) · σ ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
@@ -212,7 +209,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ e · σ ⇒ A' ⊳ Σ
     infres <- infer ctx sg e
     -- if Ψ ⊢ A' <: A
-    sub !ask (makeDimEq ctx.dctx) infres.type ty
+    subtype (makeDimEq ctx.dctx) ctx.tctx infres.type ty
     -- then Ψ | Γ ⊢ e · σ ⇐ A ⊳ Σ
     pure infres.qout
 
@@ -258,8 +255,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     --      ⊳ Σ₂, x · π₁, y · π₂
     -- if π₁, π₂ ≤ π
     let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx
-        retarg  = Pair (BVT 0) (BVT 1) :# (pairres.type // fromNat 2)
-        bodyty  = ret.term // (retarg ::: shift 2)
+        bodyty  = substCasePairRet pairres.type ret
     bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
     -- then Ψ | Γ ⊢ σ case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 571122a..21f0b3f 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -121,12 +121,17 @@ data Error q
 | ExpectedEq   (Term q d n)
 | BadUniverse  Universe Universe
 
-| ClashT EqMode (Term q d n) (Term q d n)
+-- first arg of ClashT is the type
+| ClashT EqMode (Term q d n) (Term q d n) (Term q d n)
+| ClashE EqMode (Elim q d n) (Elim q d n)
 | ClashU EqMode Universe     Universe
 | ClashQ        q            q
 | ClashD        (Dim d)      (Dim d)
 | NotInScope    Name
 
+| NotType (Term q d n)
+| WrongType (Term q d n) (Term q d n) (Term q d n)
+
 public export
 0 HasErr : Type -> (Type -> Type) -> Type
 HasErr q = MonadError (Error q)
@@ -157,3 +162,18 @@ parameters {auto _ : HasErr q m}
   export %inline
   expectEqualD : Dim d -> Dim d -> m ()
   expectEqualD = expect ClashD (==)
+
+
+export
+lookupFree' : HasErr q m => Definitions' q g -> Name -> m (Definition' q g)
+lookupFree' defs x =
+  case lookup x defs of
+    Just d  => pure d
+    Nothing => throwError $ NotInScope x
+
+
+export
+substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
+substCasePairRet dty retty =
+  let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
+  retty.term // (arg ::: shift 2)
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 94d1246..c08b1fc 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -26,11 +26,17 @@ ToInfo (Error Three) where
     [("type", "BadUniverse"),
      ("low",  show k),
      ("high", show l)]
-  toInfo (ClashT mode s t) =
+  toInfo (ClashT mode ty s t) =
     [("type", "ClashT"),
      ("mode",  show mode),
+     ("ty",    prettyStr True ty),
      ("left",  prettyStr True s),
      ("right", prettyStr True t)]
+  toInfo (ClashE mode e f) =
+    [("type", "ClashE"),
+     ("mode",  show mode),
+     ("left",  prettyStr True e),
+     ("right", prettyStr True f)]
   toInfo (ClashU mode k l) =
     [("type", "ClashU"),
      ("mode",  show mode),
@@ -44,13 +50,29 @@ ToInfo (Error Three) where
     [("type", "ClashD"),
      ("left",  prettyStr True p),
      ("right", prettyStr True q)]
+  toInfo (NotType ty) =
+    [("type",   "NotType"),
+     ("actual", prettyStr True ty)]
+  toInfo (WrongType ty s t) =
+    [("type", "WrongType"),
+     ("ty",    prettyStr True ty),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
 
 
 0 M : Type -> Type
 M = ReaderT (Definitions Three) (Either (Error Three))
 
+defGlobals : Definitions Three
+defGlobals = fromList
+  [("A", mkAbstract Zero $ TYPE 0),
+   ("B", mkAbstract Zero $ TYPE 0),
+   ("a", mkAbstract Any  $ FT "A"),
+   ("b", mkAbstract Any  $ FT "B"),
+   ("f", mkAbstract Any  $ Arr One (FT "A") (FT "A"))]
+
 parameters (label : String) (act : Lazy (M ()))
-           {default empty globals : Definitions Three}
+           {default defGlobals globals : Definitions Three}
   testEq : Test
   testEq = test label $ runReaderT globals act
 
@@ -60,17 +82,18 @@ parameters (label : String) (act : Lazy (M ()))
 
 parameters {default 0   d, n : Nat}
            {default new eqs  : DimEq d}
-  subT : Term Three d n -> Term Three d n -> M ()
-  subT s t = Term.sub !ask eqs s t
+           (ctx : TContext Three d n)
+  subT : Term Three d n -> Term Three d n -> Term Three d n -> M ()
+  subT ty s t = Term.sub eqs ctx ty s t
 
-  equalT : Term Three d n -> Term Three d n -> M ()
-  equalT s t = Term.equal !ask eqs s t
+  equalT : Term Three d n -> Term Three d n -> Term Three d n -> M ()
+  equalT ty s t = Term.equal eqs ctx ty s t
 
   subE : Elim Three d n -> Elim Three d n -> M ()
-  subE e f = Elim.sub !ask eqs e f
+  subE e f = Elim.sub eqs ctx e f
 
   equalE : Elim Three d n -> Elim Three d n -> M ()
-  equalE e f = Elim.equal !ask eqs e f
+  equalE e f = Elim.equal eqs ctx e f
 
 
 export
@@ -80,17 +103,17 @@ tests = "equality & subtyping" :- [
 
   "universes" :- [
     testEq "★₀ ≡ ★₀" $
-      equalT (TYPE 0) (TYPE 0),
+      equalT [<] (TYPE 1) (TYPE 0) (TYPE 0),
     testNeq "★₀ ≢ ★₁" $
-      equalT (TYPE 0) (TYPE 1),
+      equalT [<] (TYPE 2) (TYPE 0) (TYPE 1),
     testNeq "★₁ ≢ ★₀" $
-      equalT (TYPE 1) (TYPE 0),
+      equalT [<] (TYPE 2) (TYPE 1) (TYPE 0),
     testEq "★₀ <: ★₀" $
-      subT (TYPE 0) (TYPE 0),
+      subT [<] (TYPE 1) (TYPE 0) (TYPE 0),
     testEq "★₀ <: ★₁" $
-      subT (TYPE 0) (TYPE 1),
+      subT [<] (TYPE 2) (TYPE 0) (TYPE 1),
     testNeq "★₁ ≮: ★₀" $
-      subT (TYPE 1) (TYPE 0)
+      subT [<] (TYPE 2) (TYPE 1) (TYPE 0)
   ],
 
   "pi" :- [
@@ -98,79 +121,91 @@ tests = "equality & subtyping" :- [
     note #""A ⇾ B" for (0 _ : A) → B"#,
     testEq "A ⊸ B ≡ A ⊸ B" $
       let tm = Arr One (FT "A") (FT "B") in
-      equalT tm tm,
+      equalT [<] (TYPE 0) tm tm,
     testNeq "A ⇾ B ≢ A ⊸ B" $
       let tm1 = Arr Zero (FT "A") (FT "B")
           tm2 = Arr One  (FT "A") (FT "B") in
-      equalT tm1 tm2,
+      equalT [<] (TYPE 0) tm1 tm2,
     testEq "0=1 ⊢ A ⇾ B ≢ A ⊸ B" $
       let tm1 = Arr Zero (FT "A") (FT "B")
           tm2 = Arr One  (FT "A") (FT "B") in
-      equalT tm1 tm2 {eqs = ZeroIsOne},
+      equalT [<] (TYPE 0) tm1 tm2 {eqs = ZeroIsOne},
     testEq "A ⊸ B <: A ⊸ B" $
       let tm = Arr One (FT "A") (FT "B") in
-      subT tm tm,
+      subT [<] (TYPE 0) tm tm,
     testNeq "A ⇾ B ≮: A ⊸ B" $
       let tm1 = Arr Zero (FT "A") (FT "B")
           tm2 = Arr One  (FT "A") (FT "B") in
-      subT tm1 tm2,
+      subT [<] (TYPE 0) tm1 tm2,
     testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $
       let tm = Arr Zero (TYPE 0) (TYPE 0) in
-      equalT tm tm,
+      equalT [<] (TYPE 1) tm tm,
     testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
       let tm = Arr Zero (TYPE 0) (TYPE 0) in
-      subT tm tm,
+      subT [<] (TYPE 1) tm tm,
     testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $
       let tm1 = Arr Zero (TYPE 1) (TYPE 0)
           tm2 = Arr Zero (TYPE 0) (TYPE 0) in
-      equalT tm1 tm2,
+      equalT [<] (TYPE 2) tm1 tm2,
     testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $
       let tm1 = Arr One (TYPE 1) (TYPE 0)
           tm2 = Arr One (TYPE 0) (TYPE 0) in
-      subT tm1 tm2,
+      subT [<] (TYPE 2) tm1 tm2,
     testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $
       let tm1 = Arr Zero (TYPE 0) (TYPE 0)
           tm2 = Arr Zero (TYPE 0) (TYPE 1) in
-      equalT tm1 tm2,
+      equalT [<] (TYPE 2) tm1 tm2,
     testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
       let tm1 = Arr One (TYPE 0) (TYPE 0)
           tm2 = Arr One (TYPE 0) (TYPE 1) in
-      subT tm1 tm2,
+      subT [<] (TYPE 2) tm1 tm2,
     testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
       let tm1 = Arr One (TYPE 0) (TYPE 0)
           tm2 = Arr One (TYPE 0) (TYPE 1) in
-      subT tm1 tm2
+      subT [<] (TYPE 2) tm1 tm2
   ],
 
   "lambda" :- [
     testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
-      equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
+      equalT [<] (Arr One (FT "A") (FT "A"))
+        (Lam "x" $ TUsed $ BVT 0)
+        (Lam "x" $ TUsed $ BVT 0),
     testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
-      equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
+      subT [<] (Arr One (FT "A") (FT "A"))
+        (Lam "x" $ TUsed $ BVT 0)
+        (Lam "x" $ TUsed $ BVT 0),
     testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $
-      equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0),
+      equalT [<] (Arr One (FT "A") (FT "A"))
+        (Lam "x" $ TUsed $ BVT 0)
+        (Lam "y" $ TUsed $ BVT 0),
     testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
-      equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0),
+      equalT [<] (Arr One (FT "A") (FT "A"))
+        (Lam "x" $ TUsed $ BVT 0)
+        (Lam "y" $ TUsed $ BVT 0),
     testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $
-      equalT (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1)
-             (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0),
+      equalT [<] (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
+        (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1)
+        (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0),
     testEq "λ x ⇒ [a] ≡ λ x ⇒ [a]  (TUsed vs TUnused)" $
-      equalT (Lam "x" $ TUsed   $ FT "a")
-             (Lam "x" $ TUnused $ FT "a"),
+      equalT [<] (Arr Zero (FT "B") (FT "A"))
+        (Lam "x" $ TUsed   $ FT "a")
+        (Lam "x" $ TUnused $ FT "a"),
     skipWith "(no η yet)" $
     testEq "λ x ⇒ [f [x]] ≡ [f]  (η)" $
-      equalT (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0)
-             (FT "f")
+      equalT [<] (Arr One (FT "A") (FT "A"))
+        (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0)
+        (FT "f")
   ],
 
   "eq type" :- [
     testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $
       let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
-      equalT tm tm,
+      equalT [<] (TYPE 2) tm tm,
     testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)"
         {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
-      equalT (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
-             (Eq0 (FT "A") (TYPE 0) (TYPE 0))
+      equalT [<] (TYPE 2)
+        (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
+        (Eq0 (FT "A") (TYPE 0) (TYPE 0))
   ],
 
   todo "dim lambda",
@@ -178,17 +213,25 @@ tests = "equality & subtyping" :- [
   "term closure" :- [
     note "𝑖, 𝑗 for bound variables pointing outside of the current expr",
     testEq "[𝑖]{} ≡ [𝑖]" $
-      equalT (CloT (BVT 0) id) (BVT 0) {n = 1},
+      equalT [< FT "A"] (FT "A") {n = 1}
+        (CloT (BVT 0) id)
+        (BVT 0),
     testEq "[𝑖]{a/𝑖} ≡ [a]" $
-      equalT (CloT (BVT 0) (F "a" ::: id)) (FT "a"),
+      equalT [<] (FT "A")
+        (CloT (BVT 0) (F "a" ::: id))
+        (FT "a"),
     testEq "[𝑖]{a/𝑖,b/𝑗} ≡ [a]" $
-      equalT (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"),
+      equalT [<] (FT "A")
+        (CloT (BVT 0) (F "a" ::: F "b" ::: id))
+        (FT "a"),
     testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a]  (TUnused)" $
-      equalT (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
-             (Lam "y" $ TUnused $ FT "a"),
+      equalT [<] (Arr Zero (FT "B") (FT "A"))
+        (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
+        (Lam "y" $ TUnused $ FT "a"),
     testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a]  (TUsed)" $
-      equalT (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id))
-             (Lam "y" $ TUsed $ FT "a")
+      equalT [<] (Arr Zero (FT "B") (FT "A"))
+        (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id))
+        (Lam "y" $ TUsed $ FT "a")
   ],
 
   todo "term d-closure",
@@ -202,73 +245,74 @@ tests = "equality & subtyping" :- [
          ("B", mkDef Any (TYPE (U 1)) (FT "A"))]
   in [
     testEq "A ≡ A" $
-      equalE (F "A") (F "A"),
+      equalE [<] (F "A") (F "A"),
     testNeq "A ≢ B" $
-      equalE (F "A") (F "B"),
+      equalE [<] (F "A") (F "B"),
     testEq "0=1 ⊢ A ≡ B" $
-      equalE {eqs = ZeroIsOne} (F "A") (F "B"),
+      equalE {eqs = ZeroIsOne} [<] (F "A") (F "B"),
     testEq "A : ★₁ ≔ ★₀ ⊢ A ≡ (★₀ ∷ ★₁)" {globals = au_bu} $
-      equalE (F "A") (TYPE 0 :# TYPE 1),
+      equalE [<] (F "A") (TYPE 0 :# TYPE 1),
     testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $
-      equalE (F "A") (F "B"),
+      equalE [<] (F "A") (F "B"),
     testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $
-      equalE (F "A") (F "B"),
+      equalE [<] (F "A") (F "B"),
     testEq "A <: A" $
-      subE (F "A") (F "A"),
+      subE [<] (F "A") (F "A"),
     testNeq "A ≮: B" $
-      subE (F "A") (F "B"),
+      subE [<] (F "A") (F "B"),
     testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
         {globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)),
                              ("B", mkDef Any (TYPE 3) (TYPE 2))]} $
-      subE (F "A") (F "B"),
+      subE [<] (F "A") (F "B"),
     testEq "A : ★₁👈 ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
         {globals = fromList [("A", mkDef Any (TYPE 1) (TYPE 0)),
                              ("B", mkDef Any (TYPE 3) (TYPE 2))]} $
-      subE (F "A") (F "B"),
+      subE [<] (F "A") (F "B"),
     testEq "0=1 ⊢ A <: B" $
-      subE (F "A") (F "B") {eqs = ZeroIsOne}
+      subE [<] (F "A") (F "B") {eqs = ZeroIsOne}
   ],
 
   "bound var" :- [
     note "𝑖, 𝑗 for distinct bound variables",
     testEq "𝑖 ≡ 𝑖" $
-      equalE (BV 0) (BV 0) {n = 1},
+      equalE [< TYPE 0] (BV 0) (BV 0) {n = 1},
     testNeq "𝑖 ≢ 𝑗" $
-      equalE (BV 0) (BV 1) {n = 2},
+      equalE [< TYPE 0, TYPE 0] (BV 0) (BV 1) {n = 2},
     testEq "0=1 ⊢ 𝑖 ≡ 𝑗" $
-      equalE {n = 2, eqs = ZeroIsOne} (BV 0) (BV 1)
+      equalE [< TYPE 0, TYPE 0] (BV 0) (BV 1)
+        {n = 2, eqs = ZeroIsOne}
   ],
 
   "application" :- [
     testEq "f [a] ≡ f [a]" $
-      equalE (F "f" :@ FT "a") (F "f" :@ FT "a"),
+      equalE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"),
     testEq "f [a] <: f [a]" $
-      subE (F "f" :@ FT "a") (F "f" :@ FT "a"),
+      subE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
-      equalE
+      equalE [<]
         ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
           :@ FT "a")
         (E (FT "a" :# FT "A") :# FT "A"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a  (βυ)" $
-      equalE
+      equalE [<]
         ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
           :@ FT "a")
         (F "a"),
-    testEq "(λ g ⇒ [g [x]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [x]  (β↘↙)" $
+    testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [a]  (β↘↙)" $
       let a = FT "A"; a2a = (Arr One a a) in
-      equalE
-        ((Lam "g" (TUsed (E (BV 0 :@ FT "x"))) :# Arr One a2a a) :@ FT "f")
-        ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "x"),
+      equalE [<]
+        ((Lam "g" (TUsed (E (BV 0 :@ FT "a"))) :# Arr One a2a a) :@ FT "f")
+        ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "a"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
-      subE
+      subE [<]
         ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
           :@ FT "a")
         (F "a"),
-    testEq "f : A ⊸ A ≔ λ x ⇒ [x] ⊢ f [x] ≡ x"
-           {globals = fromList
-              [("f", mkDef Any (Arr One (FT "A") (FT "A"))
+    testEq "id : A ⊸ A ≔ λ x ⇒ [x] ⊢ id [a] ≡ a"
+           {globals = defGlobals `mergeLeft` fromList
+              [("id", mkDef Any (Arr One (FT "A") (FT "A"))
                                (Lam "x" (TUsed (BVT 0))))]} $
-      equalE (F "f" :@ FT "x") (F "x")
+      equalE [<] (F "id" :@ FT "a") (F "a")
   ],
 
   "dim application" :-
@@ -277,13 +321,16 @@ tests = "equality & subtyping" :- [
   in
   [
     note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
-    testEq "refl [A] x ≡ refl [A] x" $
-      equalE (refl (FT "A") (FT "x")) (refl (FT "A") (FT "x")),
+    testEq "refl [A] a ≡ refl [A] a" $
+      equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
     testEq "p : (a ≡ b : A), q : (a ≡ b : A) ⊢ p ≡ q"
            {globals =
               let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "b") in
-              fromList [("p", def), ("q", def)]} $
-      equalE (F "p") (F "q")
+              fromList [("A", mkAbstract Zero $ TYPE 0),
+                        ("a", mkAbstract Any  $ FT "A"),
+                        ("b", mkAbstract Any  $ FT "A"),
+                        ("p", def), ("q", def)]} $
+      equalE [<] (F "p") (F "q")
   ],
 
   todo "annotation",
@@ -294,9 +341,10 @@ tests = "equality & subtyping" :- [
 
   "clashes" :- [
     testNeq "★₀ ≢ ★₀ ⇾ ★₀" $
-      equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
+      equalT [<] (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
     testEq "0=1 ⊢ ★₀ ≡ ★₀ ⇾ ★₀" $
-      equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)) {eqs = ZeroIsOne},
+      equalT [<] (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0))
+        {eqs = ZeroIsOne},
     todo "others"
   ]
 ]
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index de08dae..bb5b3a8 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -27,16 +27,16 @@ testNoStep whnf label e = test "\{label}  (no step)" $
 
 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)
+  testWhnfT = testWhnf (whnfD defs)
 
   testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
-  testWhnfE = testWhnf (whnf defs)
+  testWhnfE = testWhnf (whnfD defs)
 
   testNoStepE : String -> Elim Three d n -> Test
-  testNoStepE = testNoStep (whnf defs)
+  testNoStepE = testNoStep (whnfD defs)
 
   testNoStepT : String -> Term Three d n -> Test
-  testNoStepT = testNoStep (whnf defs)
+  testNoStepT = testNoStep (whnfD defs)
 
 
 tests = "whnf" :- [