From a42e82c3554bca4517eecaf5d8963aebc8b96c7d Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 3 Apr 2023 17:46:23 +0200
Subject: [PATCH] type-case

---
 lib/Quox/Equal.idr              | 78 +++++++++++++++------------
 lib/Quox/Parser/Syntax.idr      | 12 +++--
 lib/Quox/Reduce.idr             | 96 +++++++++++++++++++++++++++++++++
 lib/Quox/Syntax/Term/Base.idr   | 12 +++++
 lib/Quox/Syntax/Term/Pretty.idr | 60 +++++++++++++++------
 lib/Quox/Syntax/Term/Subst.idr  |  6 +++
 lib/Quox/Typechecker.idr        | 73 +++++++++++++++++++++----
 lib/Quox/Typing.idr             |  7 +--
 lib/Quox/Typing/Context.idr     | 29 +++-------
 tests/TermImpls.idr             | 13 +++++
 tests/Tests/PrettyTerm.idr      | 33 +++++++++++-
 tests/Tests/Typechecker.idr     |  8 +++
 12 files changed, 334 insertions(+), 93 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index e23dde2..8070a13 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -48,34 +48,9 @@ parameters (ctx : EqContext n)
   wrongType ty s = throw $ WrongType ctx ty s
 
 
-||| true if a term is syntactically a type, or is neutral.
-|||
-||| this function *doesn't* push substitutions, because its main use is as a
-||| `So` argument to skip cases that are already known to be nonsense. and
-||| the substitutions have already been pushed.
-public export %inline
-isTyCon : (t : Term {}) -> Bool
-isTyCon (TYPE  {}) = True
-isTyCon (Pi    {}) = True
-isTyCon (Lam   {}) = False
-isTyCon (Sig   {}) = True
-isTyCon (Pair  {}) = False
-isTyCon (Enum  {}) = True
-isTyCon (Tag   {}) = False
-isTyCon (Eq    {}) = True
-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
-
 public export %inline
 sameTyCon : (s, t : Term d n) ->
-            (0 ts : So (isTyCon s)) => (0 tt : So (isTyCon t)) =>
+            (0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) =>
             Bool
 sameTyCon (TYPE {}) (TYPE {}) = True
 sameTyCon (TYPE {}) _         = False
@@ -132,8 +107,8 @@ parameters (defs : Definitions)
 export
 ensureTyCon : Has ErrorEff fs =>
               (ctx : EqContext n) -> (t : Term 0 n) ->
-              Eff fs (So (isTyCon t))
-ensureTyCon ctx t = case nchoose $ isTyCon t of
+              Eff fs (So (isTyConE t))
+ensureTyCon ctx t = case nchoose $ isTyConE t of
   Left  y => pure y
   Right n => throw $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
 
@@ -164,7 +139,7 @@ parameters (defs : Definitions)
       private covering
       compare0' : EqContext n ->
                   (ty, s, t : Term 0 n) ->
-                  (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
+                  (0 nty : NotRedex defs ty) => (0 tty : So (isTyConE ty)) =>
                   (0 ns  : NotRedex defs s)  => (0 nt  : NotRedex defs t) =>
                   Equal ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
@@ -298,8 +273,8 @@ parameters (defs : Definitions)
 
     private covering
     compareType' : EqContext n -> (s, t : Term 0 n) ->
-                   (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
-                   (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
+                   (0 ns : NotRedex defs s) => (0 ts : So (isTyConE s)) =>
+                   (0 nt : NotRedex defs t) => (0 tt : So (isTyConE t)) =>
                    (0 st : So (sameTyCon s t)) =>
                    Equal ()
     -- equality is the same as subtyping, except with the
@@ -369,8 +344,9 @@ parameters (defs : Definitions)
                       (0 ne : NotRedex defs e) ->
                       Equal (Term 0 n)
     computeElimType ctx (F x) _ = do
-      defs <- lookupFree' defs x
-      pure $ injectT ctx defs.type
+      def <- lookupFree x defs
+      let Val n = ctx.termLen
+      pure $ def.type
     computeElimType ctx (B i) _ = pure $ ctx.tctx !! i
     computeElimType ctx (f :@ s) ne = do
       (_, arg, res) <- expectPiE defs ctx !(computeElimType ctx f (noOr1 ne))
@@ -382,6 +358,7 @@ parameters (defs : Definitions)
     computeElimType ctx (f :% p) ne = do
       (ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne))
       pure $ dsub1 ty p
+    computeElimType ctx (TypeCase {ret, _}) _ = pure ret
     computeElimType ctx (_ :# ty) _ = pure ty
 
     private covering
@@ -503,6 +480,41 @@ parameters (defs : Definitions)
           bigger : forall a. a -> a -> Equal a
           bigger l r = mode <&> \case Super => l; _ => r
 
+      compare0' ctx (TypeCase ty1 ret1 univ1 pi1 sig1 enum1 eq1 nat1 box1)
+                    (TypeCase ty2 ret2 univ2 pi2 sig2 enum2 eq2 nat2 box2)
+                    ne _ =
+        local_ Equal $ do
+          compare0 ctx ty1 ty2
+          u <- expectTYPEE defs ctx =<< computeElimType ctx ty1 (noOr1 ne)
+          compareType ctx ret1 ret2
+          compare0 ctx univ1 univ2 ret1
+          let [< piA, piB] = pi1.names
+              piCtx = extendTyN
+                [< (Zero, piA, TYPE u),
+                   (Zero, piB, Arr Zero (BVT 0) (TYPE u))] ctx
+              ret1_2 = weakT ret1 {by = 2}
+          compare0 piCtx pi1.term  pi2.term  ret1_2
+          let [< sigA, sigB] = sig1.names
+              sigCtx = extendTyN
+                [< (Zero, sigA, TYPE u),
+                   (Zero, sigB, Arr Zero (BVT 0) (TYPE u))] ctx
+          compare0 sigCtx sig1.term sig2.term ret1_2
+          compare0 ctx enum1 enum2 ret1
+          let [< eqA0, eqA1, eqA, eqL, eqR] = eq1.names
+              eqCtx = extendTyN
+                [< (Zero, eqA0, TYPE u),
+                   (Zero, eqA1, TYPE u),
+                   (Zero, eqA,  Eq0 (TYPE u) (BVT 1) (BVT 0)),
+                   (Zero, eqL,  BVT 2),
+                   (Zero, eqR,  BVT 2)] ctx
+              ret1_5 = weakT ret1 {by = 5}
+          compare0 eqCtx eq1.term eq2.term ret1_5
+          compare0 ctx nat1 nat2 ret1
+          let boxCtx = extendTy Zero box1.name (TYPE u) ctx
+              ret1_1 = weakT ret1
+          compare0 boxCtx box1.term box2.term ret1_1
+      compare0' ctx e@(TypeCase {}) f _ _ = clashE ctx e f
+
       compare0' ctx   (s :# a) f        _ _ = Term.compare0 ctx a s (E f)
       compare0' ctx e          (t :# b) _ _ = Term.compare0 ctx b (E e) t
       compare0' ctx e@(_ :# _) f        _ _ = clashE ctx e f
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index 1be0b11..1b2d78f 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -107,7 +107,13 @@ export
 toPDim : Dim 0 -> PDim
 toPDim = toPDimWith [<]
 
+public export
+fromNat : Nat -> PTerm
+fromNat 0     = Zero
+fromNat (S k) = Succ $ fromNat k
 
+
+{-
 mutual
   namespace Term
     export
@@ -207,8 +213,4 @@ namespace Elim
   export
   toPTerm : Elim 0 0 -> PTerm
   toPTerm = toPTermWith [<] [<]
-
-public export
-fromNat : Nat -> PTerm
-fromNat 0     = Zero
-fromNat (S k) = Succ $ fromNat k
+-}
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 7c0a7a8..8268032 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -86,6 +86,38 @@ isAnn : Elim {} -> Bool
 isAnn (_ :# _) = True
 isAnn _        = False
 
+||| true if a term is syntactically a type.
+public export %inline
+isTyCon : (t : Term {}) -> Bool
+isTyCon (TYPE  {}) = True
+isTyCon (Pi    {}) = True
+isTyCon (Lam   {}) = False
+isTyCon (Sig   {}) = True
+isTyCon (Pair  {}) = False
+isTyCon (Enum  {}) = True
+isTyCon (Tag   {}) = False
+isTyCon (Eq    {}) = True
+isTyCon (DLam  {}) = False
+isTyCon Nat        = True
+isTyCon Zero       = False
+isTyCon (Succ  {}) = False
+isTyCon (BOX   {}) = True
+isTyCon (Box   {}) = False
+isTyCon (E     {}) = False
+isTyCon (CloT  {}) = False
+isTyCon (DCloT {}) = False
+
+||| true if a term is syntactically a type, or a neutral.
+public export %inline
+isTyConE : (t : Term {}) -> Bool
+isTyConE s = isTyCon s || isE s
+
+||| true if a term is syntactically a type.
+public export %inline
+isAnnTyCon : (t : Elim {}) -> Bool
+isAnnTyCon (ty :# TYPE _) = isTyCon ty
+isAnnTyCon _              = False
+
 
 mutual
   public export
@@ -107,6 +139,8 @@ mutual
     isRedexE defs f || isDLamHead f
   isRedexE defs (t :# a) =
     isE t || isRedexT defs t || isRedexT defs a
+  isRedexE defs (TypeCase {ty, _}) =
+    isRedexE defs ty || isAnnTyCon ty
   isRedexE _ (CloE  {}) = True
   isRedexE _ (DCloE {}) = True
 
@@ -224,6 +258,68 @@ mutual
           Element a anf <- whnf defs a
           pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf
 
+    -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
+    --
+    -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
+    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
+    --
+    -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
+    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
+    --
+    -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
+    --
+    -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q of {
+    --     Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
+    -- s[(A‹0/i› ∷ ★ᵢ)/a₀, (A‹1/i› ∷ ★ᵢ)/a₁,
+    --   ((δ i ⇒ A) ∷ Eq [★ᵢ] A‹0/i› A‹1/i›)/a,
+    --   (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
+    --
+    -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
+    --
+    -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
+    whnf defs (TypeCase {ty, ret, univ, pi, sig, enum, eq, nat, box}) = do
+      Element ty tynf <- whnf defs ty
+      case nchoose $ isAnnTyCon ty of
+        Left y =>
+          let ty :# TYPE u = ty in
+          case ty of
+            TYPE _ =>
+              whnf defs $ univ :# ret
+            Pi _ arg res =>
+              let arg = arg :# TYPE u
+                  res = toLam res :# Arr Zero (TYPE u) (TYPE u)
+              in
+              whnf defs $ subN pi [< arg, res] :# ret
+            Sig fst snd =>
+              let fst = fst :# TYPE u
+                  snd = toLam snd :# Arr Zero (TYPE u) (TYPE u)
+              in
+              whnf defs $ subN sig [< fst, snd] :# ret
+            Enum _ =>
+              whnf defs $ enum :# ret
+            Eq a l r =>
+              let a0' = a.zero; a1' = a.one
+                  a0 = a0' :# TYPE u
+                  a1 = a1' :# TYPE u
+                  a  = toDLam a :# Eq0 (TYPE u) a0' a1'
+                  l  = l :# a0'
+                  r  = r :# a1'
+              in
+              whnf defs $ subN eq [< a0, a1, a, l, r] :# ret
+            Nat =>
+              whnf defs $ nat :# ret
+            BOX _ s =>
+              whnf defs $ sub1 box (s :# TYPE u) :# ret
+        Right nt => pure $
+          Element (TypeCase {ty, ret, univ, pi, sig, enum, eq, nat, box}) $
+            tynf `orNo` nt
+    where
+      toLam : {s : Nat} -> ScopeTermN s d n -> Term d n
+      toLam (S names body) = names :\\ body.term
+
+      toDLam : {s : Nat} -> DScopeTermN s d n -> Term d n
+      toDLam (S names body) = names :\\% body.term
+
     whnf defs (CloE  el th) = whnf defs $ pushSubstsWith' id th el
     whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el
 
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index be74c2a..9e06b60 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -138,6 +138,18 @@ mutual
     ||| type-annotated term
     (:#) : (tm, ty : Term d n) -> Elim d n
 
+    ||| match on types (needed for coercions :mario_flop:)
+    TypeCase : (ty   : Elim d n) ->
+               (ret  : Term d n) ->
+               (univ : Term d n) ->
+               (pi   : ScopeTermN 2 d n) ->
+               (sig  : ScopeTermN 2 d n) ->
+               (enum : Term d n) ->
+               (eq   : ScopeTermN 5 d n) ->
+               (nat  : Term d n) ->
+               (box  : ScopeTerm d n) ->
+               Elim d n
+
     ||| term closure/suspended substitution
     CloE  : (el : Elim d from) -> (th : Lazy (TSubst d from to)) ->
             Elim d to
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 0523341..4ffa82b 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -25,17 +25,19 @@ annD    = hlF Syntax $ ifUnicode "∷" "::"
 natD    = hlF Syntax $ ifUnicode "ℕ" "Nat"
 
 export %inline
-eqD, colonD, commaD, semiD, caseD, returnD, ofD, dotD, zeroD, succD : Doc HL
-eqD     = hl Syntax "Eq"
-colonD  = hl Syntax ":"
-commaD  = hl Syntax ","
-semiD   = hl Syntax ";"
-caseD   = hl Syntax "case"
-ofD     = hl Syntax "of"
-returnD = hl Syntax "return"
-dotD    = hl Delim "."
-zeroD   = hl Syntax "zero"
-succD   = hl Syntax "succ"
+eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
+ofD, dotD, zeroD, succD : Doc HL
+eqD       = hl Syntax "Eq"
+colonD    = hl Syntax ":"
+commaD    = hl Syntax ","
+semiD     = hl Syntax ";"
+caseD     = hl Syntax "case"
+typecaseD = hl Syntax "type-case"
+ofD       = hl Syntax "of"
+returnD   = hl Syntax "return"
+dotD      = hl Delim "."
+zeroD     = hl Syntax "zero"
+succD     = hl Syntax "succ"
 
 
 export
@@ -141,6 +143,19 @@ prettyArms =
   map (braces . aseparate semiD) .
   traverse (\(xs, l, r) => prettyArm T xs l r)
 
+export
+prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
+              Doc HL -> a -> BaseName -> b ->
+              List (SnocList BaseName, Doc HL, c) ->
+              m (Doc HL)
+prettyCase' intro elim r ret arms = do
+  elim  <- pretty0M elim
+  ret   <- case r of
+    Unused => pretty0M ret
+    _      => prettyLams Nothing T [< r] ret
+  arms  <- prettyArms arms
+  pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
+
 export
 prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
              Qty -> a -> BaseName -> b ->
@@ -148,10 +163,7 @@ prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
              m (Doc HL)
 prettyCase pi elim r ret arms = do
   caseq <- (caseD <+>) <$> prettySuffix pi
-  elim  <- pretty0M elim
-  ret   <- prettyLams Nothing T [< r] ret
-  arms  <- prettyArms arms
-  pure $ asep [caseq <++> elim, returnD <++> ret, ofD <++> arms]
+  prettyCase' caseq elim r ret arms
 
 export
 escapeString : String -> String
@@ -293,6 +305,24 @@ parameters (showSubsts : Bool)
       s <- withPrec AnnL $ prettyM s
       a <- withPrec AnnR $ prettyM a
       parensIfM AnnR $ hang 2 $ s <++> !annD <%%> a
+    prettyM (TypeCase ty ret univ
+                (S [< piA, piB] pi) (S [< sigA, sigB] sig) enum
+                (S [< eqA0, eqA1, eqA, eqL, eqR] eq)
+                nat (S [< boxA] box)) = do
+      let v : BaseName -> Doc HL := pretty0 True . TV
+      pipat  <- pure $ parens $ hsep [v piA,  !arrowD, v piB]
+      sigpat <- pure $ parens $ hsep [v sigA, !timesD, v sigB]
+      eqpat  <- prettyApps Nothing (L eqD)
+                  [TV eqA0, TV eqA1, TV eqA, TV eqL, TV eqR]
+      boxpat <- pure $ bracks $ v boxA
+      prettyCase' typecaseD ty Unused ret
+        [([<], !typeD, eterm univ),
+         ([< piA, piB], pipat, eterm pi.term),
+         ([< sigA, sigB], sigpat, eterm sig.term),
+         ([<], hl Syntax "{}", eterm enum),
+         ([< eqA0, eqA1, eqA, eqL, eqR], eqpat, eterm eq.term),
+         ([<], !natD, eterm nat),
+         ([< boxA], boxpat, eterm box.term)]
     prettyM (CloE e th)  =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 99c4b51..7a7097a 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -305,6 +305,12 @@ mutual
       nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =
       nclo $ (s // th // ph) :# (a // th // ph)
+    pushSubstsWith th ph (TypeCase ty ret univ pi sig enum eq nat box) =
+      nclo $ TypeCase (ty   // th // ph) (ret  // th // ph)
+                      (univ // th // ph) (pi   // th // ph)
+                      (sig  // th // ph) (enum // th // ph)
+                      (eq   // th // ph) (nat  // th // ph)
+                      (box  // th // ph)
     pushSubstsWith th ph (CloE e ps) =
       pushSubstsWith th (comp th ps ph) e
     pushSubstsWith th ph (DCloE e ps) =
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 078030f..ce3b968 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -46,6 +46,17 @@ lubs ctx []        = Just $ zeroFor ctx
 lubs ctx (x :: xs) = lubs1 $ x ::: xs
 
 
+||| context extension with no names or quantities
+private
+CtxExtension0' : Nat -> Nat -> Nat -> Type
+CtxExtension0' s d n = Context (Term d . (+ n)) s
+
+private
+addNames0 : Context (Term d . (+ n)) s -> NContext s -> CtxExtension d n (s + n)
+addNames0 [<] [<] = [<]
+addNames0 (ts :< t) (xs :< x) = addNames0 ts xs :< (Zero, x, t)
+
+
 mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
   |||
@@ -222,9 +233,7 @@ mutual
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     checkTypeC ctx arg u
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
-    case res.body of
-      Y res' => checkTypeC (extendTy Zero res.name arg ctx) res' u
-      N res' => checkTypeC ctx                              res' u
+    checkTypeScope ctx arg res u
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
 
   checkType' ctx t@(Lam {}) u =
@@ -234,9 +243,7 @@ mutual
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     checkTypeC ctx fst u
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
-    case snd.body of
-      Y snd' => checkTypeC (extendTy Zero snd.name fst ctx) snd' u
-      N snd' => checkTypeC ctx                              snd' u
+    checkTypeScope ctx fst snd u
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
 
   checkType' ctx t@(Pair {}) u =
@@ -278,6 +285,32 @@ mutual
       Nothing => ignore $ expectTYPE !ask ctx infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
+  private covering
+  check0ScopeN : {s : Nat} ->
+                 TyContext d n -> CtxExtension0' s d n ->
+                 ScopeTermN s d n -> Term d n -> TC ()
+  check0ScopeN ctx ext (S _     (N body)) ty = check0 ctx body ty
+  check0ScopeN ctx ext (S names (Y body)) ty =
+    check0 (extendTyN (addNames0 ext names) ctx) body (weakT {by = s} ty)
+
+  private covering
+  check0Scope : TyContext d n -> Term d n ->
+                ScopeTerm d n -> Term d n -> TC ()
+  check0Scope ctx t = check0ScopeN ctx [< t]
+
+
+  private covering
+  checkTypeScopeN : TyContext d n -> CtxExtension0' s d n ->
+                    ScopeTermN s d n -> Maybe Universe -> TC ()
+  checkTypeScopeN ctx ext (S _     (N body)) u = checkType ctx body u
+  checkTypeScopeN ctx ext (S names (Y body)) u =
+    checkType (extendTyN (addNames0 ext names) ctx) body u
+
+  private covering
+  checkTypeScope : TyContext d n -> Term d n ->
+                   ScopeTerm d n -> Maybe Universe -> TC ()
+  checkTypeScope ctx s = checkTypeScopeN ctx [< s]
+
 
   private covering
   infer' : TyContext d n -> SQty ->
@@ -286,14 +319,12 @@ mutual
 
   infer' ctx sg (F x) = do
     -- if π·x : A {≔ s} in global context
-    g <- lookupFree x
+    g <- lookupFree x !ask
     -- if σ ≤ π
     expectCompatQ sg.fst g.qty.fst
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
-    pure $ InfRes {type = injectT ctx g.type, qout = zeroFor ctx}
-   where
-    lookupFree : Name -> TC Definition
-    lookupFree x = lookupFree' !ask x
+    let Val d = ctx.dimLen; Val n = ctx.termLen
+    pure $ InfRes {type = g.type, qout = zeroFor ctx}
 
   infer' ctx sg (B i) =
     -- if x : A ∈ Γ
@@ -417,6 +448,26 @@ mutual
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
+  infer' ctx sg (TypeCase ty ret univ pi sig enum eq nat box) = do
+    -- if σ = 0
+    expectEqualQ Zero sg.fst
+    -- if Ψ, Γ ⊢₀ e ⇒ Type u
+    u <- expectTYPE !ask ctx . type =<< inferC ctx szero ty
+    -- if Ψ, Γ ⊢₀ C ⇐ Type
+    --   (non-dependent return type)
+    checkTypeC ctx ret Nothing
+    -- if all the cases have type C
+    check0 ctx univ ret
+    check0ScopeN ctx [< TYPE u, Arr Zero (BVT 0) (TYPE u)] pi  ret
+    check0ScopeN ctx [< TYPE u, Arr Zero (BVT 0) (TYPE u)] sig ret
+    check0 ctx enum ret
+    check0ScopeN ctx [< TYPE u, TYPE u, Eq0 (TYPE u) (BVT 1) (BVT 0),
+                        BVT 2, BVT 2] eq ret
+    check0 ctx nat ret
+    check0Scope ctx (TYPE u) box ret
+    -- then Ψ, Γ ⊢₀ type-case ⋯ ⇒ C
+    pure $ InfRes {type = ret, qout = zeroFor ctx}
+
   infer' ctx sg (term :# type) = do
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
     checkTypeC ctx type Nothing
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index b8321c4..d1ff753 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -33,11 +33,8 @@ InferResult eqs d n = IfConsistent eqs $ InferResult' d n
 
 
 export
-lookupFree' : Has ErrorEff fs => Definitions -> Name -> Eff fs Definition
-lookupFree' defs x =
-  case lookup x defs of
-    Just d  => pure d
-    Nothing => throw $ NotInScope x
+lookupFree : Has ErrorEff fs => Name -> Definitions -> Eff fs Definition
+lookupFree x defs = maybe (throw $ NotInScope x) pure $ lookup x defs
 
 
 public export
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 45deb46..555e4ab 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -65,6 +65,11 @@ extendLen : Telescope a from to -> Singleton from -> Singleton to
 extendLen [<]        x = x
 extendLen (tel :< _) x = [|S $ extendLen tel x|]
 
+
+public export
+CtxExtension : Nat -> Nat -> Nat -> Type
+CtxExtension d = Telescope ((Qty, BaseName,) . Term d)
+
 namespace TyContext
   public export %inline
   empty : TyContext 0 0
@@ -76,8 +81,7 @@ namespace TyContext
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : Telescope (\n => (Qty, BaseName, Term d n)) from to ->
-              TyContext d from -> TyContext d to
+  extendTyN : CtxExtension d from to -> TyContext d from -> TyContext d to
   extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkTyContext {
@@ -89,8 +93,7 @@ namespace TyContext
     }
 
   export %inline
-  extendTy : Qty -> BaseName -> Term d n -> TyContext d n ->
-             TyContext d (S n)
+  extendTy : Qty -> BaseName -> Term d n -> TyContext d n -> TyContext d (S n)
   extendTy q x s = extendTyN [< (q, x, s)]
 
   export %inline
@@ -108,16 +111,6 @@ namespace TyContext
   eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
   eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}
 
-  export
-  injectT : TyContext d n -> Term 0 0 -> Term d n
-  injectT (MkTyContext {dimLen = Val d, termLen = Val n, _}) tm =
-    tm // shift0 d // shift0 n
-
-  export
-  injectE : TyContext d n -> Elim 0 0 -> Elim d n
-  injectE (MkTyContext {dimLen = Val d, termLen = Val n, _}) el =
-    el // shift0 d // shift0 n
-
 
 namespace QOutput
   export %inline
@@ -197,14 +190,6 @@ namespace EqContext
       dnames, tnames, qtys
     }
 
-  export
-  injectT : EqContext n -> Term 0 0 -> Term 0 n
-  injectT (MkEqContext {termLen = Val n, _}) tm = tm // shift0 n
-
-  export
-  injectE : EqContext n -> Elim 0 0 -> Elim 0 n
-  injectE (MkEqContext {termLen = Val n, _}) el = el // shift0 n
-
 
 private
 data CtxBinder a = MkCtxBinder BaseName a
diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
index ae899c1..a12ac7a 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -115,6 +115,19 @@ mutual
     (tm1 :# ty1) == (tm2 :# ty2) = tm1 == tm2 && ty1 == ty2
     (_ :# _) == _ = False
 
+    TypeCase ty1 ret1 univ1 pi1 sig1 enum1 eq1 nat1 box1
+      ==
+    TypeCase ty2 ret2 univ2 pi2 sig2 enum2 eq2 nat2 box2 =
+      ty1 == ty2 && ret1 == ret2 &&
+      pi1.term == pi2.term &&
+      sig1.term == sig2.term &&
+      enum1 == enum2 &&
+      eq1.term == eq2.term &&
+      nat1 == nat2 &&
+      box1.term == box2.term
+
+    TypeCase {} == _ = False
+
     CloE el1 th1 == CloE el2 th2 =
       case eqSubstLen th1 th2 of
            Just Refl => el1 == el2 && th1 == th2
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index 249d398..d2e7408 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -138,8 +138,8 @@ tests = "pretty printing terms" :- [
   "case" :- [
     testPrettyE [<] [<]
       (CasePair One (F "a") (SN $ TYPE 1) (SN $ TYPE 0))
-      "case1 a return _ ⇒ ★₁ of { (_, _) ⇒ ★₀ }"
-      "case1 a return _ => Type1 of { (_, _) => Type0 }",
+      "case1 a return ★₁ of { (_, _) ⇒ ★₀ }"
+      "case1 a return Type1 of { (_, _) => Type0 }",
     testPrettyT [<] [<]
       ([< "u"] :\\
         E (CaseEnum One (F "u")
@@ -152,6 +152,35 @@ tests = "pretty printing terms" :- [
       """
   ],
 
+  "type-case" :- [
+    testPrettyE [<] [<]
+      {label = "type-case ℕ ∷ ★₀ return ★₀ of { ⋯ }"}
+      (TypeCase (Nat :# TYPE 0) (TYPE 0) Nat (SN Nat) (SN Nat) Nat
+        (SN Nat) Nat (SN Nat))
+      """
+        type-case ℕ ∷ ★₀ return ★₀ of {
+          ★            ⇒ ℕ;
+          (_ → _)      ⇒ ℕ;
+          (_ × _)      ⇒ ℕ;
+          {}           ⇒ ℕ;
+          Eq _ _ _ _ _ ⇒ ℕ;
+          ℕ            ⇒ ℕ;
+          [_]          ⇒ ℕ
+        }
+      """
+      """
+        type-case Nat :: Type0 return Type0 of {
+          Type         => Nat;
+          (_ -> _)     => Nat;
+          (_ ** _)     => Nat;
+          {}           => Nat;
+          Eq _ _ _ _ _ => Nat;
+          Nat          => Nat;
+          [_]          => Nat
+        }
+      """
+  ],
+
   "annotations" :- [
     testPrettyE [<] [<] (FT "a" :# FT "A") "a ∷ A" "a :: A",
     testPrettyE [<] [<]
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index d5b5e27..3ee5ef3 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -448,6 +448,14 @@ tests = "typechecker" :- [
   todo "box values",
   todo "box elim",
 
+  "type-case" :- [
+    testTC "0 · type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ } ⇒ ★₀" $
+      inferAs empty szero
+        (TypeCase (Nat :# TYPE 0) (TYPE 0) Nat (SN Nat) (SN Nat) Nat
+          (SN Nat) Nat (SN Nat))
+        (TYPE 0)
+  ],
+
   "misc" :- [
     note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
     note "⊢",