some more properties of var

i may go back on this if it's too annoying

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))

flake.lock

@@ -130,11 +130,11 @@
     },
     "flake-utils": {
       "locked": {
-        "lastModified": 1667077288,
+        "lastModified": 1667395993,
-        "narHash": "sha256-bdC8sFNDpT0HK74u9fUkpbf1MEzVYJ+ka7NXCdgBoaA=",
+        "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,
+        "lastModified": 1672997035,
-        "narHash": "sha256-xfSTHYxuKRiqF4dcuAFdti1OUvrC2lHpQqCHWUK5/JA=",
+        "narHash": "sha256-DNaNjsGMRYefBTAxFIrVOB2ok477cj1FTpqnu/mKRf4=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7f9be6a505a31f88499c5d20d11f98accf5ae6ba",
+        "rev": "f1ffcf798e93b169321106a4aef79526a2b4bd0a",
         "type": "github"
       },
       "original": {

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

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
+  qty  : q
-  0 qtyGlobal : IsGlobal qty
+  type : AnyTerm q
-  type        : AnyTerm
+  term : Maybe $ AnyTerm q
-  term        : Maybe AnyTerm
+  {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) =>
+mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
-           (type, term : forall d, n. Term d n) -> Definition
+        (type, term : forall d, n. Term q d n) -> Definition q
-MkDef {qty, type, term} =
+mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
-  MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
 
 public export %inline
-MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
+mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
-             (type : forall d, n. Term d n) -> Definition
+             (type : forall d, n. Term q d n) -> Definition q
-MkAbstract {qty, type} =
+mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
-  MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
 
 
 public export %inline
-(.type0) : Definition -> Term 0 0
+(.type0) : Definition' q _ -> Term q 0 0
-g.type0 = g.type.def
+g.type0 = g.type.get
 
 public export %inline
-(.term0) : Definition -> Maybe (Term 0 0)
+(.term0) : Definition' q _ -> Maybe (Term q 0 0)
-g.term0 = map (\t => t.def) g.term
+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 : IsQty q => Definition q -> Bool
-isZero g = g.qty == Zero
+isZero g = isYes $ isZero g.qty
 
 public export
-Definitions : Type
+0 Definitions' : (q : Type) -> (q -> Type) -> Type
-Definitions = SortedMap Name Definition
+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

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
+record Env' q (isGlobal : q -> Type) where
-CanEq m = (MonadError Error m, MonadReader Definitions m)
+  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}
+public export
-  private %inline
+0 CanEqual' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
-  clashT : EqMode -> Term d n -> Term d n -> m a
+CanEqual' q isGlobal m = (HasErr q m, HasEnv' q isGlobal m)
-  clashT mode = throwError .: ClashT mode
 
-  private %inline
+public export
-  clashE : EqMode -> Elim d n -> Elim d n -> m a
+0 CanEqual : (q : Type) -> IsQty q => (Type -> Type) -> Type
-  clashE mode = throwError .: ClashE mode
+CanEqual q = CanEqual' q IsGlobal
-
-  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
 
 
-    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
+private %inline
-    compareEN : EqMode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
+mode : HasEnv' _ _ m => m EqMode
-    compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
+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
+  private covering %inline
-    compareT : EqMode -> DimEq d -> Term d n -> Term d n -> m ()
+  compareTN : CanEqual' q _ m => Eq q =>
-    compareT mode eqs s t =
+              NonRedexTerm q 0 n -> NonRedexTerm q 0 n -> m ()
-      for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
+  compareTN s t = compareTN' s.fst t.fst s.snd t.snd
 
-    export covering %inline
+  private covering %inline
-    compareE : EqMode -> DimEq d -> Elim d n -> Elim d n -> m ()
+  compareEN : CanEqual' q _ m => Eq q =>
-    compareE mode eqs e f =
+              NonRedexElim q 0 n -> NonRedexElim q 0 n -> m ()
-      for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
+  compareEN e f = compareEN' e.fst f.fst e.snd f.snd
 
 
-    export covering %inline
+  export covering %inline
-    compareT0 : EqMode -> Term 0 n -> Term 0 n -> m ()
+  compareT : CanEqual' q _ m => Eq q =>
-    compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
+             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
+  export covering %inline
-    compareE0 : EqMode -> Elim 0 n -> Elim 0 n -> m ()
+  compareE : CanEqual' q _ m => Eq q =>
-    compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
+             DimEq d -> Elim q d n -> Elim q d n -> m ()
-
+  compareE eqs e f =
-    export covering %inline
+    for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
-    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
+  export covering %inline
-    equalTWith : DimEq d -> Term d n -> Term d n -> m ()
+  compareT0 : CanEqual' q _ m => Eq q => Term q 0 n -> Term q 0 n -> m ()
-    equalTWith = compareT Equal
+  compareT0 s t = compareTN (whnfT s) (whnfT t)
 
-    export covering %inline
+  export covering %inline
-    equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
+  compareE0 : CanEqual' q _ m => Eq q => Elim q 0 n -> Elim q 0 n -> m ()
-    equalEWith = compareE Equal
+  compareE0 e f = compareEN (whnfE e) (whnfE f)
 
-    export covering %inline
+  export covering %inline
-    subTWith : DimEq d -> Term d n -> Term d n -> m ()
+  compareTS0 : CanEqual' q _ m => Eq q =>
-    subTWith = compareT Sub
+               ScopeTerm q 0 n -> ScopeTerm q 0 n -> m ()
-
+  compareTS0 (TUnused body1) (TUnused body2) =
-    export covering %inline
+    compareT0 body1 body2
-    subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
+  compareTS0 body1 body2 =
-    subEWith = compareE Sub
+    compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
 
 
-    export covering %inline
+private %inline
-    equalT : {d : Nat} -> Term d n -> Term d n -> m ()
+into : HasErr q m => HasDefs' q isg m => Eq q =>
-    equalT = equalTWith DimEq.new
+       (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
+export covering %inline
-    equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
+equalTWith : HasErr q m => HasDefs' q _ m => Eq q =>
-    equalE = equalEWith DimEq.new
+             DimEq d -> Term q d n -> Term q d n -> m ()
+equalTWith = into compareT Equal
 
-    export covering %inline
+export covering %inline
-    subT : {d : Nat} -> Term d n -> Term d n -> m ()
+equalEWith : HasErr q m => HasDefs' q _ m => Eq q =>
-    subT = subTWith DimEq.new
+             DimEq d -> Elim q d n -> Elim q d n -> m ()
+equalEWith = into compareE Equal
 
-    export covering %inline
+export covering %inline
-    subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
+subTWith : HasErr q m => HasDefs' q _ m => Eq q =>
-    subE = subEWith DimEq.new
+           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

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)
+  setVar i j eqs with (compareP i j) | (compare i.nat j.nat)
-    _              | IsLT lt = setVar' i j lt eqs
+    setVar i j eqs | IsLT lt | LT = setVar' i j lt eqs
-    setVar i i eqs | IsEQ    = C eqs
+    setVar i i eqs | IsEQ    | EQ = C eqs
-    _              | IsGT gt = setVar' j i gt 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

lib/Quox/Syntax/Qty.idr

@@ -1,84 +1,72 @@
 module Quox.Syntax.Qty
 
 import Quox.Pretty
-
+import public Quox.Decidable
-import Data.Fin
+import Data.DPair
-import Generics.Derive
 
 %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 []      = []
-commas [x] = [x]
+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
+interface Eq q => IsQty q where
-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
   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
+0 SQty : (q : Type) -> IsQty q => Type
-  zero  = Zero; one = One
+SQty q = Subset q IsSubj
-  (+)   = plus; (*) = times
-  (<=.) = compat
 
+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
+0 GQty : (q : Type) -> IsQty q => Type
-  SZero : IsSubj Zero
+GQty q = Subset q IsGlobal
-  SOne  : IsSubj One
 
-export Uninhabited (IsSubj Any) where uninhabited _ impossible
+public export %inline
-
+gzero : IsQty q => GQty q
-public export
+gzero = Element zero zeroIsGlobal
-data IsGlobal : Qty -> Type where
-  GZero : IsGlobal Zero
-  GAny  : IsGlobal Any
-
-export Uninhabited (IsGlobal One) where uninhabited _ impossible

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

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 : Type -> Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (\n => Elim d n)
+  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) ->
+    Pi  : (qty : q) -> (x : Name) ->
-          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
+          (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

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),

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,
+  public export
-  ||| or is `E` applied to such an elimination
+  data NotCloT : Term {} -> Type where
-  public export %inline
+    NCTYPE : NotCloT $ TYPE _
-  topCloT : Term d n -> Bool
+    NCPi   : NotCloT $ Pi {}
-  topCloT (CloT  _ _) = True
+    NCLam  : NotCloT $ Lam {}
-  topCloT (DCloT _ _) = True
+    NCE    : NotCloE e -> NotCloT $ E e
-  topCloT (E e)       = topCloE e
-  topCloT _           = False
 
-  ||| true if an elimination has a closure or dimension closure at the top level
+  public export
-  public export %inline
+  data NotCloE : Elim {} -> Type where
-  topCloE : Elim d n -> Bool
+    NCF   : NotCloE $ F _
-  topCloE (CloE  _ _) = True
+    NCB   : NotCloE $ B _
-  topCloE (DCloE _ _) = True
+    NCApp : NotCloE $ _ :@ _
-  topCloE _           = False
+    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
+  export
-IsNotCloT = So . not . topCloT
+  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
+public export
-NotCloTerm d n = Subset (Term d n) IsNotCloT
+NotCloTerm : Type -> Nat -> Nat -> Type
-
+NotCloTerm q d n = Subset (Term q d n) NotCloT
-public export IsNotCloE : Elim d n -> Type
-IsNotCloE = So . not . topCloE
 
 ||| an elimination which is not a top level closure
-public export NotCloElim : Nat -> Nat -> Type
+public export
-NotCloElim d n = Subset (Elim d n) IsNotCloE
+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 ->
+  pushSubstsTWith : DSubst dfrom dto -> TSubst q dto from to ->
-                    Term dfrom from -> NotCloTerm dto 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 ->
+  pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to ->
-                    Elim dfrom from -> NotCloElim dto 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
+    case notCloE res of
-         Left  _ => assert_total pushSubstsE res
+         Yes _ => ncloE res
-         Right _ => 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
+-- mutual
-  -- tightening a term/elim also causes substitutions to be pushed through.
+--   -- tightening a term/elim also causes substitutions to be pushed through.
-  -- this is because otherwise a variable in an unused part of the subst
+--   -- this is because otherwise a variable in an unused part of the subst
-  -- would cause it to incorrectly fail
+--   -- would cause it to incorrectly fail
 
-  export covering
+--   export covering
-  Tighten (Term d) where
+--   Tighten (Term d) where
-    tighten p (TYPE l) =
+--     tighten p (TYPE l) =
-      pure $ TYPE l
+--       pure $ TYPE l
-    tighten p (Pi qty x arg res) =
+--     tighten p (Pi qty x arg res) =
-      Pi qty x <$> tighten p arg
+--       Pi qty x <$> tighten p arg
-               <*> tighten p res
+--                <*> tighten p res
-    tighten p (Lam x body) =
+--     tighten p (Lam x body) =
-      Lam x <$> tighten p body
+--       Lam x <$> tighten p body
-    tighten p (E e) =
+--     tighten p (E e) =
-      E <$> tighten p e
+--       E <$> tighten p e
-    tighten p (CloT tm th) =
+--     tighten p (CloT tm th) =
-      tighten p $ pushSubstsTWith' id th tm
+--       tighten p $ pushSubstsTWith' id th tm
-    tighten p (DCloT tm th) =
+--     tighten p (DCloT tm th) =
-      tighten p $ pushSubstsTWith' th id tm
+--       tighten p $ pushSubstsTWith' th id tm
 
-  export covering
+--   export covering
-  Tighten (Elim d) where
+--   Tighten (Elim d) where
-    tighten p (F x) =
+--     tighten p (F x) =
-      pure $ F x
+--       pure $ F x
-    tighten p (B i) =
+--     tighten p (B i) =
-      B <$> tighten p i
+--       B <$> tighten p i
-    tighten p (fun :@ arg) =
+--     tighten p (fun :@ arg) =
-      [|tighten p fun :@ tighten p arg|]
+--       [|tighten p fun :@ tighten p arg|]
-    tighten p (tm :# ty) =
+--     tighten p (tm :# ty) =
-      [|tighten p tm :# tighten p ty|]
+--       [|tighten p tm :# tighten p ty|]
-    tighten p (CloE el th) =
+--     tighten p (CloE el th) =
-      tighten p $ pushSubstsEWith' id th el
+--       tighten p $ pushSubstsEWith' id th el
-    tighten p (DCloE el th) =
+--     tighten p (DCloE el th) =
-      tighten p $ pushSubstsEWith' th id el
+--       tighten p $ pushSubstsEWith' th id el
 
-  export covering
+--   export covering
-  Tighten (ScopeTerm d) where
+--   Tighten (ScopeTerm d) where
-    tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
+--     tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
-    tighten p (TUnused body) = TUnused <$> tighten 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
+    _ | No  no  = No  $ \case IsERedex p => no p
-  isRedexT (TYPE {}) = No $ \x => case x of {}
+  isRedexT (TYPE {}) = No $ \case _ impossible
-  isRedexT (Pi   {}) = No $ \x => case x of {}
+  isRedexT (Pi   {}) = No $ \case _ impossible
-  isRedexT (Lam  {}) = No $ \x => case x of {}
+  isRedexT (Lam  {}) = No $ \case _ impossible
-  isRedexT (E (F _)) = No $ \x => case x of IsERedex _ impossible
+  isRedexT (E (F _)) = No $ \case IsERedex _ impossible
-  isRedexT (E (B _)) = No $ \x => case x of 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 (F x)                         = No $ \case _ impossible
-  isRedexE (B i)                         = No $ \x => case x of {}
+  isRedexE (B i)                         = No $ \case _ impossible
-  isRedexE (F _                    :@ _) = No $ \x => case x of {}
+  isRedexE (F _                    :@ _) = No $ \case _ impossible
-  isRedexE (B _                    :@ _) = No $ \x => case x of {}
+  isRedexE (B _                    :@ _) = No $ \case _ impossible
-  isRedexE (_ :@ _                 :@ _) = No $ \x => case x of {}
+  isRedexE (_ :@ _                 :@ _) = No $ \case _ impossible
-  isRedexE ((TYPE _   :# _)        :@ _) = No $ \x => case x of {}
+  isRedexE ((TYPE _   :# _)        :@ _) = No $ \case _ impossible
-  isRedexE ((Pi {}    :# _)        :@ _) = No $ \x => case x of {}
+  isRedexE ((Pi {}    :# _)        :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \case _ impossible
-  isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
+  isRedexE ((E _      :# _)        :@ _) = No $ \case _ impossible
-  isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
+  isRedexE ((CloT {}  :# _)        :@ _) = No $ \case _ impossible
-  isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
+  isRedexE ((DCloT {} :# _)        :@ _) = No $ \case _ impossible
-  isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
+  isRedexE (CloE {}                :@ _) = No $ \case _ impossible
-  isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
+  isRedexE (DCloE {}               :@ _) = No $ \case _ impossible
-  isRedexE (TYPE _   :# _)               = No $ \x => case x of {}
+  isRedexE (TYPE _   :# _)               = No $ \case _ impossible
-  isRedexE (Pi {}    :# _)               = No $ \x => case x of {}
+  isRedexE (Pi {}    :# _)               = No $ \case _ impossible
-  isRedexE (Lam {}   :# _)               = No $ \x => case x of {}
+  isRedexE (Lam {}   :# _)               = No $ \case _ impossible
-  isRedexE (CloT {}  :# _)               = No $ \x => case x of {}
+  isRedexE (CloT {}  :# _)               = No $ \case _ impossible
-  isRedexE (DCloT {} :# _)               = No $ \x => case x of {}
+  isRedexE (DCloT {} :# _)               = No $ \case _ impossible
 
 
 public export %inline
-RedexTerm : Nat -> Nat -> Type
+RedexTerm : Type -> Nat -> Nat -> Type
-RedexTerm d n = Subset (Term d n) IsRedexT
+RedexTerm q d n = Subset (Term q d n) IsRedexT
 
 public export %inline
-NonRedexTerm : Nat -> Nat -> Type
+NonRedexTerm : Type -> Nat -> Nat -> Type
-NonRedexTerm d n = Subset (Term d n) NotRedexT
+NonRedexTerm q d n = Subset (Term q d n) NotRedexT
-
 
 public export %inline
-RedexElim : Nat -> Nat -> Type
+RedexElim : Type -> Nat -> Nat -> Type
-RedexElim d n = Subset (Elim d n) IsRedexE
+RedexElim q d n = Subset (Elim q d n) IsRedexE
 
 public export %inline
-NonRedexElim : Nat -> Nat -> Type
+NonRedexElim : Type -> Nat -> Nat -> Type
-NonRedexElim d n = Subset (Elim d n) NotRedexE
+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

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
+data IsLam : Term {} -> Type where
-NotLam = So . not . isLam
+  ItIsLam : IsLam $ Lam x body
-
 
 public export %inline
-isApp : Elim d n -> Bool
+isLam : (s : Term {}) -> Dec (IsLam s)
-isApp ((:@) {}) = True
+isLam (TYPE _)   = No $ \case _ impossible
-isApp _         = False
+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
+data IsApp : Elim {} -> Type where
-NotApp = So . not . isApp
+  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
+  fun      : Elim q d n
-  args     : List (Term 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' : Elim q d n -> List (Term q d n) -> GetArgs q d n
-getArgs' fun args with (choose $ isApp fun)
+getArgs' fun args with (isApp fun)
-  getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
+  getArgs' (f :@ a) args | Yes yes = getArgs' f (a :: args)
-  _ | Right no = GotArgs {fun, args, notApp = no}
+  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
+absN : Vect m Name -> Term q d (m + n) -> Term q d n
-[]      :\\ t = t
+absN {m = 0}   []        s = s
-x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
+absN {m = S m} (x :: xs) s = Lam x $ TUsed $ absN xs $
-                Lam x $ TUsed $ xs :\\ t'
+                             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
+export
-getLams : Term d n -> GetLams d n
+getLams' : forall lams, rest.
-getLams s with (choose $ isLam s)
+           Vect lams Name -> Term q d rest -> lams + n = rest -> GetLams q d n
-  getLams s@(Lam x body) | Left yes =
+getLams' xs s eq with (isLam s)
-    let inner = getLams $ assert_smaller s $ fromScopeTerm body in
+  getLams' xs (Lam x sbody) Refl | Yes ItIsLam =
-    GotLams {names  = x :: inner.names,
+    let 0 s  = Lam x sbody
-             body   = inner.body,
+        body = assert_smaller s $ fromScopeTerm sbody
-             eq     = plusSuccRightSucc {} `trans` inner.eq,
+    in
-             notLam = inner.notLam}
+    getLams' (x :: xs) body Refl
-  _ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
+  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

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 (Elim q d) where fromVar = B
-export FromVar (Term d) where fromVar = E . fromVar
+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 (Term      q d) where s // th = s // map (B {q, d}) th
-export CanSubst Var (Elim      d) where e // th = e // map (B {d}) th
+export CanSubst Var (Elim      q d) where e // th = e // map (B {q, d}) th
-export CanSubst Var (ScopeTerm d) where s // th = s // map (B {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 ->
+    subs : Term q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
-           Term dto 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 ->
+    subs : Elim q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
-           Elim dto 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 ->
+    subs : ScopeTerm q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
-           ScopeTerm dto to
+           ScopeTerm q dto to
     subs body th ph = body /// th // ph
 
-export CanShift (Term      d) where s // by = s //. Shift by
+export CanShift (Term      q d) where s // by = s //. Shift by
-export CanShift (Elim      d) where e // by = e //. Shift by
+export CanShift (Elim      q d) where e // by = e //. Shift by
-export CanShift (ScopeTerm d) where s // by = s //. 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 ->
+comp' : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
-        TSubst dto from 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

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)
+ltReflect : LT {n} `Reflects2` (<)
-isLT VZ     VZ     = No uninhabited
+ltReflect VZ     VZ     = RFalse absurd
-isLT VZ     (VS j) = Yes LTZ
+ltReflect VZ     (VS j) = RTrue LTZ
-isLT (VS i) VZ     = No uninhabited
+ltReflect (VS i) VZ     = RFalse absurd
-isLT (VS i) (VS j) with (isLT i j)
+ltReflect (VS i) (VS j) with (ltReflect i j) | (i < j)
-  _ | Yes prf   = Yes (LTS prf)
+  _ | RTrue  yes | True  = RTrue  $ LTS yes
-  _ | No contra = No  (\case LTS p => contra p)
+  _ | 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
+data Compare : (i, j : Var n) -> Ordering -> Type where
-  IsLT : (lt : i `LT` j) -> Compare i j
+  IsLT : (lt : i `LT` j) -> Compare i j LT
-  IsEQ :                    Compare i i
+  IsEQ :                    Compare i i EQ
-  IsGT : (gt : i `GT` j) -> Compare i j
+  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
+0 compare2 : Compare {n} i j o -> o = compare i j
-compareSelf (IsLT lt) = absurd lt
+compare2 (IsLT LTZ)      = Refl
-compareSelf IsEQ      = Refl
+compare2 (IsLT (LTS lt)) = compare2 (IsLT lt)
-compareSelf (IsGT gt) = absurd gt
+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
+0 compareSelf : Compare i i o -> o = EQ
-comparePSelf i = compareSelf {}
+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
+  _ | Left  eq = Left  $ cong VS eq
-  _ | (Right lt) = Right $ LTS lt
+  _ | Right lt = Right $ LTS lt
 
+export Uninhabited (VS i `LTE` VZ) where uninhabited _ impossible
 
-export Uninhabited (VZ   = VS i) where uninhabited _ impossible
+export
-export Uninhabited (VS i = VZ)   where uninhabited _ impossible
+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) with (eqReflect i j) | (i == j)
-  eqReflect (VS i) (VS j) | r with (i == j)
+  _ | RTrue  yes | True  = RTrue  $ cong VS yes
-    eqReflect (VS i) (VS j) | RTrue  yes | True   =  RTrue  $ cong VS yes
+  _ | RFalse no  | False = RFalse $ no . injective
-    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
 
 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
+-- export
-Tighten Var where
+-- Tighten Var where
-  tighten Id       i      = pure i
+--   tighten Id       i      = pure i
-  tighten (Drop q) VZ     = empty
+--   tighten (Drop q) VZ     = empty
-  tighten (Drop q) (VS i) = tighten q i
+--   tighten (Drop q) (VS i) = tighten q i
-  tighten (Keep q) VZ     = pure VZ
+--   tighten (Keep q) VZ     = pure VZ
-  tighten (Keep q) (VS i) = VS <$> tighten q i
+--   tighten (Keep q) (VS i) = VS <$> tighten q i

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 ->
+expectPi : HasErr q m => Term q d n ->
-           m (Qty, Term d n, ScopeTerm 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 =>
+expectEqualQ : HasErr q m => Eq q =>
-               (expect, actual : Qty) -> m ()
+               (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 : IsQty q => q -> Var n -> TyContext q d n -> InferResult q d n
-lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) =
+lookupBound pi VZ ctx@(MkTyContext {tctx = _ :< ty, _}) =
-  InfRes {type = weakT ty, qout = zero :< pi}
+  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 : IsQty q => (sg : SQty q) -> q -> SQty q
-subjMult sg qty =
+subjMult sg qty = if isYes $ isZero qty then szero else sg
-  if sg == Zero || qty == Zero
+
-     then Element Zero %search
+
-     else Element One  %search
+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
+0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
-CanTC m = (MonadError Error m, MonadReader Definitions m)
+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} ->
+  check : (ctx : TyContext q d n) -> (sg : SQty q) ->
-          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
+          (subj : Term q d n) -> (ty : Term q d n) ->
-          (subj : Term d n) -> (ty : Term d n) ->
+          m (CheckResult q n)
-          m (CheckResult n)
   check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
 
   export covering %inline
-  infer : {d, n : Nat} ->
+  infer : (ctx : TyContext q d n) -> (sg : SQty q) ->
-          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
+          (subj : Elim q d n) ->
-          (subj : Elim d n) ->
+          m (InferResult q d n)
-          m (InferResult d n)
   infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
 
 
   export covering
-  check' : {d, n : Nat} ->
+  check' : (ctx : TyContext q d n) -> (sg : SQty q) ->
-           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
+           (subj : NotCloTerm q d n) -> (ty : Term q d n) ->
-           (subj : NotCloTerm d n) -> (ty : Term d n) ->
+           m (CheckResult q n)
-           m (CheckResult 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
+    expectEqualQ zero sg.fst
-    ignore $ check ctx zero arg (TYPE l)
+    ignore $ check ctx szero arg (TYPE l)
     case res of
-         TUsed   res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
+         TUsed   res =>
-         TUnused res => ignore $ check ctx                     zero res (TYPE l)
+           ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
-    pure zero
+         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)
+    ignore $ check ctx szero ty (TYPE UAny)
-    subT infres.type ty
+    subTWith (makeDimEq ctx.dctx) infres.type ty
     pure infres.qout
 
   export covering
-  infer' : {d, n : Nat} ->
+  infer' : (ctx : TyContext q d n) -> (sg : SQty q) ->
-           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
+           (subj : NotCloElim q d n) ->
-           (subj : NotCloElim d n) ->
+           m (InferResult q d n)
-           m (InferResult d n)
 
   infer' ctx sg (Element (F x) _) = do
     Just g <- asks $ lookup x  | Nothing => throwError $ NotInScope x
-    when (isZero g) $ expectEqualQ sg Zero
+    when (isZero g) $ expectEqualQ sg.fst zero
-    pure $ InfRes {type = g.type.def, qout = 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}

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 : Type -> Nat -> Nat -> Type
-TContext d = Context (Term d)
+TContext q d = Context (Term q d)
 
 public export
-QContext : Nat -> Type
+QContext : Type -> Nat -> Type
-QContext = Context' Qty
+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
+  tctx : TContext q d n
-  qctx : QContext 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
+  parameters {auto _ : IsQty q}
-  (+) : QOutput n -> QOutput n -> QOutput n
+    export
-  (+) = zipWith (+)
+    (+) : QOutput q n -> QOutput q n -> QOutput q n
+    (+) = zipWith (+)
 
-  export
+    export
-  (*) : Qty -> QOutput n -> QOutput n
+    (*) : q -> QOutput q n -> QOutput q n
-  (*) pi = map (pi *)
+    (*) pi = map (pi *)
 
-  export
+    export
-  zero : {n : Nat} -> QOutput n
+    zero : {n : Nat} -> QOutput q n
-  zero = pure Zero
+    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
+  type : Term q d n
-  qout : QOutput n
+  qout : QOutput q n
 
 
 public export
@@ -97,12 +103,16 @@ data EqMode = Equal | Sub
 
 
 public export
-data Error
+data Error q
-= ExpectedTYPE (Term d n)
+= ExpectedTYPE (Term q d n)
-| ExpectedPi   (Term d n)
+| ExpectedPi   (Term q d n)
 | BadUniverse  Universe Universe
 
-| ClashT EqMode (Term d n) (Term d n)
+| ClashT EqMode (Term q d n) (Term q d n)
-| ClashU EqMode Universe Universe
+| ClashU EqMode Universe     Universe
-| ClashQ        Qty      Qty
+| ClashQ        q            q
 | NotInScope    Name
+
+public export
+0 HasErr : Type -> (Type -> Type) -> Type
+HasErr q = MonadError (Error q)

lib/quox-lib.ipkg

@@ -9,13 +9,15 @@ depends = base, contrib, elab-util, sop, snocvect
 
 modules =
   Quox.NatExtra,
-  Quox.Unicode,
+  Quox.Decidable,
-  Quox.OPE,
+  -- 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.Token,
-  Quox.Lexer,
+  -- Quox.Lexer,
-  Quox.Parser,
+  -- Quox.Parser,
   Quox.Context,
   Quox.Equal,
   Quox.Name,

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

tests/Tests.idr

@@ -1,18 +1,18 @@
 module Tests
 
 import TAP
-import Tests.Unicode
+-- import Tests.Unicode
-import Tests.Lexer
+-- import Tests.Lexer
-import Tests.Parser
+-- import Tests.Parser
 import Tests.Reduce
 import Tests.Equal
 import System
 
 
 allTests = [
-  Unicode.tests,
+  -- Unicode.tests,
-  Lexer.tests,
+  -- Lexer.tests,
-  Parser.tests,
+  -- Parser.tests,
   Reduce.tests,
   Equal.tests
 ]

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))),
+          [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
-           ("B", 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))),
+          [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
-           ("B", MkDef Any (TYPE (U 1)) (FT "A"))]
+           ("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")))

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