check quantites of subject and global

- subj qty must be 0 or 1 (atkey)
- global must not be 0 if used at non-0

src/Quox/Syntax/Qty.idr

@@ -70,3 +70,14 @@ IsQty Qty where
   zero  = Zero; one = One
   (+)   = plus; (*) = times
   (<=.) = compat
+
+
+public export
+data IsSubj : Qty -> Type where
+  SZero : IsSubj Zero
+  SOne  : IsSubj One
+
+public export
+data IsGlobal : Qty -> Type where
+  GZero : IsGlobal Zero
+  GAny  : IsGlobal Any

src/Quox/Typechecker.idr

@@ -38,6 +38,12 @@ tail : TyContext d (S n) -> TyContext d n
 tail = {tctx $= tail, qctx $= tail}
 
 
+private %inline
+globalSubjQty : Global -> Qty
+globalSubjQty (MkGlobal {qty = Zero, _}) = Zero
+globalSubjQty (MkGlobal {qty = Any,  _}) = One
+
+
 private %inline
 weakI : InferResult d n -> InferResult d (S n)
 weakI = {type $= weakT, qout $= (:< zero)}
@@ -50,85 +56,95 @@ lookupBound pi (VS i) ctx =
   weakI $ lookupBound pi i (tail ctx)
 
 
+private %inline
+subjMult : Qty -> Qty -> Subset Qty IsSubj
+subjMult sg qty =
+  if sg == Zero || qty == Zero
+     then Element Zero %search
+     else Element One  %search
+
+
 mutual
   -- [todo] it seems like the options here for dealing with substitutions are
   -- to either push them or parametrise the whole typechecker over ambient
   -- substitutions. both of them seem like the same amount of work for the
   -- computer but pushing is less work for the me
-  --
-  -- [todo] probably need to check that pi is 1 or 0 like atkey said
 
   export covering %inline
   check : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-          (ctx : TyContext d n) -> (pi : Qty) ->
+          (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
           (subj : Term d n) -> (ty : Term d n) ->
           m (CheckResult n)
-  check ctx pi subj ty = check' ctx pi (pushSubstsT subj) ty
+  check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
 
   export covering %inline
   infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-          (ctx : TyContext d n) -> (pi : Qty) -> (subj : Elim d n) ->
+          (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
+          (subj : Elim d n) ->
           m (InferResult d n)
-  infer ctx pi subj = infer' ctx pi (pushSubstsE subj)
+  infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
 
 
   export covering
   check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-           (ctx : TyContext d n) -> (pi : Qty) ->
+           (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
            (subj : NotCloTerm d n) -> (ty : Term d n) ->
            m (CheckResult n)
 
-  check' ctx pi (Element (TYPE l) _) ty = do
+  check' ctx sg (Element (TYPE l) _) ty = do
     l' <- expectTYPE ty
-    expectEqualQ zero pi
+    expectEqualQ zero sg
     unless (l < l') $ throw $ BadUniverse l l'
     pure zero
 
   -- [todo] factor this stuff out
-  check' ctx pi (Element (Pi qty x arg res) _) ty = do
+  check' ctx sg (Element (Pi qty x arg res) _) ty = do
     l <- expectTYPE ty
-    expectEqualQ zero pi
+    expectEqualQ zero sg
     ignore $ check ctx zero arg (TYPE l)
     case res of
          TUsed   res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
          TUnused res => ignore $ check ctx                     zero res (TYPE l)
     pure zero
 
-  check' ctx pi (Element (Lam x body) _) ty = do
+  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 (pi * qty) ctx) pi body res
+    qout <- check (extendTy arg (sg * qty) ctx) sg body res
     popQ qty qout
 
-  check' ctx pi (Element (E e) _) ty = do
-    infres <- infer ctx pi e
+  check' ctx sg (Element (E e) _) ty = do
+    infres <- infer ctx sg e
     ignore $ check ctx zero ty (TYPE UAny)
     infres.type `subT` ty
     pure infres.qout
 
   export covering
   infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-           (ctx : TyContext d n) -> (pi : Qty) -> (subj : NotCloElim d n) ->
+           (ctx : TyContext d n) -> (sg : Qty) -> {auto 0 sgs : IsSubj sg} ->
+           (subj : NotCloElim d n) ->
            m (InferResult d n)
 
-  infer' ctx pi (Element (F x) _) =
-    -- [todo] check that global is erased ==> pi = zero
+  infer' ctx sg (Element (F x) _) =
     case lookup x ctx.globals of
-         Just g  => pure $ InfRes {type = g.type, qout = zero}
+         Just g => do
+           expectEqualQ (globalSubjQty g) sg
+           pure $ InfRes {type = g.type, qout = zero}
          Nothing => throw $ NotInScope x
 
-  infer' ctx pi (Element (B i) _) =
-    pure $ lookupBound pi i ctx
+  infer' ctx sg (Element (B i) _) =
+    pure $ lookupBound sg i ctx
 
-  infer' ctx pi (Element (fun :@ arg) _) = do
-    funres <- infer ctx pi fun
+  infer' ctx sg (Element (fun :@ arg) _) = do
+    funres <- infer ctx sg fun
     (qty, argty, res) <- expectPi funres.type
-    argout <- check ctx (pi * qty) arg argty
+    let Element sg' _ = subjMult sg qty
+    argout <- check ctx sg' arg argty
     pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
                    qout = funres.qout + argout}
 
-  infer' ctx pi (Element (tm :# ty) _) = do
+  infer' ctx sg (Element (tm :# ty) _) = do
     ignore $ check ctx zero ty (TYPE UAny)
-    qout <- check ctx pi tm ty
+    qout <- check ctx sg tm ty
     pure $ InfRes {type = ty, qout}

src/Quox/Typing.idr

@@ -34,7 +34,9 @@ QOutput = QContext
 public export
 record Global where
   constructor MkGlobal
-  type, term : forall d, n. Term d n
+  qty         : Qty
+  0 qtyGlobal : IsGlobal qty
+  type, term  : forall d, n. Term d n
 
 public export
 Globals : Type