remove inject stuff

injecting from m to (n+m) is just id ::: id ::: ... ::: shift n.
specifically, injecting from 0 is just the shift. so.

lib/Quox/Definition.idr

@@ -7,71 +7,57 @@ import public Control.Monad.Reader
 import Decidable.Decidable
 
 
-public export
-record AnyTerm q where
-  constructor T
-  get : forall d, n. Term q d n
-
-
 public export
 data DefBody q =
-    Concrete (AnyTerm q)
+    Concrete (Term q 0 0)
   | Postulate
 
+namespace DefBody
+  public export
+  (.term0) : DefBody q -> Maybe (Term q 0 0)
+  (Concrete t).term0 = Just t
+  (Postulate).term0  = Nothing
+
+
 public export
 record Definition' q (isGlobal : Pred q) where
   constructor MkDef
-  qty  : q
+  qty   : q
-  type : AnyTerm q
+  type0 : Term q 0 0
-  body : DefBody q
+  body0 : DefBody q
   {auto 0 qtyGlobal : isGlobal qty}
 
 public export
 0 Definition : (q : Type) -> IsQty q => Type
 Definition q = Definition' q IsGlobal
 
-public export %inline
-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, body = Concrete (T term)}
-
 public export %inline
 mkPostulate : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
-             (type : forall d, n. Term q d n) -> Definition q
+             (type0 : Term q 0 0) -> Definition q
-mkPostulate qty type = MkDef {qty, type = T type, body = Postulate}
+mkPostulate qty type0 = MkDef {qty, type0, body0 = Postulate}
 
 public export %inline
-mkDef0 : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
+mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
-         (type, term : Term q 0 0) -> Definition q
+        (type0, term0 : Term q 0 0) -> Definition q
-mkDef0 qty type term = mkDef qty (inject type) (inject term)
+mkDef qty type0 term0 = MkDef {qty, type0, body0 = Concrete term0}
 
 
-public export %inline
-(.get0) : AnyTerm q -> Term q 0 0
-t.get0 = t.get
-
-public export %inline
-(.type0) : Definition' q _ -> Term q 0 0
-g.type0 = g.type.get
-
-public export %inline
-(.term) : Definition' q _ -> Maybe (AnyTerm q)
-g.term = case g.body of
-  Concrete t => Just t
-  Postulate  => Nothing
-
-public export %inline
-(.term0) : Definition' q _ -> Maybe (Term q 0 0)
-g.term0 = map (\x => x.get) g.term
-
 public export %inline
 (.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
 g.qtyP = Element g.qty g.qtyGlobal
 
+parameters {d, n : Nat}
+  public export %inline
+  (.type) : Definition' q _ -> Term q d n
+  g.type = g.type0 // shift0 d // shift0 n
 
-public export %inline
+  public export %inline
-toElim : Definition' q _ -> Maybe $ Elim q d n
+  (.term) : Definition' q _ -> Maybe (Term q d n)
-toElim def = pure $ (!def.term).get :# def.type.get
+  g.term = g.body0.term0 <&> \t => t // shift0 d // shift0 n
+
+  public export %inline
+  toElim : Definition' q _ -> Maybe $ Elim q d n
+  toElim def = pure $ !def.term :# def.type
 
 
 public export
@@ -102,6 +88,6 @@ HasDefs q = HasDefs' q IsGlobal
 
 
 public export %inline
-lookupElim : forall isGlobal.
+lookupElim : forall isGlobal. {d, n : Nat} ->
              Name -> Definitions' q isGlobal -> Maybe (Elim q d n)
 lookupElim x defs = toElim !(lookup x defs)

lib/Quox/Equal.idr

@@ -90,7 +90,7 @@ parameters (defs : Definitions' q g)
   |||   boundary separation.
   ||| * an enum type is a subsingleton if it has zero or one tags.
   public export
-  isSubSing : HasErr q m => Term q 0 n -> m Bool
+  isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool
   isSubSing ty = do
     Element ty nc <- whnfT defs ty
     case ty of
@@ -125,6 +125,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> m ()
       compare0 ctx ty s t =
         wrapErr (WhileComparingT ctx !mode ty s t) $ do
+          let Val n = ctx.termLen
           Element ty nty <- whnfT defs ty
           Element s  ns  <- whnfT defs s
           Element t  nt  <- whnfT defs t
@@ -219,6 +220,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
     export covering %inline
     compareType : EqContext q n -> (s, t : Term q 0 n) -> m ()
     compareType ctx s t = do
+      let Val n = ctx.termLen
       Element s ns <- whnfT defs s
       Element t nt <- whnfT defs t
       ts <- ensureTyCon ctx s
@@ -292,7 +294,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
                       m (Term q 0 n)
     computeElimType ctx (F x) _ = do
       defs <- lookupFree' defs x
-      pure $ defs.type.get
+      pure $ injectT ctx defs.type
     computeElimType ctx (B i) _ = do
       pure $ ctx.tctx !! i
     computeElimType ctx (f :@ s) ne = do
@@ -328,6 +330,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       compare0 : EqContext q n -> (e, f : Elim q 0 n) -> m ()
       compare0 ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
+          let Val n = ctx.termLen
           Element e ne <- whnfT defs e
           Element f nf <- whnfT defs f
           -- [fixme] there is a better way to do this "isSubSing" stuff for sure

lib/Quox/Parser/FromParser.idr

@@ -220,11 +220,11 @@ fromPDef (MkPDef qty pname ptype pterm) = do
     Just type => do
       injTC $ checkTypeC empty type Nothing
       injTC $ ignore $ checkC empty sqty term type
-      modify $ insert name $ mkDef0 qty type term
+      modify $ insert name $ mkDef qty type term
     Nothing => do
       let E elim = term | _ => throwError $ AnnotationNeeded pterm
       res <- injTC $ inferC empty sqty elim
-      modify $ insert name $ mkDef0 qty res.type term
+      modify $ insert name $ mkDef qty res.type term
 
 export
 fromPDecl : FromParser m => PDecl -> m ()

lib/Quox/Reduce.idr

@@ -18,12 +18,12 @@ data WhnfError = MissingEnumArm TagVal (List TagVal)
 
 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = forall q, d, n, g. Definitions' q g -> tm q d n -> Bool
+RedexTest tm = forall q, g. {d, n : Nat} -> Definitions' q g -> tm q d n -> Bool
 
 public export
 interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) (0 err : Type) | tm
 where
-  whnf : (defs : Definitions' q g) ->
+  whnf : {d, n : Nat} -> (defs : Definitions' q g) ->
          tm q d n -> Either err (Subset (tm q d n) (No . isRedex defs))
 
 public export

lib/Quox/Syntax/Dim.idr

@@ -84,11 +84,6 @@ prettyDSubst th =
 public export FromVar Dim where fromVar = B
 
 
-export
-inject : Dim d -> Dim (d + i)
-inject (K e) = K e
-inject (B i) = B $ inject i
-
 export
 CanShift Dim where
   K e // _  = K e

lib/Quox/Syntax/Shift.idr

@@ -120,21 +120,6 @@ ssDownViaNat by =
 %transform "Shift.ssDown" ssDown = ssDownViaNat
 
 
-public export
-inject : Shift from to -> Shift (from + n') (to + n')
-inject SZ      = SZ
-inject (SS by) = SS (inject by)
-
-public export
-injectViaNat : Shift from to -> Shift (from + n') (to + n')
-injectViaNat by =
-  rewrite shiftDiff by in
-  rewrite sym $ plusAssociative by.nat from n' in
-  fromNat by.nat
-
-%transform "Shift.inject" Shift.inject = Shift.injectViaNat
-
-
 public export
 shift : Shift from to -> Var from -> Var to
 shift SZ      i = i

lib/Quox/Syntax/Term/Subst.idr

@@ -299,77 +299,3 @@ mutual
       pushSubstsWith th (comp th ps ph) e
     pushSubstsWith th ph (DCloE e ps) =
       pushSubstsWith (ps . th) ph e
-
-
-parameters {0 d', n' : Nat}
- mutual
-  namespace Term
-    export
-    inject : Term q d n -> Term q (d + d') (n + n')
-    inject (TYPE l) = TYPE l
-    inject (Pi qty arg res) = Pi qty (inject arg) (inject res)
-    inject (Lam body) = Lam (inject body)
-    inject (Sig fst snd) = Sig (inject fst) (inject snd)
-    inject (Pair fst snd) = Pair (inject fst) (inject snd)
-    inject (Enum cases) = Enum cases
-    inject (Tag tag) = Tag tag
-    inject (Eq ty l r) = Eq (inject ty) (inject l) (inject r)
-    inject (DLam body) = DLam (inject body)
-    inject (E e) = E (inject e)
-    inject (CloT tm th) = CloT (inject tm) (inject th)
-    inject (DCloT tm th) = DCloT (inject tm) (inject th)
-
-  namespace Elim
-    export
-    inject : Elim q d n -> Elim q (d + d') (n + n')
-    inject (F x) = F x
-    inject (B i) = B $ inject i
-    inject (fun :@ arg) = (inject fun) :@ (inject arg)
-    inject (CasePair qty pair ret body) =
-      CasePair qty (inject pair) (inject ret) (inject body)
-    inject (CaseEnum qty tag ret arms) =
-      CaseEnum qty (inject tag) (inject ret)
-        (assert_total $ map inject arms)
-    inject (fun :% arg) = (inject fun) :% (inject arg)
-    inject (tm :# ty) = (inject tm) :# (inject ty)
-    inject (CloE el th) = CloE (inject el) (inject th)
-    inject (DCloE el th) = DCloE (inject el) (inject th)
-
-  namespace ScopeTerm
-    export
-    inject : ScopeTermN s q d n -> ScopeTermN s q (d + d') (n + n')
-    inject (S names (N body)) = S names (N (inject body))
-    inject (S names (Y body)) {s, n} =
-      S names $ Y $ rewrite plusAssociative s n n' in inject body
-
-  namespace DScopeTerm
-    export
-    inject : DScopeTermN s q d n -> DScopeTermN s q (d + d') (n + n')
-    inject (S names (N body)) = S names (N (inject body))
-    inject (S names (Y body)) {s, d} =
-      S names $ Y $ rewrite plusAssociative s d d' in inject body
-
-  namespace TSubst
-    export
-    inject : TSubst q d from to -> TSubst q (d + d') (from + n') (to + n')
-    inject (Shift by) = Shift $ inject by
-    inject (t ::: th) = inject t ::: inject th
-
-  namespace DSubst
-    export
-    inject : DSubst from to -> DSubst (from + d') (to + d')
-    inject (Shift by) = Shift $ inject by
-    inject (p ::: th) = inject p ::: inject th
-
-
--- [fixme]
--- Error: Linearity checking failed on metavar Quox.Syntax.Term.Subst.{b:7362}
--- (Int not a function type)
-{-
-%transform "Term.inject" Term.inject t = believe_me t
-%transform "Elim.inject" Elim.inject e = believe_me e
-%transform "ScopeTerm.inject" ScopeTerm.inject t = believe_me t
-%transform "DScopeTerm.inject" DScopeTerm.inject t = believe_me t
-%transform "TSubst.inject" TSubst.inject th = believe_me th
-%transform "DSubst.inject" DSubst.inject th = believe_me th
--}

lib/Quox/Syntax/Var.idr

@@ -116,18 +116,6 @@ toFromNat 0     (LTESucc x) = Refl
 toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
-export
-inject : Var m -> Var (m + i)
-inject VZ     = VZ
-inject (VS i) = VS $ inject i
-
-private
-injectViaNat : Var m -> Var (m + n)
-injectViaNat i = fromNatWith i.nat (toNatLT i `transitive` lteAddRight m)
-
-%transform "Var.inject" Var.inject = injectViaNat
-
-
 -- not using %transform like other things because weakSpec requires the proof
 -- to be relevant. but since only `LTESucc` is ever possible that seems
 -- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?

lib/Quox/Typechecker.idr

@@ -250,7 +250,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if σ ≤ π
     expectCompatQ sg.fst g.qty
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
-    pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
+    pure $ InfRes {type = injectT ctx g.type, qout = zeroFor ctx}
    where
     lookupFree : Name -> m (Definition q)
     lookupFree x = lookupFree' !ask x

lib/Quox/Typing.idr

@@ -48,10 +48,11 @@ substCasePairRet dty retty =
 parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   export covering %inline
   whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
-          tm q d n -> m (NonRedex tm q d n defs)
+          {d, n : Nat} -> tm q d n -> m (NonRedex tm q d n defs)
   whnfT = either (throwError . WhnfError) pure . whnf defs
 
-  parameters (ctx : Lazy (TyContext q d1 n)) (th : Lazy (DSubst d2 d1))
+  parameters {d2, n : Nat} (ctx : Lazy (TyContext q d1 n))
+             (th : Lazy (DSubst d2 d1))
     export covering %inline
     expectTYPE_ : Term q d2 n -> m Universe
     expectTYPE_ s = case fst !(whnfT s) of
@@ -88,42 +89,62 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   parameters (ctx : TyContext q d n)
     export covering %inline
     expectTYPE : Term q d n -> m Universe
-    expectTYPE = expectTYPE_ ctx id
+    expectTYPE =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectTYPE_ ctx id
 
     export covering %inline
     expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
-    expectPi = expectPi_ ctx id
+    expectPi =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectPi_ ctx id
 
     export covering %inline
     expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
-    expectSig = expectSig_ ctx id
+    expectSig =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectSig_ ctx id
 
     export covering %inline
     expectEnum : Term q d n -> m (SortedSet TagVal)
-    expectEnum = expectEnum_ ctx id
+    expectEnum =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectEnum_ ctx id
 
     export covering %inline
     expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
-    expectEq = expectEq_ ctx id
+    expectEq =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectEq_ ctx id
 
 
   parameters (ctx : EqContext q n)
     export covering %inline
     expectTYPEE : Term q 0 n -> m Universe
-    expectTYPEE t = expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectTYPEE t =
+      let Val n = ctx.termLen in
+      expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectPiE : Term q 0 n -> m (q, Term q 0 n, ScopeTerm q 0 n)
-    expectPiE t = expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectPiE t =
+      let Val n = ctx.termLen in
+      expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectSigE : Term q 0 n -> m (Term q 0 n, ScopeTerm q 0 n)
-    expectSigE t = expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectSigE t =
+      let Val n = ctx.termLen in
+      expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectEnumE : Term q 0 n -> m (SortedSet TagVal)
-    expectEnumE t = expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectEnumE t =
+      let Val n = ctx.termLen in
+      expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
     expectEqE : Term q 0 n -> m (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
-    expectEqE t = expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectEqE t =
+      let Val n = ctx.termLen in
+      expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t

lib/Quox/Typing/Context.idr

@@ -3,6 +3,7 @@ module Quox.Typing.Context
 import Quox.Syntax
 import Quox.Context
 import Quox.Pretty
+import public Data.Singleton
 
 %default total
 
@@ -27,6 +28,8 @@ DimAssign = Context' DimConst
 public export
 record TyContext q d n where
   constructor MkTyContext
+  {auto dimLen  : Singleton d}
+  {auto termLen : Singleton n}
   dctx   : DimEq d
   dnames : NContext d
   tctx   : TContext q d n
@@ -39,6 +42,7 @@ public export
 record EqContext q n where
   constructor MkEqContext
   {dimLen : Nat}
+  {auto termLen : Singleton n}
   dassign : DimAssign dimLen -- only used for printing
   dnames  : NContext dimLen -- only used for printing
   tctx    : TContext q 0 n
@@ -56,6 +60,11 @@ namespace TContext
   zeroFor : IsQty q => Context tm n -> QOutput q n
   zeroFor ctx = zero <$ ctx
 
+private
+extendLen : Telescope a from to -> Singleton from -> Singleton to
+extendLen [<]        x = x
+extendLen (tel :< _) x = [|S $ extendLen tel x|]
+
 namespace TyContext
   public export %inline
   empty : TyContext q 0 0
@@ -65,9 +74,15 @@ namespace TyContext
   export %inline
   extendTyN : Telescope (\n => (q, BaseName, Term q d n)) from to ->
               TyContext q d from -> TyContext q d to
-  extendTyN xss ctx =
+  extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
-    {qtys $= (. qs), tctx $= (. ss), tnames $= (. xs)} ctx
+    MkTyContext {
+      dctx, dnames,
+      termLen = extendLen xss termLen,
+      tctx    = tctx . ss,
+      tnames  = tnames . xs,
+      qtys    = qtys . qs
+    }
 
   export %inline
   extendTy : q -> BaseName -> Term q d n -> TyContext q d n ->
@@ -76,11 +91,28 @@ namespace TyContext
 
   export %inline
   extendDim : BaseName -> TyContext q d n -> TyContext q (S d) n
-  extendDim x = {dctx $= (:<? Nothing), dnames $= (:< x), tctx $= pushD}
+  extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
+    MkTyContext {
+      dctx   = dctx :<? Nothing,
+      dnames = dnames :< x,
+      dimLen = [|S dimLen|],
+      tctx   = pushD tctx,
+      tnames, qtys
+    }
 
   export %inline
   eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
-  eqDim p q = {dctx $= set p q}
+  eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}
+
+  export
+  injectT : TyContext q d n -> Term q 0 0 -> Term q d n
+  injectT (MkTyContext {dimLen = Val d, termLen = Val n, _}) tm =
+    tm // shift0 d // shift0 n
+
+  export
+  injectE : TyContext q d n -> Elim q 0 0 -> Elim q d n
+  injectE (MkTyContext {dimLen = Val d, termLen = Val n, _}) el =
+    el // shift0 d // shift0 n
 
 
 namespace QOutput
@@ -106,6 +138,7 @@ makeDAssign (K e ::: th) = makeDAssign th :< e
 export
 makeEqContext' : {d : Nat} -> TyContext q d n -> DSubst d 0 -> EqContext q n
 makeEqContext' ctx th = MkEqContext {
+  termLen = ctx.termLen,
   dassign = makeDAssign th,
   dnames  = ctx.dnames,
   tctx    = map (// th) ctx.tctx,
@@ -128,9 +161,15 @@ namespace EqContext
   export %inline
   extendTyN : Telescope (\n => (q, BaseName, Term q 0 n)) from to ->
               EqContext q from -> EqContext q to
-  extendTyN tel ctx =
+  extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
-    let (qs, xs, ss) = unzip3 tel in
+    let (qs, xs, ss) = unzip3 xss in
-    {qtys $= (. qs), tctx $= (. ss), tnames $= (. xs)} ctx
+    MkEqContext {
+      termLen = extendLen xss termLen,
+      tctx    = tctx . ss,
+      tnames  = tnames . xs,
+      qtys    = qtys . qs,
+      dassign, dnames
+    }
 
   export %inline
   extendTy : q -> BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n)
@@ -138,7 +177,9 @@ namespace EqContext
 
   export %inline
   extendDim : BaseName -> DimConst -> EqContext q n -> EqContext q n
-  extendDim x e ctx = {dassign $= (:< e), dnames $= (:< x)} ctx
+  extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
+    MkEqContext {dassign = dassign :< e, dnames = dnames :< x,
+                 tctx, tnames, qtys}
 
   export
   toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n
@@ -149,6 +190,14 @@ namespace EqContext
       dnames, tnames, qtys
     }
 
+  export
+  injectT : EqContext q n -> Term q 0 0 -> Term q 0 n
+  injectT (MkEqContext {termLen = Val n, _}) tm = tm // shift0 n
+
+  export
+  injectE : EqContext q n -> Elim q 0 0 -> Elim q 0 n
+  injectE (MkEqContext {termLen = Val n, _}) el = el // shift0 n
+
 
 parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
   private

tests/Tests/Equal.idr

@@ -47,7 +47,7 @@ parameters (ctx : TyContext Three 0 n)
   equalE = equalED 0 ctx
 
 empty01 : TyContext q 0 0
-empty01 = {dctx := ZeroIsOne} empty
+empty01 = eqDim (K Zero) (K One) empty
 
 
 export

tests/Tests/Typechecker.idr

@@ -110,7 +110,7 @@ ctx01 tel = let (ns, ts) = unzip tel in
             MkTyContext ZeroIsOne [<] ts ns anys
 
 empty01 : TyContext Three 0 0
-empty01 = {dctx := ZeroIsOne} empty
+empty01 = eqDim (K Zero) (K One) empty
 
 inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
 inferredTypeEq ctx exp got =