box type

lib/Quox/Equal.idr

@@ -66,6 +66,8 @@ isTyCon (DLam  {}) = False
 isTyCon Nat        = True
 isTyCon Zero       = False
 isTyCon (Succ  {}) = False
+isTyCon (BOX   {}) = True
+isTyCon (Box   {}) = False
 isTyCon (E     {}) = True
 isTyCon (CloT  {}) = False
 isTyCon (DCloT {}) = False
@@ -86,6 +88,8 @@ sameTyCon (Eq   {}) (Eq   {}) = True
 sameTyCon (Eq   {}) _         = False
 sameTyCon Nat       Nat       = True
 sameTyCon Nat       _         = False
+sameTyCon (BOX  {}) (BOX  {}) = True
+sameTyCon (BOX  {}) _         = False
 sameTyCon (E    {}) (E    {}) = True
 sameTyCon (E    {}) _         = False
 
@@ -117,6 +121,8 @@ parameters (defs : Definitions' q g)
       Nat             => pure False
       Zero            => pure False
       Succ {}         => pure False
+      BOX  {ty, _}    => isSubSing ty
+      Box  {}         => pure False
       E    (s :# _)   => isSubSing s
       E    _          => pure False
 
@@ -253,6 +259,19 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           (E _,    t) => wrongType ctx Nat t
           (s,      _) => wrongType ctx Nat s
 
+      compare0' ctx ty@(BOX q ty') s t = local {mode := Equal} $
+        case (s, t) of
+          --     Γ ⊢ s = t : A
+          -- -----------------------
+          --  Γ ⊢ [s] = [t] : [π.A]
+          (Box s, Box t) => compare0 ctx ty' s t
+
+          (E e, E f) => Elim.compare0 ctx e f
+
+          (Box _, t) => wrongType ctx ty t
+          (E   _, t) => wrongType ctx ty t
+          (s,     _) => wrongType ctx ty s
+
       compare0' ctx ty@(E _) s t = do
         -- a neutral type can only be inhabited by neutral values
         -- e.g. an abstract value in an abstract type, bound variables, …
@@ -330,6 +349,10 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       --  Γ ⊢ ℕ <: ℕ
       pure ()
 
+    compareType' ctx (BOX pi a) (BOX rh b) = do
+      expectEqualQ pi rh
+      compareType ctx a b
+
     compareType' ctx (E e) (E f) = do
       -- no fanciness needed here cos anything other than a neutral
       -- has been inlined by whnf
@@ -352,6 +375,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
     computeElimType ctx (CasePair {pair, ret, _}) _ = pure $ sub1 ret pair
     computeElimType ctx (CaseEnum {tag, ret, _}) _ = pure $ sub1 ret tag
     computeElimType ctx (CaseNat {nat, ret, _}) _ = pure $ sub1 ret nat
+    computeElimType ctx (CaseBox {box, ret, _}) _ = pure $ sub1 ret box
     computeElimType ctx (f :% p) ne = do
       (ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne))
       pure $ dsub1 ty p
@@ -457,6 +481,19 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
           expectEqualQ epi' fpi'
       compare0' ctx e@(CaseNat {}) f _ _ = clashE ctx e f
 
+      compare0' ctx (CaseBox epi e eret ebody)
+                    (CaseBox fpi f fret fbody) ne nf =
+        local {mode := Equal} $ do
+          compare0 ctx e f
+          ety <- computeElimType ctx e (noOr1 ne)
+          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
+          (q, ty) <- expectBOXE defs ctx ety
+          compare0 (extendTy (epi * q) ebody.name ty ctx)
+            (substCaseBoxRet ety eret)
+            ebody.term fbody.term
+          expectEqualQ epi fpi
+      compare0' ctx e@(CaseBox {}) f _ _ = clashE ctx e f
+
       compare0' ctx (s :# a) (t :# b) _ _ =
           Term.compare0 ctx !(bigger a b) s t
         where

lib/Quox/Parser/FromParser.idr

@@ -148,6 +148,16 @@ mutual
     DLam i s =>
       DLam <$> fromPTermDScope ds ns [< i] s
 
+    BOX q ty => BOX q <$> fromPTermWith ds ns ty
+
+    Box val => Box <$> fromPTermWith ds ns val
+
+    Case pi box (r, ret) (CaseBox b body) =>
+      Prelude.map E $ CaseBox pi
+        <$> fromPTermElim ds ns box
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> fromPTermTScope ds ns [< b] body
+
     s :% p =>
       map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
 

lib/Quox/Parser/Parser.idr

@@ -204,7 +204,8 @@ mutual
     succCase = do
       resC "succ"
       n  <- bname
-      ih  <- option (Zero, Nothing) $ bracks [|MkPair qty (resC "." *> bname)|]
+      ih <- option (Zero, Nothing) $
+        resC "," *> [|MkPair qty (resC "." *> bname)|]
       rhs <- darr *> term
       pure $ (n, fst ih, snd ih, rhs)
 
@@ -263,17 +264,20 @@ mutual
   private covering
   aTerm : Grammar True PTerm
   aTerm = [|Enum $ braces $ commaSep bareTag|]
+      <|> foldr1 Pair <$> parens (commaSep1 term)
+      <|> boxTerm
       <|> [|TYPE universe|]
       <|> Nat  <$ resC "ℕ"
       <|> Zero <$ resC "zero"
       <|> (nat <&> \n => fromNat n :# Nat)
       <|> [|V name|]
       <|> [|Tag tag|]
-      <|> foldr1 Pair <$> parens (commaSep1 term)
+
-  where
+  private covering
-    fromNat : Nat -> PTerm
+  boxTerm : Grammar True PTerm
-    fromNat 0     = Zero
+  boxTerm = bracks $
-    fromNat (S k) = Succ $ fromNat k
+        [|BOX (qty <* resC ".") term|]
+    <|> [|Box term|]
 
   private covering
   optBinderTerm : Grammar True (BName, PTerm)

lib/Quox/Parser/Syntax.idr

@@ -54,6 +54,9 @@ namespace PTerm
       | Nat
       | Zero | Succ PTerm
 
+      | BOX PQty PTerm
+      | Box PTerm
+
       | V PName
       | (:#) PTerm PTerm
     %name PTerm s, t
@@ -63,6 +66,7 @@ namespace PTerm
         CasePair (BName, BName) PTerm
       | CaseEnum (List (TagVal, PTerm))
       | CaseNat PTerm (BName, PQty, BName, PTerm)
+      | CaseBox BName PTerm
     %name PCaseBody body
 
 %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show]
@@ -150,6 +154,8 @@ mutual
       Nat => Nat
       Zero => Zero
       Succ n => Succ $ toPTermWith ds ns n
+      BOX q ty => BOX q $ toPTermWith ds ns ty
+      Box val => Box $ toPTermWith ds ns val
       E e =>
         toPTermWith ds ns e
 
@@ -187,6 +193,11 @@ mutual
              (CaseNat (toPTermWith ds ns zer)
                       (Just $ baseStr p, qtyIH, Just $ baseStr ih,
                        toPTermWith ds (ns :< baseStr p :< baseStr ih) suc.term))
+      CaseBox qty box (S [< r] ret) (S [< b] body) =>
+        Case qty (toPTermWith ds ns box)
+             (Just $ baseStr r, toPTermWith ds (ns :< baseStr r) ret.term)
+             (CaseBox (Just $ baseStr b) $
+                toPTermWith ds (ns :< baseStr b) body.term)
       fun :% arg =>
         toPTermWith ds ns fun :% toPDimWith ds arg
       tm :# ty =>
@@ -201,3 +212,8 @@ namespace Elim
   export
   toPTerm : Elim Three 0 0 -> PTerm
   toPTerm = toPTermWith [<] [<]
+
+public export
+fromNat : Nat -> PTerm
+fromNat 0     = Zero
+fromNat (S k) = Succ $ fromNat k

lib/Quox/Reduce.idr

@@ -72,6 +72,11 @@ isNatHead (Zero   :# Nat) = True
 isNatHead (Succ n :# Nat) = True
 isNatHead _ = False
 
+public export %inline
+isBoxHead : Elim {} -> Bool
+isBoxHead (Box {} :# BOX {}) = True
+isBoxHead _ = False
+
 public export %inline
 isE : Term {} -> Bool
 isE (E _) = True
@@ -97,6 +102,8 @@ mutual
     isRedexE defs tag || isTagHead tag
   isRedexE defs (CaseNat {nat, _}) =
     isRedexE defs nat || isNatHead nat
+  isRedexE defs (CaseBox {box, _}) =
+    isRedexE defs box || isBoxHead box
   isRedexE defs (f :% _) =
     isRedexE defs f || isDLamHead f
   isRedexE defs (t :# a) =
@@ -120,6 +127,7 @@ mutual
 
     whnf _ (B i) = pure $ nred $ B i
 
+    -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
     whnf defs (f :@ s) = do
       Element f fnf <- whnf defs f
       case nchoose $ isLamHead f of
@@ -130,6 +138,8 @@ mutual
           whnf defs $ sub1 body s :# sub1 res s
         Right nlh => pure $ Element (f :@ s) $ fnf `orNo` nlh
 
+    -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
+    -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
     whnf defs (CasePair pi pair ret body) = do
       Element pair pairnf <- whnf defs pair
       case nchoose $ isPairHead pair of
@@ -143,6 +153,8 @@ mutual
           pure $ Element (CasePair pi pair ret body)
                          (pairnf `orNo` np)
 
+    -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
+    -- u ∷ C['a∷{a,…}/p]
     whnf defs (CaseEnum pi tag ret arms) = do
       Element tag tagnf <- whnf defs tag
       case nchoose $ isTagHead tag of
@@ -156,6 +168,11 @@ mutual
         Right nt =>
           pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
 
+    -- case zero ∷ ℕ return p ⇒ C of { zero ⇒ u; … } ⇝
+    --   u ∷ C[zero∷ℕ/p]
+    --
+    -- case succ n ∷ ℕ return p ⇒ C of { succ n' [π.ih] ⇒ u; … } ⇝
+    --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
     whnf defs (CaseNat pi piIH nat ret zer suc) = do
       Element nat natnf <- whnf defs nat
       case nchoose $ isNatHead nat of
@@ -171,6 +188,23 @@ mutual
         Right nn =>
           pure $ Element (CaseNat pi piIH nat ret zer suc) $ natnf `orNo` nn
 
+    -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
+    --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
+    whnf defs (CaseBox pi box ret body) = do
+      Element box boxnf <- whnf defs box
+      case nchoose $ isBoxHead box of
+        Left _ =>
+          let Box val :# BOX q bty = box
+              ty = sub1 ret box
+          in
+          whnf defs $ sub1 body (val :# bty) :# ty
+        Right nb =>
+          pure $ Element (CaseBox pi box ret body) $ boxnf `orNo` nb
+
+    -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @0 ⇝ t ∷ A‹0/𝑗›
+    -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗›
+    -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
+    --   (if 𝑘 is a variable)
     whnf defs (f :% p) = do
       Element f fnf <- whnf defs f
       case nchoose $ isDLamHead f of
@@ -182,6 +216,7 @@ mutual
         Right ndlh =>
           pure $ Element (f :% p) $ fnf `orNo` ndlh
 
+    -- e ∷ A ⇝ e
     whnf defs (s :# a) = do
       Element s snf <- whnf defs s
       case nchoose $ isE s of
@@ -207,7 +242,10 @@ mutual
     whnf _    Nat      = pure $ nred Nat
     whnf _    Zero     = pure $ nred Zero
     whnf _ t@(Succ {}) = pure $ nred t
+    whnf _ t@(BOX  {}) = pure $ nred t
+    whnf _ t@(Box  {}) = pure $ nred t
 
+    -- s ∷ A ⇝ s   (in term context)
     whnf defs (E e) = do
       Element e enf <- whnf defs e
       case nchoose $ isAnn e of

lib/Quox/Syntax/Term/Base.idr

@@ -81,6 +81,10 @@ mutual
     Zero : Term q d n
     Succ : (p : Term q d n) -> Term q d n
 
+    ||| "box" (package a value up with a certain quantity)
+    BOX : (qty : q) -> (ty : Term q d n) -> Term q d n
+    Box : (val : Term q d n) -> Term q d n
+
     ||| elimination
     E : (e : Elim q d n) -> Term q d n
 
@@ -124,6 +128,12 @@ mutual
               (succ : ScopeTermN 2 q d n) ->
               Elim q d n
 
+    ||| unboxing
+    CaseBox : (qty : q) -> (box : Elim q d n) ->
+              (ret : ScopeTerm q d n) ->
+              (body : ScopeTerm q d n) ->
+              Elim q d n
+
     ||| dim application
     (:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
 

lib/Quox/Syntax/Term/Pretty.idr

@@ -162,6 +162,10 @@ export
 prettyTagBare : TagVal -> Doc HL
 prettyTagBare t = hl Tag $ quoteTag t
 
+export
+prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
+prettyBoxVal val = bracks <$> pretty0M val
+
 export
 toNatLit : Term q d n -> Maybe Nat
 toNatLit Zero     = Just 0
@@ -224,6 +228,11 @@ parameters (showSubsts : Bool)
         Nothing => do
           n <- withPrec Arg $ prettyM n
           parensIfM App $ succD <++> n
+    prettyM (BOX pi ty) = do
+      pi <- pretty0M pi
+      ty <- pretty0M ty
+      pure $ bracks $ hcat [pi, dotD, align ty]
+    prettyM (Box val) = prettyBoxVal val
     prettyM (E e) = prettyM e
     prettyM (CloT s th) =
       if showSubsts then
@@ -260,8 +269,13 @@ parameters (showSubsts : Bool)
          ([< s, ih], !succPat, eterm suc.term)]
       where
         succPat : m (Doc HL)
-        succPat = pure $
+        succPat = case ih of
-          hsep [succD, !(pretty0M s), bracks !(pretty0M $ MkWithQty pi' ih)]
+          Unused => pure $ hsep [succD, !(pretty0M s)]
+          _      => pure $ sep [hsep [succD, !(pretty0M s)] <+> comma,
+                                !(pretty0M $ MkWithQty pi' ih)]
+    prettyM (CaseBox pi box (S [< r] ret) (S [< u] body)) =
+      prettyCase pi box r ret.term
+        [([< u], !(prettyBoxVal $ TV u), body.term)]
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
       prettyApps (Just "@") fun args

lib/Quox/Syntax/Term/Subst.idr

@@ -271,6 +271,8 @@ mutual
     pushSubstsWith _ _ Nat = nclo Nat
     pushSubstsWith _ _ Zero = nclo Zero
     pushSubstsWith th ph (Succ n) = nclo $ Succ $ n // th // ph
+    pushSubstsWith th ph (BOX pi ty) = nclo $ BOX pi $ ty // th // ph
+    pushSubstsWith th ph (Box val) = nclo $ Box $ val // th // ph
     pushSubstsWith th ph (E e) =
       let Element e nc = pushSubstsWith th ph e in nclo $ E e
     pushSubstsWith th ph (CloT s ps) =
@@ -297,6 +299,8 @@ mutual
     pushSubstsWith th ph (CaseNat pi pi' n r z s) =
       nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
                (z // th // ph) (s // th // ph)
+    pushSubstsWith th ph (CaseBox pi x r b) =
+      nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph)
     pushSubstsWith th ph (f :% d) =
       nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =

lib/Quox/Typechecker.idr

@@ -187,6 +187,15 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     expectNat !ask ctx ty
     checkC ctx sg n Nat
 
+  check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
+
+  check' ctx sg (Box val) ty = do
+    (q, ty) <- expectBOX !ask ctx ty
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
+    valout <- checkC ctx sg val ty
+    -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
+    pure $ q * valout
+
   check' ctx sg (E e) ty = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- inferC ctx sg e
@@ -254,14 +263,17 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   checkType' ctx Zero u = throwError $ NotType ctx Zero
   checkType' ctx t@(Succ _) u = throwError $ NotType ctx t
 
+  checkType' ctx (BOX q ty) u = checkType ctx ty u
+  checkType' ctx t@(Box _) u = throwError $ NotType ctx t
+
   checkType' ctx (E e) u = do
-    -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
+    -- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
     infres <- inferC ctx szero e
-    -- if Ψ | Γ ⊢ A' <: A
+    -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
       Just u  => subtype ctx infres.type (TYPE u)
       Nothing => ignore $ expectTYPE !ask ctx infres.type
-    -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
+    -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
 
   private covering
@@ -320,11 +332,11 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
         pisg    = pi * sg.fst
         bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
         bodyty  = substCasePairRet pairres.type ret
-    bodyout <- checkC bodyctx sg body.term bodyty
+    bodyout <- checkC bodyctx sg body.term bodyty >>= popQs [< pisg, pisg]
     -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,
-      qout = pi * pairres.qout + !(popQs [< pisg, pisg] bodyout)
+      qout = pi * pairres.qout + bodyout
     }
 
   infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do
@@ -336,8 +348,8 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
     checkTypeC (extendTy zero ret.name tres.type ctx) ret.term Nothing
     -- if for each "a ⇒ s" in arms,
-    --   Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂
+    --   Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σᵢ
-    -- for fixed Σ₂
+    -- with Σ₂ = lubs Σᵢ
     let arms = SortedMap.toList arms
     let armTags = SortedSet.fromList $ map fst arms
     unless (ttags == armTags) $ throwError $ BadCaseEnum ttags armTags
@@ -380,6 +392,24 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       qout = pi * nres.qout + armout
     }
 
+  infer' ctx sg (CaseBox pi box ret body) = do
+    -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
+    boxres <- inferC ctx sg box
+    (q, ty) <- expectBOX !ask ctx boxres.type
+    -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
+    checkTypeC (extendTy zero ret.name boxres.type ctx) ret.term Nothing
+    -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
+    --   with ς ≤ ρπσ
+    let qpisg    = q * pi * sg.fst
+        bodyCtx  = extendTy qpisg body.name boxres.type ctx
+        bodyType = substCaseBoxRet ty ret
+    bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg
+    -- then Ψ | Γ ⊢ case ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
+    pure $ InfRes {
+      type = sub1 ret box,
+      qout = boxres.qout + bodyout
+    }
+
   infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun

lib/Quox/Typing.idr

@@ -48,6 +48,10 @@ public export
 substCaseNatRet : ScopeTerm q d n -> Term q d (2 + n)
 substCaseNatRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
 
+public export
+substCaseBoxRet : Term q d n -> ScopeTerm q d n -> Term q d (S n)
+substCaseBoxRet dty retty =
+  retty.term // (Box (BVT 0) :# weakT dty ::: shift 1)
 
 parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   export covering %inline
@@ -93,6 +97,12 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
       Nat => pure ()
       _   => throwError $ ExpectedNat ctx (s // th)
 
+    export covering %inline
+    expectBOX_ : Term q d2 n -> m (q, Term q d2 n)
+    expectBOX_ s = case fst !(whnfT s) of
+      BOX q a => pure (q, a)
+      _       => throwError $ ExpectedBOX ctx (s // th)
+
 
   -- [fixme] refactor this stuff
 
@@ -133,6 +143,12 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectNat_ ctx id
 
+    export covering %inline
+    expectBOX : Term q d n -> m (q, Term q d n)
+    expectBOX =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectBOX_ ctx id
+
 
   parameters (ctx : EqContext q n)
     export covering %inline
@@ -170,3 +186,9 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
     expectNatE t =
       let Val n = ctx.termLen in
       expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t
+
+    export covering %inline
+    expectBOXE : Term q 0 n -> m (q, Term q 0 n)
+    expectBOXE t =
+      let Val n = ctx.termLen in
+      expectBOX_ (toTyContext ctx) (shift0 ctx.dimLen) t

lib/Quox/Typing/Error.idr

@@ -18,6 +18,7 @@ data Error q
 | ExpectedEnum (TyContext q d n) (Term q d n)
 | ExpectedEq   (TyContext q d n) (Term q d n)
 | ExpectedNat  (TyContext q d n) (Term q d n)
+| ExpectedBOX  (TyContext q d n) (Term q d n)
 | BadUniverse  Universe Universe
 | TagNotIn     TagVal (SortedSet TagVal)
 | BadCaseEnum  (SortedSet TagVal) (SortedSet TagVal)
@@ -208,8 +209,12 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
     ExpectedEq ctx s =>
       sep ["expected an equality type, but got", termt ctx s]
 
-    ExpectedNat ctx s =>
+    ExpectedNat ctx s {d, n} =>
-      sep ["expected the type ℕ, but got", termt ctx s]
+      sep ["expected the type", pretty0 unicode $ Nat {q, d, n},
+           "but got", termt ctx s]
+
+    ExpectedBOX ctx s =>
+      sep ["expected a box type, but got", termt ctx s]
 
     BadUniverse k l =>
       sep ["the universe level", prettyUniverse k,

tests/TermImpls.idr

@@ -60,6 +60,12 @@ mutual
     Succ m == Succ n = m == n
     Succ _ == _ = False
 
+    BOX q1 ty1 == BOX q2 ty2 = q1 == q2 && ty1 == ty2
+    BOX {} == _ = False
+
+    Box val1 == Box val2 = val1 == val2
+    Box _ == _ = False
+
     E e == E f = e == f
     E _ == _ = False
 
@@ -99,6 +105,10 @@ mutual
       r1.term == r2.term && z1 == z2 && s1.term == s2.term
     CaseNat {} == _ = False
 
+    CaseBox q1 x1 r1 b1 == CaseBox q2 x2 r2 b2 =
+      q1 == q2 && x1 == x2 && r1.term == r2.term && b1.term == b2.term
+    CaseBox {} == _ = False
+
     (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
     (_ :% _) == _ = False
 

tests/Tests/Equal.idr

@@ -500,6 +500,10 @@ tests = "equality & subtyping" :- [
   todo "enum",
   todo "enum elim",
 
+  todo "box types",
+  todo "boxes",
+  todo "box elim",
+
   "elim closure" :- [
     testEq "#0{a} = a" $
       equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"),

tests/Tests/Parser.idr

@@ -233,6 +233,14 @@ tests = "parser" :- [
     parseFails term "succ"
   ],
 
+  "box" :- [
+    parsesAs term "[1.ℕ]" $ BOX One Nat,
+    parsesAs term "[ω. ℕ × ℕ]" $ BOX Any (Sig Nothing Nat Nat),
+    parsesAs term "[a]" $ Box (V "a"),
+    parsesAs term "[0]" $ Box (Zero :# Nat),
+    parsesAs term "[1]" $ Box (Succ Zero :# Nat)
+  ],
+
   "case" :- [
     parsesAs term
       "case1 f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
@@ -264,7 +272,7 @@ tests = "parser" :- [
     parsesAs term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }" $
       Case Any (V "n") (Nothing, V "A") $
         CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"),
-    parsesAs term "caseω n return ℕ of { succ _ [1.ih] ⇒ ih; zero ⇒ 0; }" $
+    parsesAs term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }" $
       Case Any (V "n") (Nothing, Nat) $
         CaseNat (Zero :# Nat) (Nothing, One, Just "ih", V "ih"),
     parseFails term "caseω n return A of { zero ⇒ a }",

tests/Tests/Typechecker.idr

@@ -390,6 +390,31 @@ tests = "typechecker" :- [
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
   ],
 
+  "natural numbers" :- [
+    testTC "0 · ℕ ⇐ ★₀" $ check_ empty szero Nat (TYPE 0),
+    testTC "0 · ℕ ⇐ ★₇" $ check_ empty szero Nat (TYPE 7),
+    testTCFail "1 · ℕ ⇍ ★₀" $ check_ empty sone Nat (TYPE 0),
+    testTC "1 · zero ⇐ ℕ" $ check_ empty sone Zero Nat,
+    testTC "1 · zero ⇍ ℕ×ℕ" $ check_ empty sone Zero (Nat `And` Nat),
+    testTC "ω·n : ℕ ⊢ 1 · succ n ⇐ ℕ" $
+      check_ (ctx [< ("n", Nat)]) sone (Succ (BVT 0)) Nat,
+    testTC "1 · λ n ⇒ succ n ⇐ 1.ℕ → ℕ" $
+      check_ empty sone ([< "n"] :\\ Succ (BVT 0)) (Arr One Nat Nat),
+    todo "nat elim"
+  ],
+
+  "box types" :- [
+    testTC "0 · [0.ℕ] ⇐ ★₀" $
+      check_ empty szero (BOX Zero Nat) (TYPE 0),
+    testTC "0 · [0.★₀] ⇐ ★₁" $
+      check_ empty szero (BOX Zero (TYPE 0)) (TYPE 1),
+    testTCFail "0 · [0.★₀] ⇍ ★₀" $
+      check_ empty szero (BOX Zero (TYPE 0)) (TYPE 0)
+  ],
+
+  todo "box values",
+  todo "box elim",
+
   "misc" :- [
     note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
     note "⊢",