some more properties of var

index Var.Compare by compare
i may go back on this if it's too annoying
2023-01-12 16:03:09 +01:00 · 2023-01-10 00:17:24 +01:00 · 2023-01-09 23:45:21 +01:00 · 2023-01-09 23:43:55 +01:00 · 2023-01-09 23:43:23 +01:00 · 2023-01-09 19:03:21 +01:00
29 changed files with 950 additions and 631 deletions
--- a/exe/Main.idr
+++ b/exe/Main.idr
@ -5,6 +5,7 @@ import public Quox.Syntax
 import public Quox.Equal
 import public Quox.Pretty
 import public Quox.Typechecker
+import public Quox.Syntax.Qty.Three

 import Data.Nat
 import Data.Vect
@ -53,7 +54,7 @@ banner : PrettyOpts -> String
 banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)

 export
-tm : Term 1 2
+tm : Term Three 1 2
 tm =
  (Pi One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
    `DCloT` (K One ::: id))
--- a/flake.lock
+++ b/flake.lock
@ -130,11 +130,11 @@
    },
    "flake-utils": {
      "locked": {
-        "lastModified": 1667077288,
-        "narHash": "sha256-bdC8sFNDpT0HK74u9fUkpbf1MEzVYJ+ka7NXCdgBoaA=",
+        "lastModified": 1667395993,
+        "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=",
        "owner": "numtide",
        "repo": "flake-utils",
-        "rev": "6ee9ebb6b1ee695d2cacc4faa053a7b9baa76817",
+        "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f",
        "type": "github"
      },
      "original": {
@ -392,11 +392,11 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1667055375,
-        "narHash": "sha256-xfSTHYxuKRiqF4dcuAFdti1OUvrC2lHpQqCHWUK5/JA=",
+        "lastModified": 1672997035,
+        "narHash": "sha256-DNaNjsGMRYefBTAxFIrVOB2ok477cj1FTpqnu/mKRf4=",
        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "7f9be6a505a31f88499c5d20d11f98accf5ae6ba",
+        "rev": "f1ffcf798e93b169321106a4aef79526a2b4bd0a",
        "type": "github"
      },
      "original": {
--- a/lib/Quox/Decidable.idr
+++ b/lib/Quox/Decidable.idr
@ -0,0 +1,53 @@
+module Quox.Decidable
+
+import public Data.Bool.Decidable
+import public Decidable.Decidable
+import public Decidable.Equality
+import public Control.Relation
+
+
+public export
+0 REL : Type -> Type -> Type
+REL a b = a -> b -> Type
+
+
+public export
+0 Pred : Type -> Type
+Pred a = a -> Type
+
+
+public export
+0 Dec1 : Pred a -> Type
+Dec1 p = (x : a) -> Dec (p x)
+
+public export
+0 Dec2 : REL a b -> Type
+Dec2 p = (x : a) -> (y : b) -> Dec (p x y)
+
+
+public export
+0 Reflects1 : Pred a -> (a -> Bool) -> Type
+p `Reflects1` f = (x : a) -> p x `Reflects` f x
+
+public export
+0 Reflects2 : REL a b -> (a -> b -> Bool) -> Type
+p `Reflects2` f = (x : a) -> (y : b) -> p x y `Reflects` f x y
+
+
+public export
+(||) : Dec p -> Dec q -> Dec (Either p q)
+Yes y1 || _      = Yes $ Left y1
+No  _  || Yes y2 = Yes $ Right y2
+No  n1 || No  n2 = No  $ \case Left y1 => n1 y1; Right y2 => n2 y2
+
+public export
+(&&) : Dec p -> Dec q -> Dec (p, q)
+Yes y1 && Yes y2 = Yes (y1, y2)
+Yes _  && No  n2 = No $ n2 . snd
+No  n1 && _      = No $ n1 . fst
+
+
+public export
+reflectToDec : p `Reflects` b -> Dec p
+reflectToDec (RTrue  y) = Yes y
+reflectToDec (RFalse n) = No  n
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@ -2,51 +2,66 @@ module Quox.Definition

 import public Quox.Syntax
 import public Data.SortedMap
-import public Control.Monad.State
+import public Control.Monad.Reader
+import Decidable.Decidable


 public export
-record AnyTerm where
+record AnyTerm q where
  constructor T
-  def : forall d, n. Term d n
+  get : forall d, n. Term q d n

 public export
-record Definition where
+record Definition' q (isGlobal : q -> Type) where
  constructor MkDef'
-  qty         : Qty
-  0 qtyGlobal : IsGlobal qty
-  type        : AnyTerm
-  term        : Maybe AnyTerm
+  qty  : q
+  type : AnyTerm q
+  term : Maybe $ AnyTerm q
+  {auto 0 qtyGlobal : isGlobal qty}
+
+public export
+0 Definition : (q : Type) -> IsQty q => Type
+Definition q = Definition' q IsGlobal

 public export %inline
-MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
-           (type, term : forall d, n. Term d n) -> Definition
-MkDef {qty, type, term} =
-  MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
+mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
+        (type, term : forall d, n. Term q d n) -> Definition q
+mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}

 public export %inline
-MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
-             (type : forall d, n. Term d n) -> Definition
-MkAbstract {qty, type} =
-  MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
+mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
+             (type : forall d, n. Term q d n) -> Definition q
+mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}


 public export %inline
-(.type0) : Definition -> Term 0 0
-g.type0 = g.type.def
+(.type0) : Definition' q _ -> Term q 0 0
+g.type0 = g.type.get

 public export %inline
-(.term0) : Definition -> Maybe (Term 0 0)
-g.term0 = map (\t => t.def) g.term
+(.term0) : Definition' q _ -> Maybe (Term q 0 0)
+g.term0 = map (\t => t.get) g.term

 public export %inline
-(.qtyP) : Definition -> Subset Qty IsGlobal
+(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
 g.qtyP = Element g.qty g.qtyGlobal

 public export %inline
-isZero : Definition -> Bool
-isZero g = g.qty == Zero
+isZero : IsQty q => Definition q -> Bool
+isZero g = isYes $ isZero g.qty

 public export
-Definitions : Type
-Definitions = SortedMap Name Definition
+0 Definitions' : (q : Type) -> (q -> Type) -> Type
+Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
+
+public export
+0 Definitions : (q : Type) -> IsQty q => Type
+Definitions q = Definitions' q IsGlobal
+
+
+public export
+0 HasDefs' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal)
+
+0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type
+HasDefs q = HasDefs' q IsGlobal
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@ -9,178 +9,228 @@ import Data.Maybe


 private %inline
-ClashE : EqMode -> Elim d n -> Elim d n -> Error
+ClashE : EqMode -> Elim q d n -> Elim q d n -> Error q
 ClashE mode = ClashT mode `on` E

+
 public export
-CanEq : (Type -> Type) -> Type
-CanEq m = (MonadError Error m, MonadReader Definitions m)
+record Env' q (isGlobal : q -> Type) where
+  constructor MakeEnv
+  defs : Definitions' q isGlobal
+  mode : EqMode
+
+public export
+0 Env : (q : Type) -> IsQty q => Type
+Env q = Env' q IsGlobal
+
+public export
+0 HasEnv' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+HasEnv' q isGlobal = MonadReader (Env' q isGlobal)
+
+public export
+0 HasEnv : (q : Type) -> IsQty q => (Type -> Type) -> Type
+HasEnv q = HasEnv' q IsGlobal


-parameters {auto _ : CanEq m}
-  private %inline
-  clashT : EqMode -> Term d n -> Term d n -> m a
-  clashT mode = throwError .: ClashT mode
+public export
+0 CanEqual' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+CanEqual' q isGlobal m = (HasErr q m, HasEnv' q isGlobal m)

-  private %inline
-  clashE : EqMode -> Elim d n -> Elim d n -> m a
-  clashE mode = throwError .: ClashE mode
-
-  private %inline
-  defE : Name -> m (Maybe (Elim d n))
-  defE x = asks $ \defs => do
-    g <- lookup x defs
-    pure $ (!g.term).def :# g.type.def
-
-  private %inline
-  defT : Name -> m (Maybe (Term d n))
-  defT x = map E <$> defE x
-
-  export %inline
-  compareU' : EqMode -> Universe -> Universe -> Bool
-  compareU' = \case Equal => (==); Sub => (<=)
-
-  export %inline
-  compareU : EqMode -> Universe -> Universe -> m ()
-  compareU mode k l = unless (compareU' mode k l) $
-    throwError $ ClashU mode k l
-
-  mutual
-    private covering
-    compareTN' : EqMode ->
-                 (s, t : Term 0 n) ->
-                 (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
-
-    compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
-    -- if either term is a def, try to unfold it
-    compareTN' mode s@(E (F x)) t ps pt = do
-      Just s' <- defT x  | Nothing => clashT mode s t
-      compareT0 mode s' t
-    compareTN' mode s t@(E (F y)) ps pt = do
-      Just t' <- defT y  | Nothing => clashT mode s t
-      compareT0 mode s t'
-    compareTN' mode s@(E _) t _ _ = clashT mode s t
-
-    compareTN' mode (TYPE k) (TYPE l) _ _ = compareU mode k l
-    compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
-
-    compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
-      unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
-      compareT0  mode arg2 arg1 -- reversed for contravariant domain
-      compareTS0 mode res1 res2
-    compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
-
-    -- [todo] eta
-    compareTN' _ (Lam _ body1) (Lam _ body2) _ _ =
-      compareTS0 Equal body1 body2
-    compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
-
-    compareTN' _ (CloT  {}) _ ps _ = void $ ps IsCloT
-    compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
-
-    private covering
-    compareEN' : EqMode ->
-                 (e, f : Elim 0 n) ->
-                 (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
-
-    compareEN' mode e@(F x) f@(F y) _ _ =
-      if x == y then pure () else
-      case (!(defE x), !(defE y)) of
-           (Nothing, Nothing) => clashE mode e f
-           (s', t') => compareE0 mode (fromMaybe e s') (fromMaybe f t')
-    compareEN' mode e@(F x) f _ _ = do
-      Just e' <- defE x  | Nothing => clashE mode e f
-      compareE0 mode e' f
-    compareEN' mode e f@(F y) _ _ = do
-      Just f' <- defE y  | Nothing => clashE mode e f
-      compareE0 mode e f'
-
-    compareEN' mode e@(B i) f@(B j) _ _ =
-      unless (i == j) $ clashE mode e f
-    compareEN' mode e@(B _) f _ _ = clashE mode e f
-
-    -- [todo] tracking variance of functions? maybe???
-    -- probably not
-    compareEN' _ (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
-      compareE0 Equal fun1 fun2
-      compareT0 Equal arg1 arg2
-    compareEN' mode e@(_ :@ _) f _ _ = clashE mode e f
-
-    -- [todo] is always checking the types are equal correct?
-    compareEN' mode (tm1 :# ty1) (tm2 :# ty2) _ _ = do
-      compareT0 mode tm1 tm2
-      compareT0 Equal ty1 ty2
-    compareEN' mode e@(_ :# _) f _ _ = clashE mode e f
-
-    compareEN' _ (CloE  {}) _ pe _ = void $ pe IsCloE
-    compareEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
+public export
+0 CanEqual : (q : Type) -> IsQty q => (Type -> Type) -> Type
+CanEqual q = CanEqual' q IsGlobal


-    private covering %inline
-    compareTN : EqMode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
-    compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd

-    private covering %inline
-    compareEN : EqMode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
-    compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
+private %inline
+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
+
+private %inline
+clashE : CanEqual' q _ m => Elim q d n -> Elim q d n -> m a
+clashE e f = throwError $ ClashE !mode e f
+
+private %inline
+defE : HasEnv' q _ m => Name -> m (Maybe (Elim q d n))
+defE x = asks $ \env => do
+  g <- lookup x env.defs
+  pure $ (!g.term).get :# g.type.get
+
+private %inline
+defT : HasEnv' q _ m => Name -> m (Maybe (Term q d n))
+defT x = map E <$> defE x
+
+export %inline
+compareU' : HasEnv' q _ m => Universe -> Universe -> m Bool
+compareU' i j = pure $
+  case !mode of Equal => i == j; Sub => i <= j
+
+export %inline
+compareU : CanEqual' q _ m => Universe -> Universe -> m ()
+compareU k l = unless !(compareU' k l) $
+  throwError $ ClashU !mode k l
+
+mutual
+  private covering
+  compareTN' : CanEqual' q _ m => Eq q =>
+               (s, t : Term q 0 n) ->
+               (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
+
+  compareTN' (E e) (E f) ps pt = compareE0 e f
+  -- if either term is a def, try to unfold it
+  compareTN' s@(E (F x)) t ps pt = do
+    Just s' <- defT x  | Nothing => clashT s t
+    compareT0 s' t
+  compareTN' s t@(E (F y)) ps pt = do
+    Just t' <- defT y  | Nothing => clashT s t
+    compareT0 s t'
+  compareTN' s@(E _) t _ _ = clashT s t
+
+  compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
+  compareTN' s@(TYPE _) t _ _ = clashT s t
+
+  compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
+    unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
+    compareT0  arg2 arg1 -- reversed for contravariant domain
+    compareTS0 res1 res2
+  compareTN' s@(Pi {}) t _ _ = clashT s t
+
+  -- [todo] eta
+  compareTN' (Lam _ body1) (Lam _ body2) _ _ =
+    local {mode := Equal} $ compareTS0 body1 body2
+  compareTN' s@(Lam {}) t _ _ = clashT s t
+
+  compareTN' (CloT  {}) _ ps _ = void $ ps IsCloT
+  compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
+
+  private covering
+  compareEN' : CanEqual' q _ m => Eq q =>
+               (e, f : Elim q 0 n) ->
+               (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
+
+  compareEN' e@(F x) f@(F y) _ _ =
+    if x == y then pure () else
+    case (!(defE x), !(defE y)) of
+         (Nothing, Nothing) => clashE e f
+         (s', t') => compareE0 (fromMaybe e s') (fromMaybe f t')
+  compareEN' e@(F x) f _ _ = do
+    Just e' <- defE x  | Nothing => clashE e f
+    compareE0 e' f
+  compareEN' e f@(F y) _ _ = do
+    Just f' <- defE y  | Nothing => clashE e f
+    compareE0 e f'
+
+  compareEN' e@(B i) f@(B j) _ _ =
+    unless (i == j) $ clashE e f
+  compareEN' e@(B _) f _ _ = clashE e f
+
+  -- [todo] tracking variance of functions? maybe???
+  -- probably not
+  compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
+    local {mode := Equal} $ do
+      compareE0 fun1 fun2
+      compareT0 arg1 arg2
+  compareEN' e@(_ :@ _) f _ _ = clashE e f
+
+  -- [todo] is always checking the types are equal correct?
+  compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
+    compareT0 tm1 tm2
+    local {mode := Equal} $ compareT0 ty1 ty2
+  compareEN' e@(_ :# _) f _ _ = clashE e f
+
+  compareEN' (CloE  {}) _ pe _ = void $ pe IsCloE
+  compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE


-    export covering %inline
-    compareT : EqMode -> DimEq d -> Term d n -> Term d n -> m ()
-    compareT mode eqs s t =
-      for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
+  private covering %inline
+  compareTN : CanEqual' q _ m => Eq q =>
+              NonRedexTerm q 0 n -> NonRedexTerm q 0 n -> m ()
+  compareTN s t = compareTN' s.fst t.fst s.snd t.snd

-    export covering %inline
-    compareE : EqMode -> DimEq d -> Elim d n -> Elim d n -> m ()
-    compareE mode eqs e f =
-      for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
+  private covering %inline
+  compareEN : CanEqual' q _ m => Eq q =>
+              NonRedexElim q 0 n -> NonRedexElim q 0 n -> m ()
+  compareEN e f = compareEN' e.fst f.fst e.snd f.snd


-    export covering %inline
-    compareT0 : EqMode -> Term 0 n -> Term 0 n -> m ()
-    compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
+  export covering %inline
+  compareT : CanEqual' q _ m => Eq q =>
+             DimEq d -> Term q d n -> Term q d n -> m ()
+  compareT eqs s t =
+    for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th)

-    export covering %inline
-    compareE0 : EqMode -> Elim 0 n -> Elim 0 n -> m ()
-    compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
-
-    export covering %inline
-    compareTS0 : EqMode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
-    compareTS0 mode (TUnused body1) (TUnused body2) =
-      compareT0 mode body1 body2
-    compareTS0 mode body1 body2 =
-      compareT0 mode (fromScopeTerm body1) (fromScopeTerm body2)
+  export covering %inline
+  compareE : CanEqual' q _ m => Eq q =>
+             DimEq d -> Elim q d n -> Elim q d n -> m ()
+  compareE eqs e f =
+    for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)


-    export covering %inline
-    equalTWith : DimEq d -> Term d n -> Term d n -> m ()
-    equalTWith = compareT Equal
+  export covering %inline
+  compareT0 : CanEqual' q _ m => Eq q => Term q 0 n -> Term q 0 n -> m ()
+  compareT0 s t = compareTN (whnfT s) (whnfT t)

-    export covering %inline
-    equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
-    equalEWith = compareE Equal
+  export covering %inline
+  compareE0 : CanEqual' q _ m => Eq q => Elim q 0 n -> Elim q 0 n -> m ()
+  compareE0 e f = compareEN (whnfE e) (whnfE f)

-    export covering %inline
-    subTWith : DimEq d -> Term d n -> Term d n -> m ()
-    subTWith = compareT Sub
-
-    export covering %inline
-    subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
-    subEWith = compareE Sub
+  export covering %inline
+  compareTS0 : CanEqual' q _ m => Eq q =>
+               ScopeTerm q 0 n -> ScopeTerm q 0 n -> m ()
+  compareTS0 (TUnused body1) (TUnused body2) =
+    compareT0 body1 body2
+  compareTS0 body1 body2 =
+    compareT0 (fromScopeTerm body1) (fromScopeTerm body2)


-    export covering %inline
-    equalT : {d : Nat} -> Term d n -> Term d n -> m ()
-    equalT = equalTWith DimEq.new
+private %inline
+into : HasErr q m => HasDefs' q isg m => Eq q =>
+       (forall n. HasErr q n => HasEnv' q isg n => d -> a -> a -> n ()) ->
+       EqMode -> d -> a -> a -> m ()
+into f mode eqs a b =
+  runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b

-    export covering %inline
-    equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
-    equalE = equalEWith DimEq.new
+export covering %inline
+equalTWith : HasErr q m => HasDefs' q _ m => Eq q =>
+             DimEq d -> Term q d n -> Term q d n -> m ()
+equalTWith = into compareT Equal

-    export covering %inline
-    subT : {d : Nat} -> Term d n -> Term d n -> m ()
-    subT = subTWith DimEq.new
+export covering %inline
+equalEWith : HasErr q m => HasDefs' q _ m => Eq q =>
+             DimEq d -> Elim q d n -> Elim q d n -> m ()
+equalEWith = into compareE Equal

-    export covering %inline
-    subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
-    subE = subEWith DimEq.new
+export covering %inline
+subTWith : HasErr q m => HasDefs' q _ m => Eq q =>
+           DimEq d -> Term q d n -> Term q d n -> m ()
+subTWith = into compareT Sub
+
+export covering %inline
+subEWith : HasErr q m => HasDefs' q _ m => Eq q =>
+           DimEq d -> Elim q d n -> Elim q d n -> m ()
+subEWith = into compareE Sub
+
+
+export covering %inline
+equalT : HasErr q m => HasDefs' q _ m => Eq q =>
+         {d : Nat} -> Term q d n -> Term q d n -> m ()
+equalT = equalTWith DimEq.new
+
+export covering %inline
+equalE : HasErr q m => HasDefs' q _ m => Eq q =>
+         {d : Nat} -> Elim q d n -> Elim q d n -> m ()
+equalE = equalEWith DimEq.new
+
+export covering %inline
+subT : HasErr q m => HasDefs' q _ m => Eq q =>
+       {d : Nat} -> Term q d n -> Term q d n -> m ()
+subT = subTWith DimEq.new
+
+export covering %inline
+subE : HasErr q m => HasDefs' q _ m => Eq q =>
+       {d : Nat} -> Elim q d n -> Elim q d n -> m ()
+subE = subEWith DimEq.new
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@ -104,10 +104,10 @@ mutual

  export %inline
  setVar : (i, j : Var d) -> DimEq' d -> DimEq d
-  setVar i j eqs with (compareP i j)
-    _              | IsLT lt = setVar' i j lt eqs
-    setVar i i eqs | IsEQ    = C eqs
-    _              | IsGT gt = setVar' j i gt eqs
+  setVar i j eqs with (compareP i j) | (compare i.nat j.nat)
+    setVar i j eqs | IsLT lt | LT = setVar' i j lt eqs
+    setVar i i eqs | IsEQ    | EQ = C eqs
+    setVar i j eqs | IsGT gt | GT = setVar' j i gt eqs


 export %inline
@ -166,7 +166,10 @@ export
 setSelf p ZeroIsOne = Refl
 setSelf (K Zero) (C eqs) = Refl
 setSelf (K One)  (C eqs) = Refl
-setSelf (B i)    (C eqs) = rewrite comparePSelf i in Refl
+setSelf (B i)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
+  _ | IsLT lt | LT = absurd lt
+  _ | IsEQ    | EQ = Refl
+  _ | IsGT gt | GT = absurd gt


 -- [todo] "well formed" dimeqs
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@ -1,84 +1,72 @@
 module Quox.Syntax.Qty

 import Quox.Pretty
-
-import Data.Fin
-import Generics.Derive
+import public Quox.Decidable
+import Data.DPair

 %default total
-%language ElabReflection


-public export
-data Qty = Zero | One | Any
-%name Qty.Qty pi, rh
-
-%runElab derive "Qty" [Generic, Meta, Eq, Ord, DecEq, Show]
-
-
-export
-PrettyHL Qty where
-  prettyM pi = hl Qty <$>
-    case pi of
-      Zero => ifUnicode "𝟬" "0"
-      One  => ifUnicode "𝟭" "1"
-      Any  => ifUnicode "𝛚" "*"
-
 private
 commas : List (Doc HL) -> List (Doc HL)
-commas [] = []
-commas [x] = [x]
+commas []      = []
+commas [x]     = [x]
 commas (x::xs) = (x <+> hl Delim ",") :: commas xs

 export %inline
-prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
+prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => List q -> m (Doc HL)
 prettyQtyBinds =
  map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M


 public export
-plus : Qty -> Qty -> Qty
-plus Zero rh   = rh
-plus pi   Zero = pi
-plus _    _    = Any
-
-public export
-times : Qty -> Qty -> Qty
-times Zero _    = Zero
-times _    Zero = Zero
-times One  rh   = rh
-times pi   One  = pi
-times Any  Any  = Any
-
-infix 6 <=.
-public export
-compat : Qty -> Qty -> Bool
-compat pi rh = rh == Any || pi == rh
-
-
-public export
-interface IsQty q where
+interface Eq q => IsQty q where
  zero, one : q
  (+),  (*) : q -> q -> q
-  (<=.)     : q -> q -> Bool
+
+  ||| true if bindings of this quantity will be erased
+  ||| and must not be runtime relevant
+  IsZero : Pred q
+  isZero : Dec1 IsZero
+  zeroIsZero : IsZero zero
+
+  ||| ``p `Compat` q`` if it is ok for a binding of
+  ||| quantity `q` to be used exactly `p` times.
+  ||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
+  Compat : Rel q
+  compat : Dec2 Compat
+
+  ||| true if it is ok for this quantity to appear for the
+  ||| subject of a typing judgement. this is about the
+  ||| subject reduction stuff in atkey
+  IsSubj : Pred q
+  isSubj : Dec1 IsSubj
+  zeroIsSubj : IsSubj zero
+  oneIsSubj  : IsSubj one
+  timesSubj  : forall pi, rh. IsSubj pi -> IsSubj rh -> IsSubj (pi * rh)
+
+  ||| true if it is ok for a global definition to have this
+  ||| quantity. so not exact usage counts, maybe.
+  IsGlobal : Pred q
+  isGlobal : Dec1 IsGlobal
+  zeroIsGlobal : IsGlobal zero

 public export
-IsQty Qty where
-  zero  = Zero; one = One
-  (+)   = plus; (*) = times
-  (<=.) = compat
+0 SQty : (q : Type) -> IsQty q => Type
+SQty q = Subset q IsSubj

+public export %inline
+szero : IsQty q => SQty q
+szero = Element zero zeroIsSubj
+
+public export %inline
+sone : IsQty q => SQty q
+sone = Element one oneIsSubj

 public export
-data IsSubj : Qty -> Type where
-  SZero : IsSubj Zero
-  SOne  : IsSubj One
+0 GQty : (q : Type) -> IsQty q => Type
+GQty q = Subset q IsGlobal

-export Uninhabited (IsSubj Any) where uninhabited _ impossible
-
-public export
-data IsGlobal : Qty -> Type where
-  GZero : IsGlobal Zero
-  GAny  : IsGlobal Any
-
-export Uninhabited (IsGlobal One) where uninhabited _ impossible
+public export %inline
+gzero : IsQty q => GQty q
+gzero = Element zero zeroIsGlobal
--- a/lib/Quox/Syntax/Qty/Three.idr
+++ b/lib/Quox/Syntax/Qty/Three.idr
@ -0,0 +1,113 @@
+module Quox.Syntax.Qty.Three
+
+import Quox.Pretty
+import public Quox.Syntax.Qty
+import Generics.Derive
+
+%default total
+%language ElabReflection
+
+
+public export
+data Three = Zero | One | Any
+%name Three pi, rh
+
+%runElab derive "Three" [Generic, Meta, Eq, Ord, DecEq, Show]
+
+
+export
+PrettyHL Three where
+  prettyM pi = hl Qty <$>
+    case pi of
+      Zero => ifUnicode "𝟬" "0"
+      One  => ifUnicode "𝟭" "1"
+      Any  => ifUnicode "𝛚" "*"
+
+
+public export
+plus : Three -> Three -> Three
+plus Zero rh   = rh
+plus pi   Zero = pi
+plus _    _    = Any
+
+public export
+times : Three -> Three -> Three
+times Zero _    = Zero
+times _    Zero = Zero
+times One  rh   = rh
+times pi   One  = pi
+times Any  Any  = Any
+
+public export
+data Compat3 : Rel Three where
+  CmpRefl : Compat3 rh rh
+  CmpAny  : Compat3 rh Any
+
+public export
+compat3 : Dec2 Compat3
+compat3 pi rh with (decEq pi rh) | (decEq rh Any)
+  compat3 pi pi  | Yes Refl | _        = Yes CmpRefl
+  compat3 pi Any | No  _    | Yes Refl = Yes CmpAny
+  compat3 pi rh  | No  ne   | No  na   =
+    No $ \case CmpRefl => ne Refl; CmpAny => na Refl
+
+
+public export
+data IsSubj3 : Pred Three where
+  SZero : IsSubj3 Zero
+  SOne  : IsSubj3 One
+
+public export
+isSubj3 : Dec1 IsSubj3
+isSubj3 Zero = Yes SZero
+isSubj3 One  = Yes SOne
+isSubj3 Any  = No $ \case _ impossible
+
+public export
+timesSubj3 : forall pi, rh. IsSubj3 pi -> IsSubj3 rh -> IsSubj3 (times pi rh)
+timesSubj3 SZero SZero = SZero
+timesSubj3 SZero SOne  = SZero
+timesSubj3 SOne  SZero = SZero
+timesSubj3 SOne  SOne  = SOne
+
+
+public export
+data IsGlobal3 : Pred Three where
+  GZero : IsGlobal3 Zero
+  GAny  : IsGlobal3 Any
+
+isGlobal3 : Dec1 IsGlobal3
+isGlobal3 Zero = Yes GZero
+isGlobal3 One  = No $ \case _ impossible
+isGlobal3 Any  = Yes GAny
+
+
+public export
+IsQty Three where
+  zero = Zero
+  one  = One
+
+  (+) = plus
+  (*) = times
+
+  IsZero     = Equal Zero
+  isZero     = decEq Zero
+  zeroIsZero = Refl
+
+  Compat = Compat3
+  compat = compat3
+
+  IsSubj     = IsSubj3
+  isSubj     = isSubj3
+  zeroIsSubj = SZero
+  oneIsSubj  = SOne
+  timesSubj  = timesSubj3
+
+  IsGlobal     = IsGlobal3
+  isGlobal     = isGlobal3
+  zeroIsGlobal = GZero
+
+
+export Uninhabited (IsGlobal3 One) where uninhabited _ impossible
+
+export Uninhabited (IsSubj3 Any) where uninhabited _ impossible
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@ -7,7 +7,7 @@ import public Quox.Syntax.Universe
 import public Quox.Syntax.Qty
 import public Quox.Syntax.Dim
 import public Quox.Name
-import public Quox.OPE
+-- import public Quox.OPE

 import Quox.Pretty

@ -26,63 +26,67 @@ infixl 8 :#
 infixl 9 :@
 mutual
  public export
-  TSubst : Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (\n => Elim d n)
+  TSubst : Type -> Nat -> Nat -> Nat -> Type
+  TSubst q d = Subst (\n => Elim q d n)

  ||| first argument `d` is dimension scope size, second `n` is term scope size
  public export
-  data Term : (d, n : Nat) -> Type where
+  data Term : (q : Type) -> (d, n : Nat) -> Type where
    ||| type of types
-    TYPE : (l : Universe) -> Term d n
+    TYPE : (l : Universe) -> Term q d n

    ||| function type
-    Pi  : (qty : Qty) -> (x : Name) ->
-          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
+    Pi  : (qty : q) -> (x : Name) ->
+          (arg : Term q d n) -> (res : ScopeTerm q d n) -> Term q d n
    ||| function term
-    Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
+    Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n

    ||| elimination
-    E : (e : Elim d n) -> Term d n
+    E : (e : Elim q d n) -> Term q d n

    ||| term closure/suspended substitution
-    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    CloT  : (tm : Term q d from) -> (th : Lazy (TSubst q d from to)) ->
+            Term q d to
    ||| dimension closure/suspended substitution
-    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+    DCloT : (tm : Term q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
+            Term q dto n

  ||| first argument `d` is dimension scope size, second `n` is term scope size
  public export
-  data Elim : (d, n : Nat) -> Type where
+  data Elim : (q : Type) -> (d, n : Nat) -> Type where
    ||| free variable
-    F : (x : Name) -> Elim d n
+    F : (x : Name) -> Elim q d n
    ||| bound variable
-    B : (i : Var n) -> Elim d n
+    B : (i : Var n) -> Elim q d n

    ||| term application
-    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
+    (:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n

    ||| type-annotated term
-    (:#) : (tm, ty : Term d n) -> Elim d n
+    (:#) : (tm, ty : Term q d n) -> Elim q d n

    ||| term closure/suspended substitution
-    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    CloE  : (el : Elim q d from) -> (th : Lazy (TSubst q d from to)) ->
+            Elim q d to
    ||| dimension closure/suspended substitution
-    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+    DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
+            Elim q dto n

  ||| a scope with one more bound variable
  public export
-  data ScopeTerm : (d, n : Nat) -> Type where
+  data ScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
    ||| variable is used
-    TUsed : (body : Term d (S n)) -> ScopeTerm d n
+    TUsed : (body : Term q d (S n)) -> ScopeTerm q d n
    ||| variable is unused
-    TUnused : (body : Term d n) -> ScopeTerm d n
+    TUnused : (body : Term q d n) -> ScopeTerm q d n

  ||| a scope with one more bound dimension variable
  public export
-  data DScopeTerm : (d, n : Nat) -> Type where
+  data DScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
    ||| variable is used
-    DUsed : (body : Term (S d) n) -> DScopeTerm d n
+    DUsed : (body : Term q (S d) n) -> DScopeTerm q d n
    ||| variable is unused
-    DUnused : (body : Term d n) -> DScopeTerm d n
+    DUnused : (body : Term q d n) -> DScopeTerm q d n

 %name Term s, t, r
 %name Elim e, f
@ -90,21 +94,21 @@ mutual
 %name DScopeTerm body

 public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
+Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
 Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}

 ||| same as `F` but as a term
 public export %inline
-FT : Name -> Term d n
+FT : Name -> Term q d n
 FT = E . F

 ||| abbreviation for a bound variable like `BV 4` instead of
 ||| `B (VS (VS (VS (VS VZ))))`
 public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
+BV : (i : Nat) -> (0 _ : LT i n) => Elim q d n
 BV i = B $ V i

 ||| same as `BV` but as a term
 public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
+BVT : (i : Nat) -> (0 _ : LT i n) => Term q d n
 BVT i = E $ BV i
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@ -28,7 +28,7 @@ colonD = hl Syntax ":"

 mutual
  export covering
-  PrettyHL (Term d n) where
+  PrettyHL q => PrettyHL (Term q d n) where
    prettyM (TYPE l) =
      parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
    prettyM (Pi qty x s t) =
@ -49,7 +49,7 @@ mutual
        [|withPrec SApp (prettyM s) </> prettyDSubst th|]

  export covering
-  PrettyHL (Elim d n) where
+  PrettyHL q => PrettyHL (Elim q d n) where
    prettyM (F x) =
      hl' Free <$> prettyM x
    prettyM (B i) =
@ -70,15 +70,17 @@ mutual
        [|withPrec SApp (prettyM e) </> prettyDSubst th|]

  export covering
-  PrettyHL (ScopeTerm d n) where
+  PrettyHL q => PrettyHL (ScopeTerm q d n) where
    prettyM body = prettyM $ fromScopeTerm body

  export covering
-  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
+  prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
+                 TSubst q d from to -> m (Doc HL)
  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s

  export covering
-  prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
+  prettyBinder : Pretty.HasEnv m => PrettyHL q =>
+                 List q -> Name -> Term q d n -> m (Doc HL)
  prettyBinder pis x a =
    pure $ parens $ hang 2 $
      hsep [hl TVar !(prettyM x),
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@ -7,43 +7,57 @@ import Quox.Syntax.Term.Subst


 mutual
-  ||| true if a term has a closure or dimension closure at the top level,
-  ||| or is `E` applied to such an elimination
-  public export %inline
-  topCloT : Term d n -> Bool
-  topCloT (CloT  _ _) = True
-  topCloT (DCloT _ _) = True
-  topCloT (E e)       = topCloE e
-  topCloT _           = False
+  public export
+  data NotCloT : Term {} -> Type where
+    NCTYPE : NotCloT $ TYPE _
+    NCPi   : NotCloT $ Pi {}
+    NCLam  : NotCloT $ Lam {}
+    NCE    : NotCloE e -> NotCloT $ E e

-  ||| true if an elimination has a closure or dimension closure at the top level
-  public export %inline
-  topCloE : Elim d n -> Bool
-  topCloE (CloE  _ _) = True
-  topCloE (DCloE _ _) = True
-  topCloE _           = False
+  public export
+  data NotCloE : Elim {} -> Type where
+    NCF   : NotCloE $ F _
+    NCB   : NotCloE $ B _
+    NCApp : NotCloE $ _ :@ _
+    NCAnn : NotCloE $ _ :# _

+mutual
+  export
+  notCloT : (t : Term {}) -> Dec (NotCloT t)
+  notCloT (TYPE _) = Yes NCTYPE
+  notCloT (Pi {})  = Yes NCPi
+  notCloT (Lam {}) = Yes NCLam
+  notCloT (E e) with (notCloE e)
+    notCloT (E e) | Yes nc = Yes $ NCE nc
+    notCloT (E e) | No  c  = No  $ \case NCE nc => c nc
+  notCloT (CloT {})  = No $ \case _ impossible
+  notCloT (DCloT {}) = No $ \case _ impossible

-public export IsNotCloT : Term d n -> Type
-IsNotCloT = So . not . topCloT
+  export
+  notCloE : (e : Elim {}) -> Dec (NotCloE e)
+  notCloE (F _)      = Yes NCF
+  notCloE (B _)      = Yes NCB
+  notCloE (_ :@ _)   = Yes NCApp
+  notCloE (_ :# _)   = Yes NCAnn
+  notCloE (CloE  {}) = No $ \case _ impossible
+  notCloE (DCloE {}) = No $ \case _ impossible

 ||| a term which is not a top level closure
-public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) IsNotCloT
-
-public export IsNotCloE : Elim d n -> Type
-IsNotCloE = So . not . topCloE
+public export
+NotCloTerm : Type -> Nat -> Nat -> Type
+NotCloTerm q d n = Subset (Term q d n) NotCloT

 ||| an elimination which is not a top level closure
-public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) IsNotCloE
+public export
+NotCloElim : Type -> Nat -> Nat -> Type
+NotCloElim q d n = Subset (Elim q d n) NotCloE

 public export %inline
-ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
+ncloT : (t : Term q d n) -> (0 _ : NotCloT t) => NotCloTerm q d n
 ncloT t @{p} = Element t p

 public export %inline
-ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
+ncloE : (e : Elim q d n) -> (0 _ : NotCloE e) => NotCloElim q d n
 ncloE e @{p} = Element e p


@ -52,18 +66,18 @@ mutual
  ||| if the input term has any top-level closures, push them under one layer of
  ||| syntax
  export %inline
-  pushSubstsT : Term d n -> NotCloTerm d n
+  pushSubstsT : Term q d n -> NotCloTerm q d n
  pushSubstsT s = pushSubstsTWith id id s

  ||| if the input elimination has any top-level closures, push them under one
  ||| layer of syntax
  export %inline
-  pushSubstsE : Elim d n -> NotCloElim d n
+  pushSubstsE : Elim q d n -> NotCloElim q d n
  pushSubstsE e = pushSubstsEWith id id e

  export
-  pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Term dfrom from -> NotCloTerm dto to
+  pushSubstsTWith : DSubst dfrom dto -> TSubst q dto from to ->
+                    Term q dfrom from -> NotCloTerm q dto to
  pushSubstsTWith th ph (TYPE l) =
    ncloT $ TYPE l
  pushSubstsTWith th ph (Pi qty x a body) =
@ -78,15 +92,15 @@ mutual
    pushSubstsTWith (ps . th) ph s

  export
-  pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Elim dfrom from -> NotCloElim dto to
+  pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to ->
+                    Elim q dfrom from -> NotCloElim q dto to
  pushSubstsEWith th ph (F x) =
    ncloE $ F x
  pushSubstsEWith th ph (B i) =
    let res = ph !! i in
-    case choose $ topCloE res of
-         Left  _ => assert_total pushSubstsE res
-         Right _ => ncloE res
+    case notCloE res of
+         Yes _ => ncloE res
+         No  _ => assert_total pushSubstsE res
  pushSubstsEWith th ph (f :@ s) =
    ncloE $ subs f th ph :@ subs s th ph
  pushSubstsEWith th ph (s :# a) =
@ -97,103 +111,103 @@ mutual
    pushSubstsEWith (ps . th) ph e


-parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
+parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
  public export %inline
-  pushSubstsTWith' : Term dfrom from -> Term dto to
+  pushSubstsTWith' : Term q dfrom from -> Term q dto to
  pushSubstsTWith' s = (pushSubstsTWith th ph s).fst

  public export %inline
-  pushSubstsEWith' : Elim dfrom from -> Elim dto to
+  pushSubstsEWith' : Elim q dfrom from -> Elim q dto to
  pushSubstsEWith' e = (pushSubstsEWith th ph e).fst


 public export %inline
-pushSubstsT' : Term d n -> Term d n
+pushSubstsT' : Term q d n -> Term q d n
 pushSubstsT' s = (pushSubstsT s).fst

 public export %inline
-pushSubstsE' : Elim d n -> Elim d n
+pushSubstsE' : Elim q d n -> Elim q d n
 pushSubstsE' e = (pushSubstsE e).fst


-mutual
-  -- tightening a term/elim also causes substitutions to be pushed through.
-  -- this is because otherwise a variable in an unused part of the subst
-  -- would cause it to incorrectly fail
+-- mutual
+--   -- tightening a term/elim also causes substitutions to be pushed through.
+--   -- this is because otherwise a variable in an unused part of the subst
+--   -- would cause it to incorrectly fail

-  export covering
-  Tighten (Term d) where
-    tighten p (TYPE l) =
-      pure $ TYPE l
-    tighten p (Pi qty x arg res) =
-      Pi qty x <$> tighten p arg
-               <*> tighten p res
-    tighten p (Lam x body) =
-      Lam x <$> tighten p body
-    tighten p (E e) =
-      E <$> tighten p e
-    tighten p (CloT tm th) =
-      tighten p $ pushSubstsTWith' id th tm
-    tighten p (DCloT tm th) =
-      tighten p $ pushSubstsTWith' th id tm
+--   export covering
+--   Tighten (Term d) where
+--     tighten p (TYPE l) =
+--       pure $ TYPE l
+--     tighten p (Pi qty x arg res) =
+--       Pi qty x <$> tighten p arg
+--                <*> tighten p res
+--     tighten p (Lam x body) =
+--       Lam x <$> tighten p body
+--     tighten p (E e) =
+--       E <$> tighten p e
+--     tighten p (CloT tm th) =
+--       tighten p $ pushSubstsTWith' id th tm
+--     tighten p (DCloT tm th) =
+--       tighten p $ pushSubstsTWith' th id tm

-  export covering
-  Tighten (Elim d) where
-    tighten p (F x) =
-      pure $ F x
-    tighten p (B i) =
-      B <$> tighten p i
-    tighten p (fun :@ arg) =
-      [|tighten p fun :@ tighten p arg|]
-    tighten p (tm :# ty) =
-      [|tighten p tm :# tighten p ty|]
-    tighten p (CloE el th) =
-      tighten p $ pushSubstsEWith' id th el
-    tighten p (DCloE el th) =
-      tighten p $ pushSubstsEWith' th id el
+--   export covering
+--   Tighten (Elim d) where
+--     tighten p (F x) =
+--       pure $ F x
+--     tighten p (B i) =
+--       B <$> tighten p i
+--     tighten p (fun :@ arg) =
+--       [|tighten p fun :@ tighten p arg|]
+--     tighten p (tm :# ty) =
+--       [|tighten p tm :# tighten p ty|]
+--     tighten p (CloE el th) =
+--       tighten p $ pushSubstsEWith' id th el
+--     tighten p (DCloE el th) =
+--       tighten p $ pushSubstsEWith' th id el

-  export covering
-  Tighten (ScopeTerm d) where
-    tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
-    tighten p (TUnused body) = TUnused <$> tighten p body
+--   export covering
+--   Tighten (ScopeTerm d) where
+--     tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
+--     tighten p (TUnused body) = TUnused <$> tighten p body


 public export %inline
-weakT : Term d n -> Term d (S n)
+weakT : Term q d n -> Term q d (S n)
 weakT t = t //. shift 1

 public export %inline
-weakE : Elim d n -> Elim d (S n)
+weakE : Elim q d n -> Elim q d (S n)
 weakE t = t //. shift 1


 mutual
  public export
-  data IsRedexT : Term d n -> Type where
+  data IsRedexT : Term q d n -> Type where
    IsUpsilonT : IsRedexT $ E (_ :# _)
    IsCloT     : IsRedexT $ CloT {}
    IsDCloT    : IsRedexT $ DCloT {}
    IsERedex   : IsRedexE e -> IsRedexT $ E e

  public export %inline
-  NotRedexT : Term d n -> Type
+  NotRedexT : Term q d n -> Type
  NotRedexT = Not . IsRedexT

  public export
-  data IsRedexE : Elim d n -> Type where
+  data IsRedexE : Elim q d n -> Type where
    IsUpsilonE : IsRedexE $ E _ :# _
    IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
    IsCloE     : IsRedexE $ CloE {}
    IsDCloE    : IsRedexE $ DCloE {}

  public export %inline
-  NotRedexE : Elim d n -> Type
+  NotRedexE : Elim q d n -> Type
  NotRedexE = Not . IsRedexE


 mutual
  export %inline
-  isRedexT : (t : Term d n) -> Dec (IsRedexT t)
+  isRedexT : (t : Term {}) -> Dec (IsRedexT t)
  isRedexT (E (tm :# ty)) = Yes IsUpsilonT
  isRedexT (CloT {})      = Yes IsCloT
  isRedexT (DCloT {})     = Yes IsDCloT
@ -201,77 +215,76 @@ mutual
  isRedexT (E (DCloE {})) = Yes $ IsERedex IsDCloE
  isRedexT (E e@(_ :@ _)) with (isRedexE e)
    _ | Yes yes = Yes $ IsERedex yes
-    _ | No  no  = No \case IsERedex p => no p
-  isRedexT (TYPE {}) = No $ \x => case x of {}
-  isRedexT (Pi   {}) = No $ \x => case x of {}
-  isRedexT (Lam  {}) = No $ \x => case x of {}
-  isRedexT (E (F _)) = No $ \x => case x of IsERedex _ impossible
-  isRedexT (E (B _)) = No $ \x => case x of IsERedex _ impossible
+    _ | No  no  = No  $ \case IsERedex p => no p
+  isRedexT (TYPE {}) = No $ \case _ impossible
+  isRedexT (Pi   {}) = No $ \case _ impossible
+  isRedexT (Lam  {}) = No $ \case _ impossible
+  isRedexT (E (F _)) = No $ \case IsERedex _ impossible
+  isRedexT (E (B _)) = No $ \case IsERedex _ impossible

  export %inline
-  isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
+  isRedexE : (e : Elim {}) -> Dec (IsRedexE e)
  isRedexE (E _ :# _)                    = Yes IsUpsilonE
  isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
  isRedexE (CloE {})                     = Yes IsCloE
  isRedexE (DCloE {})                    = Yes IsDCloE
-  isRedexE (F x)                         = No $ \x => case x of {}
-  isRedexE (B i)                         = No $ \x => case x of {}
-  isRedexE (F _                    :@ _) = No $ \x => case x of {}
-  isRedexE (B _                    :@ _) = No $ \x => case x of {}
-  isRedexE (_ :@ _                 :@ _) = No $ \x => case x of {}
-  isRedexE ((TYPE _   :# _)        :@ _) = No $ \x => case x of {}
-  isRedexE ((Pi {}    :# _)        :@ _) = No $ \x => case x of {}
-  isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
-  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
-  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
-  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
-  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
-  isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
-  isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
-  isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
-  isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
-  isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
-  isRedexE (TYPE _   :# _)               = No $ \x => case x of {}
-  isRedexE (Pi {}    :# _)               = No $ \x => case x of {}
-  isRedexE (Lam {}   :# _)               = No $ \x => case x of {}
-  isRedexE (CloT {}  :# _)               = No $ \x => case x of {}
-  isRedexE (DCloT {} :# _)               = No $ \x => case x of {}
+  isRedexE (F x)                         = No $ \case _ impossible
+  isRedexE (B i)                         = No $ \case _ impossible
+  isRedexE (F _                    :@ _) = No $ \case _ impossible
+  isRedexE (B _                    :@ _) = No $ \case _ impossible
+  isRedexE (_ :@ _                 :@ _) = No $ \case _ impossible
+  isRedexE ((TYPE _   :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((Pi {}    :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \case _ impossible
+  isRedexE ((E _      :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((CloT {}  :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((DCloT {} :# _)        :@ _) = No $ \case _ impossible
+  isRedexE (CloE {}                :@ _) = No $ \case _ impossible
+  isRedexE (DCloE {}               :@ _) = No $ \case _ impossible
+  isRedexE (TYPE _   :# _)               = No $ \case _ impossible
+  isRedexE (Pi {}    :# _)               = No $ \case _ impossible
+  isRedexE (Lam {}   :# _)               = No $ \case _ impossible
+  isRedexE (CloT {}  :# _)               = No $ \case _ impossible
+  isRedexE (DCloT {} :# _)               = No $ \case _ impossible


 public export %inline
-RedexTerm : Nat -> Nat -> Type
-RedexTerm d n = Subset (Term d n) IsRedexT
+RedexTerm : Type -> Nat -> Nat -> Type
+RedexTerm q d n = Subset (Term q d n) IsRedexT

 public export %inline
-NonRedexTerm : Nat -> Nat -> Type
-NonRedexTerm d n = Subset (Term d n) NotRedexT
-
+NonRedexTerm : Type -> Nat -> Nat -> Type
+NonRedexTerm q d n = Subset (Term q d n) NotRedexT

 public export %inline
-RedexElim : Nat -> Nat -> Type
-RedexElim d n = Subset (Elim d n) IsRedexE
+RedexElim : Type -> Nat -> Nat -> Type
+RedexElim q d n = Subset (Elim q d n) IsRedexE

 public export %inline
-NonRedexElim : Nat -> Nat -> Type
-NonRedexElim d n = Subset (Elim d n) NotRedexE
+NonRedexElim : Type -> Nat -> Nat -> Type
+NonRedexElim q d n = Subset (Elim q d n) NotRedexE


 ||| substitute a term with annotation for the bound variable of a `ScopeTerm`
 export %inline
-substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
+substScope : (arg, argTy : Term q d n) -> (body : ScopeTerm q d n) -> Term q d n
 substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
 substScope arg argTy (TUnused body) = body

 mutual
  export %inline
-  stepT' : (s : Term d n) -> IsRedexT s -> Term d n
+  stepT' : (s : Term q d n) -> IsRedexT s -> Term q d n
  stepT' (E (s :# _)) IsUpsilonT   = s
  stepT' (CloT  s th) IsCloT       = pushSubstsTWith' id th s
  stepT' (DCloT s th) IsDCloT      = pushSubstsTWith' th id s
  stepT' (E e)        (IsERedex p) = E $ stepE' e p

  export %inline
-  stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
+  stepE' : (e : Elim q d n) -> IsRedexE e -> Elim q d n
  stepE' (E e :# _) IsUpsilonE = e
  stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
    substScope s arg body :# substScope s arg res
@ -279,21 +292,21 @@ mutual
  stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e

 export %inline
-stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
+stepT : (s : Term q d n) -> Either (NotRedexT s) (Term q d n)
 stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n

 export %inline
-stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
+stepE : (e : Elim q d n) -> Either (NotRedexE e) (Elim q d n)
 stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n

 export covering
-whnfT : Term d n -> NonRedexTerm d n
+whnfT : Term q d n -> NonRedexTerm q d n
 whnfT s = case stepT s of
               Right s'   => whnfT s'
               Left  done => Element s done

 export covering
-whnfE : Elim d n -> NonRedexElim d n
+whnfE : Elim q d n -> NonRedexElim q d n
 whnfE e = case stepE e of
               Right e'   => whnfE e'
               Left  done => Element e done
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@ -9,74 +9,100 @@ import Data.Vect
 %default total


-public export %inline
-isLam : Term d n -> Bool
-isLam (Lam {}) = True
-isLam _        = False
-
 public export
-NotLam : Term d n -> Type
-NotLam = So . not . isLam
-
+data IsLam : Term {} -> Type where
+  ItIsLam : IsLam $ Lam x body

 public export %inline
-isApp : Elim d n -> Bool
-isApp ((:@) {}) = True
-isApp _         = False
+isLam : (s : Term {}) -> Dec (IsLam s)
+isLam (TYPE _)   = No $ \case _ impossible
+isLam (Pi {})    = No $ \case _ impossible
+isLam (Lam {})   = Yes ItIsLam
+isLam (E _)      = No $ \case _ impossible
+isLam (CloT {})  = No $ \case _ impossible
+isLam (DCloT {}) = No $ \case _ impossible
+
+public export %inline
+NotLam : Term {} -> Type
+NotLam = Not . IsLam
+

 public export
-NotApp : Elim d n -> Type
-NotApp = So . not . isApp
+data IsApp : Elim {} -> Type where
+  ItIsApp : IsApp $ f :@ s
+
+public export %inline
+isApp : (e : Elim {}) -> Dec (IsApp e)
+isApp (F _)      = No $ \case _ impossible
+isApp (B _)      = No $ \case _ impossible
+isApp (_ :@ _)   = Yes ItIsApp
+isApp (_ :# _)   = No $ \case _ impossible
+isApp (CloE {})  = No $ \case _ impossible
+isApp (DCloE {}) = No $ \case _ impossible
+
+public export
+NotApp : Elim {} -> Type
+NotApp = Not . IsApp


 infixl 9 :@@
 ||| apply multiple arguments at once
 public export %inline
-(:@@) : Elim d n -> List (Term d n) -> Elim d n
+(:@@) : Elim q d n -> List (Term q d n) -> Elim q d n
 f :@@ ss = foldl (:@) f ss

 public export
-record GetArgs (d, n : Nat) where
+record GetArgs q d n where
  constructor GotArgs
-  fun      : Elim d n
-  args     : List (Term d n)
+  fun      : Elim q d n
+  args     : List (Term q d n)
  0 notApp : NotApp fun

 export
-getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
-getArgs' fun args with (choose $ isApp fun)
-  getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
-  _ | Right no = GotArgs {fun, args, notApp = no}
+getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
+getArgs' fun args with (isApp fun)
+  getArgs' (f :@ a) args | Yes yes = getArgs' f (a :: args)
+  getArgs' fun args      | No  no  = GotArgs {fun, args, notApp = no}

 ||| splits an application into its head and arguments. if it's not an
 ||| application then the list is just empty
 export %inline
-getArgs : Elim d n -> GetArgs d n
+getArgs : Elim q d n -> GetArgs q d n
 getArgs e = getArgs' e []


 infixr 1 :\\
 public export
-(:\\) : Vect m Name -> Term d (m + n) -> Term d n
-[]      :\\ t = t
-x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
-                Lam x $ TUsed $ xs :\\ t'
+absN : Vect m Name -> 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
+
+public export %inline
+(:\\) : Vect m Name -> Term q d (m + n) -> Term q d n
+(:\\) = absN
+

 public export
-record GetLams (d, n : Nat) where
+record GetLams q d n where
  constructor GotLams
  names    : Vect lams Name
-  body     : Term d rest
+  body     : Term q d rest
  0 eq     : lams + n = rest
  0 notLam : NotLam body

-public export
-getLams : Term d n -> GetLams d n
-getLams s with (choose $ isLam s)
-  getLams s@(Lam x body) | Left yes =
-    let inner = getLams $ assert_smaller s $ fromScopeTerm body in
-    GotLams {names  = x :: inner.names,
-             body   = inner.body,
-             eq     = plusSuccRightSucc {} `trans` inner.eq,
-             notLam = inner.notLam}
-  _ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
+export
+getLams' : forall lams, rest.
+           Vect lams Name -> Term q d rest -> lams + n = rest -> GetLams q d n
+getLams' xs s eq with (isLam s)
+  getLams' xs (Lam x sbody) Refl | Yes ItIsLam =
+    let 0 s  = Lam x sbody
+        body = assert_smaller s $ fromScopeTerm sbody
+    in
+    getLams' (x :: xs) body Refl
+  getLams' xs s eq | No no =
+    GotLams xs s eq no
+
+export
+getLams : Term q d n -> GetLams q d n
+getLams s = getLams' [] s Refl
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@ -5,8 +5,8 @@ import Quox.Syntax.Term.Base
 %default total


-export FromVar (Elim d) where fromVar = B
-export FromVar (Term d) where fromVar = E . fromVar
+export FromVar (Elim q d) where fromVar = B
+export FromVar (Term q d) where fromVar = E . fromVar

 ||| does the minimal reasonable work:
 ||| - deletes the closure around a free name since it doesn't do anything
@ -15,7 +15,7 @@ export FromVar (Term d) where fromVar = E . fromVar
 ||| - immediately looks up a bound variable
 ||| - otherwise, wraps in a new closure
 export
-CanSubst (Elim d) (Elim d) where
+CanSubst (Elim q d) (Elim q d) where
  F x       // _  = F x
  B i       // th = th !! i
  CloE e ph // th = assert_total CloE e $ ph . th
@ -30,7 +30,7 @@ CanSubst (Elim d) (Elim d) where
 ||| - goes inside `E` in case it is a simple variable or something
 ||| - otherwise, wraps in a new closure
 export
-CanSubst (Elim d) (Term d) where
+CanSubst (Elim q d) (Term q d) where
  TYPE l    // _  = TYPE l
  E e       // th = E $ e // th
  CloT s ph // th = CloT s $ ph . th
@ -39,13 +39,13 @@ CanSubst (Elim d) (Term d) where
                         th       => CloT s th

 export
-CanSubst (Elim d) (ScopeTerm d) where
+CanSubst (Elim q d) (ScopeTerm q d) where
  TUsed   body // th = TUsed   $ body // push th
  TUnused body // th = TUnused $ body // th

-export CanSubst Var (Term      d) where s // th = s // map (B {d}) th
-export CanSubst Var (Elim      d) where e // th = e // map (B {d}) th
-export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
+export CanSubst Var (Term      q d) where s // th = s // map (B {q, d}) th
+export CanSubst Var (Elim      q d) where e // th = e // map (B {q, d}) th
+export CanSubst Var (ScopeTerm q d) where s // th = s // map (B {q, d}) th


 infixl 8 //., ///
@ -53,13 +53,13 @@ mutual
  namespace Term
    ||| applies a term substitution with a less ambiguous type
    export
-    (//.) : Term d from -> TSubst d from to -> Term d to
+    (//.) : Term q d from -> TSubst q d from to -> Term q d to
    t //. th = t // th

    ||| applies a dimension substitution with the same behaviour as `(//)`
    ||| above
    export
-    (///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
+    (///) : Term q dfrom n -> DSubst dfrom dto -> Term q dto n
    TYPE l     /// _        = TYPE l
    E e        /// th       = E $ e /// th
    DCloT s ph /// th       = DCloT s $ ph . th
@ -68,20 +68,20 @@ mutual

    ||| applies a term and dimension substitution
    public export %inline
-    subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           Term dto to
+    subs : Term q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           Term q dto to
    subs s th ph = s /// th // ph

  namespace Elim
    ||| applies a term substitution with a less ambiguous type
    export
-    (//.) : Elim d from -> TSubst d from to -> Elim d to
+    (//.) : Elim q d from -> TSubst q d from to -> Elim q d to
    e //. th = e // th

    ||| applies a dimension substitution with the same behaviour as `(//)`
    ||| above
    export
-    (///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
+    (///) : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
    F x        /// _        = F x
    B i        /// _        = B i
    DCloE e ph /// th       = DCloE e $ ph . th
@ -90,46 +90,46 @@ mutual

    ||| applies a term and dimension substitution
    public export %inline
-    subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           Elim dto to
+    subs : Elim q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           Elim q dto to
    subs e th ph = e /// th // ph

  namespace ScopeTerm
    ||| applies a term substitution with a less ambiguous type
    export
-    (//.) : ScopeTerm d from -> TSubst d from to -> ScopeTerm d to
+    (//.) : ScopeTerm q d from -> TSubst q d from to -> ScopeTerm q d to
    body //. th = body // th

    ||| applies a dimension substitution with the same behaviour as `(//)`
    ||| above
    export
-    (///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
+    (///) : ScopeTerm q dfrom n -> DSubst dfrom dto -> ScopeTerm q dto n
    TUsed   body /// th = TUsed   $ body /// th
    TUnused body /// th = TUnused $ body /// th

    ||| applies a term and dimension substitution
    public export %inline
-    subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           ScopeTerm dto to
+    subs : ScopeTerm q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           ScopeTerm q dto to
    subs body th ph = body /// th // ph

-export CanShift (Term      d) where s // by = s //. Shift by
-export CanShift (Elim      d) where e // by = e //. Shift by
-export CanShift (ScopeTerm d) where s // by = s //. Shift by
+export CanShift (Term      q d) where s // by = s //. Shift by
+export CanShift (Elim      q d) where e // by = e //. Shift by
+export CanShift (ScopeTerm q d) where s // by = s //. Shift by


 export %inline
-comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
-        TSubst dto from to
+comp' : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
+        TSubst q dto from to
 comp' th ps ph = map (/// th) ps . ph


 export
-fromDScopeTerm : DScopeTerm d n -> Term (S d) n
+fromDScopeTerm : DScopeTerm q d n -> Term q (S d) n
 fromDScopeTerm (DUsed   body) = body
 fromDScopeTerm (DUnused body) = body /// shift 1

 export
-fromScopeTerm : ScopeTerm d n -> Term d (S n)
+fromScopeTerm : ScopeTerm q d n -> Term q d (S n)
 fromScopeTerm (TUsed   body) = body
 fromScopeTerm (TUnused body) = body //. shift 1
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@ -2,12 +2,13 @@ module Quox.Syntax.Var

 import Quox.Name
 import Quox.Pretty
-import Quox.OPE
+-- import Quox.OPE

 import Data.Nat
 import Data.List
-import Decidable.Equality
+import public Quox.Decidable
 import Data.Bool.Decidable
+import Data.DPair

 %default total

@ -34,6 +35,11 @@ export %inline Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat

 public export %inline Injective VS where injective Refl = Refl

+export Uninhabited (Var 0) where uninhabited _ impossible
+
+export Uninhabited (VZ   = VS i) where uninhabited _ impossible
+export Uninhabited (VS i = VZ)   where uninhabited _ impossible
+

 parameters {auto _ : Pretty.HasEnv m}
  private
@ -142,14 +148,14 @@ public export FromVar Var where fromVar = id


 public export
-data LT : Var n -> Var n -> Type where
+data LT : Rel (Var n) where
  LTZ : VZ `LT` VS i
  LTS : i `LT` j -> VS i `LT` VS j
 %builtin Natural Var.LT
 %name Var.LT lt

 public export %inline
-GT : Var n -> Var n -> Type
+GT : Rel (Var n)
 i `GT` j = j `LT` i

 export
@ -160,49 +166,61 @@ Transitive (Var n) LT where
 export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
 export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible

+
 export
-isLT : (i, j : Var n) -> Dec (i `LT` j)
-isLT VZ     VZ     = No uninhabited
-isLT VZ     (VS j) = Yes LTZ
-isLT (VS i) VZ     = No uninhabited
-isLT (VS i) (VS j) with (isLT i j)
-  _ | Yes prf   = Yes (LTS prf)
-  _ | No contra = No  (\case LTS p => contra p)
+ltReflect : LT {n} `Reflects2` (<)
+ltReflect VZ     VZ     = RFalse absurd
+ltReflect VZ     (VS j) = RTrue LTZ
+ltReflect (VS i) VZ     = RFalse absurd
+ltReflect (VS i) (VS j) with (ltReflect i j) | (i < j)
+  _ | RTrue  yes | True  = RTrue  $ LTS yes
+  _ | RFalse no  | False = RFalse $ \case LTS p => no p
+
+export
+isLT : Dec2 Var.LT
+isLT i j = reflectToDec $ ltReflect i j


 public export
-data Compare : (i, j : Var n) -> Type where
-  IsLT : (lt : i `LT` j) -> Compare i j
-  IsEQ :                    Compare i i
-  IsGT : (gt : i `GT` j) -> Compare i j
+data Compare : (i, j : Var n) -> Ordering -> Type where
+  IsLT : (lt : i `LT` j) -> Compare i j LT
+  IsEQ :                    Compare i i EQ
+  IsGT : (gt : i `GT` j) -> Compare i j GT
 %name Compare cmp

 export
-compareS : Compare i j -> Compare (VS i) (VS j)
+compareS : Compare i j o -> Compare (VS i) (VS j) o
 compareS (IsLT lt) = IsLT (LTS lt)
 compareS IsEQ      = IsEQ
 compareS (IsGT gt) = IsGT (LTS gt)

 export
-compareP : (i, j : Var n) -> Compare i j
+compareP : (i, j : Var n) -> Compare i j (compare i j)
 compareP VZ     VZ     = IsEQ
 compareP VZ     (VS j) = IsLT LTZ
 compareP (VS i) VZ     = IsGT LTZ
 compareP (VS i) (VS j) = compareS $ compareP i j

 export
-0 compareSelf : (c : Compare i i) -> c = IsEQ
-compareSelf (IsLT lt) = absurd lt
-compareSelf IsEQ      = Refl
-compareSelf (IsGT gt) = absurd gt
+0 compare2 : Compare {n} i j o -> o = compare i j
+compare2 (IsLT LTZ)      = Refl
+compare2 (IsLT (LTS lt)) = compare2 (IsLT lt)
+compare2 IsEQ            = sym $ compareNatDiag i.nat
+compare2 (IsGT LTZ)      = Refl
+compare2 (IsGT (LTS gt)) = compare2 $ IsGT gt
+compare2 _ {n = 0}       = absurd i

 export
-0 comparePSelf : (i : Var n) -> compareP i i = IsEQ
-comparePSelf i = compareSelf {}
+0 compareSelf : Compare i i o -> o = EQ
+compareSelf p = rewrite compare2 p in compareNatDiag i.nat
+
+export
+0 comparePSelf : (i : Var n) -> Compare i i EQ
+comparePSelf i = rewrite sym $ compareNatDiag i.nat in compareP i i


 public export
-data LTE : Var n -> Var n -> Type where
+data LTE : Rel (Var n) where
  LTEZ : VZ `LTE` j
  LTES : i  `LTE` j -> VS i `LTE` VS j

@ -226,12 +244,19 @@ splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `LT` j)
 splitLTE {j = VZ}   LTEZ     = Left Refl
 splitLTE {j = VS _} LTEZ     = Right LTZ
 splitLTE            (LTES p) with (splitLTE p)
-  _ | (Left  eq) = Left $ cong VS eq
-  _ | (Right lt) = Right $ LTS lt
+  _ | Left  eq = Left  $ cong VS eq
+  _ | Right lt = Right $ LTS lt

+export Uninhabited (VS i `LTE` VZ) where uninhabited _ impossible

-export Uninhabited (VZ   = VS i) where uninhabited _ impossible
-export Uninhabited (VS i = VZ)   where uninhabited _ impossible
+export
+lteReflect : (i, j : Var n) -> (LTE i j) `Reflects` (i <= j)
+lteReflect VZ     VZ     = RTrue LTEZ
+lteReflect VZ     (VS j) = RTrue LTEZ
+lteReflect (VS i) VZ     = RFalse absurd
+lteReflect (VS i) (VS j) with (lteReflect i j) | (i <= j)
+  _ | RTrue  yes | True  = RTrue (LTES yes)
+  _ | RFalse no  | False = RFalse $ \case LTES lte => no lte


 public export
@ -239,15 +264,9 @@ eqReflect : (i, j : Var n) -> (i = j) `Reflects` (i == j)
 eqReflect VZ     VZ     = RTrue  Refl
 eqReflect VZ     (VS i) = RFalse absurd
 eqReflect (VS i) VZ     = RFalse absurd
-eqReflect (VS i) (VS j) with (eqReflect i j)
-  eqReflect (VS i) (VS j) | r with (i == j)
-    eqReflect (VS i) (VS j) | RTrue  yes | True   =  RTrue  $ cong VS yes
-    eqReflect (VS i) (VS j) | RFalse no  | False  =  RFalse $ no . injective
-
-public export
-reflectToDec : p `Reflects` b -> Dec p
-reflectToDec (RTrue  y) = Yes y
-reflectToDec (RFalse n) = No  n
+eqReflect (VS i) (VS j) with (eqReflect i j) | (i == j)
+  _ | RTrue  yes | True  = RTrue  $ cong VS yes
+  _ | RFalse no  | False = RFalse $ no . injective

 public export %inline
 varDecEq : (i, j : Var n) -> Dec (i = j)
@ -264,10 +283,10 @@ decEqFromBool i j =

 public export %inline DecEq (Var n) where decEq = varDecEq

-export
-Tighten Var where
-  tighten Id       i      = pure i
-  tighten (Drop q) VZ     = empty
-  tighten (Drop q) (VS i) = tighten q i
-  tighten (Keep q) VZ     = pure VZ
-  tighten (Keep q) (VS i) = VS <$> tighten q i
+-- export
+-- Tighten Var where
+--   tighten Id       i      = pure i
+--   tighten (Drop q) VZ     = empty
+--   tighten (Drop q) (VS i) = tighten q i
+--   tighten (Keep q) VZ     = pure VZ
+--   tighten (Keep q) (VS i) = VS <$> tighten q i
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@ -4,67 +4,76 @@ import public Quox.Syntax
 import public Quox.Typing
 import public Quox.Equal
 import public Control.Monad.Either
+import Decidable.Decidable

 %default total


 private covering %inline
-expectTYPE : MonadError Error m => Term d n -> m Universe
+expectTYPE : HasErr q m => Term q d n -> m Universe
 expectTYPE s =
  case (whnfT s).fst of
       TYPE l => pure l
       _      => throwError $ ExpectedTYPE s

 private covering %inline
-expectPi : MonadError Error m => Term d n ->
-           m (Qty, Term d n, ScopeTerm d n)
+expectPi : HasErr q m => Term q d n ->
+           m (q, Term q d n, ScopeTerm q d n)
 expectPi ty =
  case (whnfT ty).fst of
       Pi qty _ arg res => pure (qty, arg, res)
       _                => throwError $ ExpectedPi ty

 private %inline
-expectEqualQ : MonadError Error m =>
-               (expect, actual : Qty) -> m ()
+expectEqualQ : HasErr q m => Eq q =>
+               (expect, actual : q) -> m ()
 expectEqualQ pi rh =
  unless (pi == rh) $ throwError $ ClashQ pi rh


 private %inline
-popQ : MonadError Error m => Qty -> QOutput (S n) -> m (QOutput n)
+popQ : HasErr q m => Eq q => q -> QOutput q (S n) -> m (QOutput q n)
 popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx


 private %inline
-tail : TyContext d (S n) -> TyContext d n
+tail : TyContext q d (S n) -> TyContext q d n
 tail = {tctx $= tail, qctx $= tail}


 private %inline
-weakI : InferResult d n -> InferResult d (S n)
+weakI : IsQty q => InferResult q d n -> InferResult q d (S n)
 weakI = {type $= weakT, qout $= (:< zero)}

 private
-lookupBound : {n : Nat} -> Qty -> Var n -> TyContext d n -> InferResult d n
-lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) =
-  InfRes {type = weakT ty, qout = zero :< pi}
+lookupBound : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n
+lookupBound pi VZ ctx@(MkTyContext {tctx = _ :< ty, _}) =
+  InfRes {type = weakT ty, qout = zeroFor (tail ctx) :< pi}
 lookupBound pi (VS i) ctx =
  weakI $ lookupBound pi i (tail ctx)


 private %inline
-subjMult : Qty -> Qty -> Subset Qty IsSubj
-subjMult sg qty =
-  if sg == Zero || qty == Zero
-     then Element Zero %search
-     else Element One  %search
+subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
+subjMult sg qty = if isYes $ isZero qty then szero else sg
+
+
+export
+makeDimEq : DContext d -> DimEq d
+makeDimEq DNil           = zeroEq
+makeDimEq (DBind dctx)   = makeDimEq dctx :<? Nothing
+makeDimEq (DEq p q dctx) = set p q $ makeDimEq dctx


 public export
-CanTC : (Type -> Type) -> Type
-CanTC m = (MonadError Error m, MonadReader Definitions m)
+0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)

-parameters {auto _ : CanTC m}
+public export
+0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
+CanTC q = CanTC' q IsGlobal
+
+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
@ -72,77 +81,75 @@ parameters {auto _ : CanTC m}
  -- computer but pushing is less work for the me

  export covering %inline
-  check : {d, n : Nat} ->
-          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-          (subj : Term d n) -> (ty : Term d n) ->
-          m (CheckResult n)
+  check : (ctx : TyContext q d n) -> (sg : SQty q) ->
+          (subj : Term q d n) -> (ty : Term q d n) ->
+          m (CheckResult q n)
  check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty

  export covering %inline
-  infer : {d, n : Nat} ->
-          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-          (subj : Elim d n) ->
-          m (InferResult d n)
+  infer : (ctx : TyContext q d n) -> (sg : SQty q) ->
+          (subj : Elim q d n) ->
+          m (InferResult q d n)
  infer ctx sg subj = infer' ctx sg (pushSubstsE subj)


  export covering
-  check' : {d, n : Nat} ->
-           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-           (subj : NotCloTerm d n) -> (ty : Term d n) ->
-           m (CheckResult n)
+  check' : (ctx : TyContext q d n) -> (sg : SQty q) ->
+           (subj : NotCloTerm q d n) -> (ty : Term q d n) ->
+           m (CheckResult q n)

  check' ctx sg (Element (TYPE l) _) ty = do
    l' <- expectTYPE ty
-    expectEqualQ zero sg
+    expectEqualQ zero sg.fst
    unless (l < l') $ throwError $ BadUniverse l l'
-    pure zero
+    pure $ zeroFor ctx

  check' ctx sg (Element (Pi qty x arg res) _) ty = do
    l <- expectTYPE ty
-    expectEqualQ zero sg
-    ignore $ check ctx zero arg (TYPE l)
+    expectEqualQ zero sg.fst
+    ignore $ check ctx szero arg (TYPE l)
    case res of
-         TUsed   res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
-         TUnused res => ignore $ check ctx                     zero res (TYPE l)
-    pure zero
+         TUsed   res =>
+           ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
+         TUnused res =>
+           ignore $ check ctx szero res (TYPE l)
+    pure $ zeroFor ctx

  check' ctx sg (Element (Lam x body) _) ty = do
    (qty, arg, res) <- expectPi ty
    -- [todo] do this properly?
    let body = fromScopeTerm body; res = fromScopeTerm res
-    qout <- check (extendTy arg (sg * qty) ctx) sg body res
+    qout <- check (extendTy arg (sg.fst * qty) ctx) sg body res
    popQ qty qout

  check' ctx sg (Element (E e) _) ty = do
    infres <- infer ctx sg e
-    ignore $ check ctx zero ty (TYPE UAny)
-    subT infres.type ty
+    ignore $ check ctx szero ty (TYPE UAny)
+    subTWith (makeDimEq ctx.dctx) infres.type ty
    pure infres.qout

  export covering
-  infer' : {d, n : Nat} ->
-           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-           (subj : NotCloElim d n) ->
-           m (InferResult d n)
+  infer' : (ctx : TyContext q d n) -> (sg : SQty q) ->
+           (subj : NotCloElim q d n) ->
+           m (InferResult q d n)

  infer' ctx sg (Element (F x) _) = do
    Just g <- asks $ lookup x  | Nothing => throwError $ NotInScope x
-    when (isZero g) $ expectEqualQ sg Zero
-    pure $ InfRes {type = g.type.def, qout = zero}
+    when (isZero g) $ expectEqualQ sg.fst zero
+    pure $ InfRes {type = g.type.get, qout = zeroFor ctx}

  infer' ctx sg (Element (B i) _) =
-    pure $ lookupBound sg i ctx
+    pure $ lookupBound sg.fst i ctx

  infer' ctx sg (Element (fun :@ arg) _) = do
    funres <- infer ctx sg fun
    (qty, argty, res) <- expectPi funres.type
-    let Element sg' _ = subjMult sg qty
+    let sg' = subjMult sg qty
    argout <- check ctx sg' arg argty
    pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
                   qout = funres.qout + argout}

  infer' ctx sg (Element (tm :# ty) _) = do
-    ignore $ check ctx zero ty (TYPE UAny)
+    ignore $ check ctx szero ty (TYPE UAny)
    qout <- check ctx sg tm ty
    pure $ InfRes {type = ty, qout}
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@ -6,6 +6,7 @@ import public Quox.Definition

 import Data.Nat
 import public Data.SortedMap
+import Control.Monad.Either
 import Control.Monad.Reader
 import Control.Monad.State
 import Generics.Derive
@ -24,71 +25,76 @@ data DContext : Nat -> Type where
  DEq   : Dim d -> Dim d -> DContext d -> DContext d

 public export
-TContext : Nat -> Nat -> Type
-TContext d = Context (Term d)
+TContext : Type -> Nat -> Nat -> Type
+TContext q d = Context (Term q d)

 public export
-QContext : Nat -> Type
-QContext = Context' Qty
+QContext : Type -> Nat -> Type
+QContext = Context'

 public export
-QOutput : Nat -> Type
+QOutput : Type -> Nat -> Type
 QOutput = QContext


 public export
-record TyContext (d, n : Nat) where
+record TyContext q d n where
  constructor MkTyContext
  dctx : DContext d
-  tctx : TContext d n
-  qctx : QContext n
+  tctx : TContext q d n
+  qctx : QContext q n

 %name TyContext ctx


 namespace TContext
  export
-  pushD : TContext d n -> TContext (S d) n
+  pushD : TContext q d n -> TContext q (S d) n
  pushD tel = map (/// shift 1) tel


 namespace TyContext
  export
-  extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
+  extendTy : Term q d n -> q -> TyContext q d n -> TyContext q d (S n)
  extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}

  export
-  extendDim : TyContext d n -> TyContext (S d) n
+  extendDim : TyContext q d n -> TyContext q (S d) n
  extendDim = {dctx $= DBind, tctx $= pushD}

  export
-  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
+  eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
  eqDim p q = {dctx $= DEq p q}


 namespace QOutput
-  export
-  (+) : QOutput n -> QOutput n -> QOutput n
-  (+) = zipWith (+)
+  parameters {auto _ : IsQty q}
+    export
+    (+) : QOutput q n -> QOutput q n -> QOutput q n
+    (+) = zipWith (+)

-  export
-  (*) : Qty -> QOutput n -> QOutput n
-  (*) pi = map (pi *)
+    export
+    (*) : q -> QOutput q n -> QOutput q n
+    (*) pi = map (pi *)

-  export
-  zero : {n : Nat} -> QOutput n
-  zero = pure Zero
+    export
+    zero : {n : Nat} -> QOutput q n
+    zero = pure zero
+
+    export
+    zeroFor : TyContext q _ n -> QOutput q n
+    zeroFor ctx = const zero <$> ctx.qctx


 public export
-CheckResult : Nat -> Type
+CheckResult : Type -> Nat -> Type
 CheckResult = QOutput

 public export
-record InferResult d n where
+record InferResult q d n where
  constructor InfRes
-  type : Term d n
-  qout : QOutput n
+  type : Term q d n
+  qout : QOutput q n


 public export
@ -97,12 +103,16 @@ data EqMode = Equal | Sub


 public export
-data Error
-= ExpectedTYPE (Term d n)
-| ExpectedPi   (Term d n)
+data Error q
+= ExpectedTYPE (Term q d n)
+| ExpectedPi   (Term q d n)
 | BadUniverse  Universe Universe

-| ClashT EqMode (Term d n) (Term d n)
-| ClashU EqMode Universe Universe
-| ClashQ        Qty      Qty
+| ClashT EqMode (Term q d n) (Term q d n)
+| ClashU EqMode Universe     Universe
+| ClashQ        q            q
 | NotInScope    Name
+
+public export
+0 HasErr : Type -> (Type -> Type) -> Type
+HasErr q = MonadError (Error q)
--- a/lib/on-hold/Quox/Lexer.idr
+++ b/lib/on-hold/Quox/Lexer.idr
--- a/lib/on-hold/Quox/OPE.idr
+++ b/lib/on-hold/Quox/OPE.idr
--- a/lib/on-hold/Quox/Parser.idr
+++ b/lib/on-hold/Quox/Parser.idr
--- a/lib/on-hold/Quox/Token.idr
+++ b/lib/on-hold/Quox/Token.idr
--- a/lib/on-hold/Quox/Unicode.idr
+++ b/lib/on-hold/Quox/Unicode.idr
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@ -9,13 +9,15 @@ depends = base, contrib, elab-util, sop, snocvect

 modules =
  Quox.NatExtra,
-  Quox.Unicode,
-  Quox.OPE,
+  Quox.Decidable,
+  -- Quox.Unicode,
+  -- Quox.OPE,
  Quox.Pretty,
  Quox.Syntax,
  Quox.Syntax.Dim,
  Quox.Syntax.DimEq,
  Quox.Syntax.Qty,
+  Quox.Syntax.Qty.Three,
  Quox.Syntax.Shift,
  Quox.Syntax.Subst,
  Quox.Syntax.Term,
@ -27,9 +29,9 @@ modules =
  Quox.Syntax.Universe,
  Quox.Syntax.Var,
  Quox.Definition,
-  Quox.Token,
-  Quox.Lexer,
-  Quox.Parser,
+  -- Quox.Token,
+  -- Quox.Lexer,
+  -- Quox.Parser,
  Quox.Context,
  Quox.Equal,
  Quox.Name,
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@ -1,7 +1,7 @@
 module TermImpls

 import Quox.Syntax
-import Quox.Pretty
+import public Quox.Pretty


 private
@ -22,7 +22,7 @@ eqSubst (_ ::: _)  (Shift _)  = Nothing

 mutual
  export covering
-  Eq (Term d n) where
+  Eq q => Eq (Term q d n) where
    TYPE k == TYPE l = k == l
    TYPE _ == _ = False

@ -49,7 +49,7 @@ mutual
    DCloT {} == _ = False

  export covering
-  Eq (Elim d n) where
+  Eq q => Eq (Elim q d n) where
    F x == F y = x == y
    F _ == _ = False

@ -75,16 +75,16 @@ mutual
    DCloE {} == _ = False

  export covering
-  Eq (ScopeTerm d n) where
+  Eq q => Eq (ScopeTerm q d n) where
    TUsed   s == TUsed   t = s == t
    TUnused s == TUnused t = s == t
    TUsed   _ == TUnused _ = False
    TUnused _ == TUsed   _ = False

 export covering
-Show (Term d n) where
+PrettyHL q => Show (Term q d n) where
  showPrec d t = showParens (d /= Open) $ prettyStr True t

 export covering
-Show (Elim d n) where
+PrettyHL q => Show (Elim q d n) where
  showPrec d e = showParens (d /= Open) $ prettyStr True e
--- a/tests/Tests.idr
+++ b/tests/Tests.idr
@ -1,18 +1,18 @@
 module Tests

 import TAP
-import Tests.Unicode
-import Tests.Lexer
-import Tests.Parser
+-- import Tests.Unicode
+-- import Tests.Lexer
+-- import Tests.Parser
 import Tests.Reduce
 import Tests.Equal
 import System


 allTests = [
-  Unicode.tests,
-  Lexer.tests,
-  Parser.tests,
+  -- Unicode.tests,
+  -- Lexer.tests,
+  -- Parser.tests,
  Reduce.tests,
  Equal.tests
 ]
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@ -2,10 +2,11 @@ module Tests.Equal

 import Quox.Equal as Lib
 import Quox.Pretty
+import Quox.Syntax.Qty.Three
 import TAP

 export
-ToInfo Error where
+ToInfo (Error Three) where
  toInfo (NotInScope x) =
    [("type", "NotInScope"),
     ("name", show x)]
@ -35,10 +36,11 @@ ToInfo Error where
     ("right", prettyStr True rh)]


-M = ReaderT Definitions (Either Error)
+0 M : Type -> Type
+M = ReaderT (Definitions Three) (Either (Error Three))

 parameters (label : String) (act : Lazy (M ()))
-           {default empty globals : Definitions}
+           {default empty globals : Definitions Three}
  testEq : Test
  testEq = test label $ runReaderT globals act

@ -46,19 +48,19 @@ parameters (label : String) (act : Lazy (M ()))
  testNeq = testThrows label (const True) $ runReaderT globals act


-subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+subT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M ()
 subT = Lib.subT
 %hide Lib.subT

-equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+equalT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M ()
 equalT = Lib.equalT
 %hide Lib.equalT

-subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+subE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M ()
 subE = Lib.subE
 %hide Lib.subE

-equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+equalE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M ()
 equalE = Lib.equalE
 %hide Lib.equalE

@ -139,7 +141,11 @@ tests = "equality & subtyping" :- [
               (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")
+               (Lam "x" $ TUnused $ FT "a"),
+      skipWith "(no η yet)" $
+      testEq "λ x ⇒ [f [x]] ≡ [f]  (η)" $
+        equalT (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0)
+               (FT "f")
    ],

    "term closure" :- [
@ -161,11 +167,11 @@ tests = "equality & subtyping" :- [

    "free var" :-
    let au_bu = fromList
-          [("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
-           ("B", MkDef Any (TYPE (U 1)) (TYPE (U 0)))]
+          [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
+           ("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))]
        au_ba = fromList
-          [("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
-           ("B", MkDef Any (TYPE (U 1)) (FT "A"))]
+          [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
+           ("B", mkDef Any (TYPE (U 1)) (FT "A"))]
    in [
      testEq "A ≡ A" $
        equalE (F "A") (F "A"),
@ -203,6 +209,11 @@ tests = "equality & subtyping" :- [
          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
            :@ FT "a")
          (F "a"),
+      testEq "(λ g ⇒ [g [x]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [x]  (β↘↙)" $
+        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"),
      testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
        subE
          ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@ -1,6 +1,7 @@
 module Tests.Reduce

 import Quox.Syntax as Lib
+import Quox.Syntax.Qty.Three
 import TermImpls
 import TAP

@ -22,17 +23,18 @@ testNoStep step label e = test "\{label}  (no step)" $
       Right e' => with Prelude.(::) Left [("reduced", e')]


+
 parameters {default 0 d, n : Nat}
-  testWhnfT : String -> Term d n -> Term d n -> Test
+  testWhnfT : String -> Term Three d n -> Term Three d n -> Test
  testWhnfT = testWhnf whnfT

-  testWhnfE : String -> Elim d n -> Elim d n -> Test
+  testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
  testWhnfE = testWhnf whnfE

-  testNoStepE : String -> Elim d n -> Test
+  testNoStepE : String -> Elim Three d n -> Test
  testNoStepE = testNoStep stepE

-  testNoStepT : String -> Term d n -> Test
+  testNoStepT : String -> Term Three d n -> Test
  testNoStepT = testNoStep stepT


--- a/tests/on-hold/Tests/Lexer.idr
+++ b/tests/on-hold/Tests/Lexer.idr
--- a/tests/on-hold/Tests/Parser.idr
+++ b/tests/on-hold/Tests/Parser.idr
--- a/tests/on-hold/Tests/Unicode.idr
+++ b/tests/on-hold/Tests/Unicode.idr
Author	SHA1	Message	Date
rhiannon morris	b25e5320d9	some more properties of var	2023-01-12 16:03:09 +01:00
rhiannon morris	ef8b8b0da3	index Var.Compare by compare i may go back on this if it's too annoying	2023-01-10 00:17:24 +01:00
rhiannon morris	f405aeb7f9	simplify some matches	2023-01-09 23:45:21 +01:00
rhiannon morris	82795e9976	remove IsOne stuff; add timesSubj	2023-01-09 23:43:55 +01:00
rhiannon morris	28055c0f39	add Decidable-related stuff	2023-01-09 23:43:23 +01:00
rhiannon morris	84e524c978	make typechecker actually pass the dimeq to subT also erase some length arguments	2023-01-09 19:03:21 +01:00
rhiannon morris	d8df40ab39	β↘↙ test	2023-01-08 21:46:42 +01:00
rhiannon morris	c45a963ba0	parameterise over qty semiring	2023-01-08 20:44:25 +01:00
rhiannon morris	961c8415b5	a skipped η test	2023-01-08 15:44:29 +01:00
rhiannon morris	28eb99c091	style tweaks	2023-01-08 15:44:20 +01:00
rhiannon morris	0c1b3a78c3	remove ope stuff too	2023-01-08 15:43:54 +01:00
rhiannon morris	9dbd0b066c	AnyTerm.(.def) => (.get)	2023-01-08 15:07:01 +01:00
rhiannon morris	98fa8d9967	mode eq mode into a reader	2023-01-08 14:59:25 +01:00
rhiannon morris	8443b2f6d8	remove lex/parse stuff for now	2023-01-08 14:58:18 +01:00
rhiannon morris	44c4aea06c	nix flake update	2023-01-07 14:06:19 +01:00