module Tests.Typechecker

import Quox.Syntax
import Quox.Typechecker as Lib
import public TypingImpls
import TAP
import Quox.EffExtra
import AstExtra
import PrettyExtra


%hide Prelude.App
%hide Pretty.App


data Error'
  = TCError Typing.Error
  | WrongInfer (BContext d) (BContext n) (Term d n) (Term d n)
  | WrongQOut (QOutput n) (QOutput n)

export
ToInfo Error' where
  toInfo (TCError e) = toInfo e
  toInfo (WrongInfer dnames tnames good bad) =
    [("type", "WrongInfer"),
     ("wanted", prettyStr $ prettyTerm dnames tnames good),
     ("got", prettyStr $ prettyTerm dnames tnames bad)]
  toInfo (WrongQOut good bad) =
    [("type", "WrongQOut"),
     ("wanted", show good),
     ("wanted", show bad)]

0 M : Type -> Type
M = Eff [Except Error', DefsReader]

inj : TC a -> M a
inj act = rethrow $ mapFst TCError $ runTC !defs act


reflTy : Term d n
reflTy =
  ^PiY Zero "A" (^TYPE 0)
    (^PiY One  "x" (^BVT 0)
      (^Eq0 (^BVT 1) (^BVT 0) (^BVT 0)))

reflDef : Term d n
reflDef = ^LamY "A" (^LamY "x" (^DLamY "i" (^BVT 0)))


fstTy : Term d n
fstTy =
  ^PiY Zero "A" (^TYPE 1)
    (^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 1))
      (^Arr Any (^SigY "x" (^BVT 1) (E $ ^App (^BV 1) (^BVT 0))) (^BVT 1)))

fstDef : Term d n
fstDef =
  ^LamY "A" (^LamY "B" (^LamY "p"
    (E $ ^CasePair Any (^BV 0) (SN $ ^BVT 2)
      (SY [< "x", "y"] $ ^BVT 1))))

sndTy : Term d n
sndTy =
  ^PiY Zero "A" (^TYPE 1)
    (^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 1))
      (^PiY Any "p" (^SigY "x" (^BVT 1) (E $ ^App (^BV 1) (^BVT 0)))
        (E $ ^App (^BV 1)
          (E $ ^App (^App (^App (^F "fst") (^BVT 2)) (^BVT 1)) (^BVT 0)))))

sndDef : Term d n
sndDef =
  -- λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (x, y) ⇒ y }
  ^LamY "A" (^LamY "B" (^LamY "p"
    (E $ ^CasePair Any (^BV 0)
      (SY [< "p"] $ E $
        ^App (^BV 2)
          (E $ ^App (^App (^App (^F "fst") (^BVT 3)) (^BVT 2)) (^BVT 0)))
      (SY [< "x", "y"] $ ^BVT 0))))

nat : Term d n
nat = ^Nat


defGlobals : Definitions
defGlobals = fromList
  [("A",  ^mkPostulate gzero (^TYPE 0)),
   ("B",  ^mkPostulate gzero (^TYPE 0)),
   ("C",  ^mkPostulate gzero (^TYPE 1)),
   ("D",  ^mkPostulate gzero (^TYPE 1)),
   ("P",  ^mkPostulate gzero (^Arr Any (^FT "A") (^TYPE 0))),
   ("a",  ^mkPostulate gany  (^FT "A")),
   ("a'", ^mkPostulate gany  (^FT "A")),
   ("b",  ^mkPostulate gany  (^FT "B")),
   ("f",  ^mkPostulate gany  (^Arr One (^FT "A") (^FT "A"))),
   ("fω", ^mkPostulate gany  (^Arr Any (^FT "A") (^FT "A"))),
   ("g",  ^mkPostulate gany  (^Arr One (^FT "A") (^FT "B"))),
   ("f2", ^mkPostulate gany
      (^Arr One (^FT "A") (^Arr One (^FT "A") (^FT "B")))),
   ("p",  ^mkPostulate gany
      (^PiY One "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))),
   ("q",  ^mkPostulate gany
      (^PiY One "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))),
   ("refl", ^mkDef gany reflTy reflDef),
   ("fst",  ^mkDef gany fstTy fstDef),
   ("snd",  ^mkDef gany sndTy sndDef)]

parameters (label : String) (act : Lazy (M ()))
           {default defGlobals globals : Definitions}
  testTC : Test
  testTC = test label {e = Error', a = ()} $
    extract $ runExcept $ runReaderAt DEFS globals act

  testTCFail : Test
  testTCFail = testThrows label (const True) $
    (extract $ runExcept $ runReaderAt DEFS globals act) $> "()"


inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> M ()
inferredTypeEq ctx exp got =
  wrapErr (const $ WrongInfer ctx.dnames ctx.tnames exp got) $ inj $ lift $
    equalType noLoc ctx exp got

qoutEq : (exp, got : QOutput n) -> M ()
qoutEq qout res = unless (qout == res) $ throw $ WrongQOut qout res

inferAs : TyContext d n -> (sg : SQty) -> Elim d n -> Term d n -> M ()
inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
  case !(inj $ infer ctx sg e) of
    Just res => inferredTypeEq ctx ty res.type
    Nothing  => pure ()

inferAsQ : TyContext d n -> (sg : SQty) ->
           Elim d n -> Term d n -> QOutput n -> M ()
inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
  case !(inj $ infer ctx sg e) of
    Just res => do
      inferredTypeEq ctx ty res.type
      qoutEq qout res.qout
    Nothing => pure ()

infer_ : TyContext d n -> (sg : SQty) -> Elim d n -> M ()
infer_ ctx sg e = ignore $ inj $ infer ctx sg e

checkQ : TyContext d n -> SQty ->
         Term d n -> Term d n -> QOutput n -> M ()
checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
  case !(inj $ check ctx sg s ty) of
    Just res => qoutEq qout res
    Nothing  => pure ()

check_ : TyContext d n -> SQty -> Term d n -> Term d n -> M ()
check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty

checkType_ : TyContext d n -> Term d n -> Maybe Universe -> M ()
checkType_ ctx s u = inj $ checkType ctx s u


export
tests : Test
tests = "typechecker" :- [
  "universes" :- [
    testTC "0 · ★₀ ⇐ ★₁  # by checkType" $
      checkType_ empty (^TYPE 0) (Just 1),
    testTC "0 · ★₀ ⇐ ★₁  # by check" $
      check_ empty szero (^TYPE 0) (^TYPE 1),
    testTC "0 · ★₀ ⇐ ★₂" $
      checkType_ empty (^TYPE 0) (Just 2),
    testTC "0 · ★₀ ⇐ ★_" $
      checkType_ empty (^TYPE 0) Nothing,
    testTCFail "0 · ★₁ ⇍ ★₀" $
      checkType_ empty (^TYPE 1) (Just 0),
    testTCFail "0 · ★₀ ⇍ ★₀" $
      checkType_ empty (^TYPE 0) (Just 0),
    testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
      checkType_ empty01 (^TYPE 1) (Just 0),
    testTCFail "1 · ★₀ ⇍ ★₁  # by check" $
      check_ empty sone (^TYPE 0) (^TYPE 1)
  ],

  "function types" :- [
    note "A, B : ★₀;  C, D : ★₁;  P : 0.A → ★₀",
    testTC "0 · 1.A → B ⇐ ★₀" $
      check_ empty szero (^Arr One (^FT "A") (^FT "B")) (^TYPE 0),
    note "subtyping",
    testTC "0 · 1.A → B ⇐ ★₁" $
      check_ empty szero (^Arr One (^FT "A") (^FT "B")) (^TYPE 1),
    testTC "0 · 1.C → D ⇐ ★₁" $
      check_ empty szero (^Arr One (^FT "C") (^FT "D")) (^TYPE 1),
    testTCFail "0 · 1.C → D ⇍ ★₀" $
      check_ empty szero (^Arr One (^FT "C") (^FT "D")) (^TYPE 0),
    testTC "0 · 1.(x : A) → P x ⇐ ★₀" $
      check_ empty szero
        (^PiY One "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))
        (^TYPE 0),
    testTCFail "0 · 1.A → P ⇍ ★₀" $
      check_ empty szero (^Arr One (^FT "A") (^FT "P")) (^TYPE 0),
    testTC "0=1 ⊢ 0 · 1.A → P ⇐ ★₀" $
      check_ empty01 szero (^Arr One (^FT "A") (^FT "P")) (^TYPE 0)
  ],

  "pair types" :- [
    testTC "0 · A × A ⇐ ★₀" $
      check_ empty szero (^And (^FT "A") (^FT "A")) (^TYPE 0),
    testTCFail "0 · A × P ⇍ ★₀" $
      check_ empty szero (^And (^FT "A") (^FT "P")) (^TYPE 0),
    testTC "0 · (x : A) × P x ⇐ ★₀" $
      check_ empty szero
        (^SigY "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))
        (^TYPE 0),
    testTC "0 · (x : A) × P x ⇐ ★₁" $
      check_ empty szero
        (^SigY "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))
        (^TYPE 1),
    testTC "0 · (A : ★₀) × A ⇐ ★₁" $
      check_ empty szero
        (^SigY "A" (^TYPE 0) (^BVT 0))
        (^TYPE 1),
    testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
      check_ empty szero
        (^SigY "A" (^TYPE 0) (^BVT 0))
        (^TYPE 0),
    testTCFail "1 · A × A ⇍ ★₀" $
      check_ empty sone
        (^And (^FT "A") (^FT "A"))
        (^TYPE 0)
  ],

  "enum types" :- [
    testTC "0 · {} ⇐ ★₀" $ check_ empty szero (^enum []) (^TYPE 0),
    testTC "0 · {} ⇐ ★₃" $ check_ empty szero (^enum []) (^TYPE 3),
    testTC "0 · {a,b,c} ⇐ ★₀" $
      check_ empty szero (^enum ["a", "b", "c"]) (^TYPE 0),
    testTC "0 · {a,b,c} ⇐ ★₃" $
      check_ empty szero (^enum ["a", "b", "c"]) (^TYPE 3),
    testTCFail "1 · {} ⇍ ★₀" $ check_ empty sone (^enum []) (^TYPE 0),
    testTC "0=1 ⊢ 1 · {} ⇐ ★₀" $ check_ empty01 sone (^enum []) (^TYPE 0)
  ],

  "free vars" :- [
    note "A : ★₀",
    testTC "0 · A ⇒ ★₀" $
      inferAs empty szero (^F "A") (^TYPE 0),
    testTC "0 · [A] ⇐ ★₀" $
      check_ empty szero (^FT "A") (^TYPE 0),
    note "subtyping",
    testTC "0 · [A] ⇐ ★₁" $
      check_ empty szero (^FT "A") (^TYPE 1),
    note "(fail) runtime-relevant type",
    testTCFail "1 · A ⇏ ★₀" $
      infer_ empty sone (^F "A"),
    testTC "1 . f ⇒ 1.A → A" $
      inferAs empty sone (^F "f") (^Arr One (^FT "A") (^FT "A")),
    testTC "1 . f ⇐ 1.A → A" $
      check_ empty sone (^FT "f") (^Arr One (^FT "A") (^FT "A")),
    testTCFail "1 . f ⇍ 0.A → A" $
      check_ empty sone (^FT "f") (^Arr Zero (^FT "A") (^FT "A")),
    testTCFail "1 . f ⇍ ω.A → A" $
      check_ empty sone (^FT "f") (^Arr Any (^FT "A") (^FT "A")),
    testTC "1 . (λ x ⇒ f x) ⇐ 1.A → A" $
      check_ empty sone
        (^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
        (^Arr One (^FT "A") (^FT "A")),
    testTC "1 . (λ x ⇒ f x) ⇐ ω.A → A" $
      check_ empty sone
        (^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
        (^Arr Any (^FT "A") (^FT "A")),
    testTCFail "1 . (λ x ⇒ f x) ⇍ 0.A → A" $
      check_ empty sone
        (^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
        (^Arr Zero (^FT "A") (^FT "A")),
    testTC "1 . fω ⇒ ω.A → A" $
      inferAs empty sone (^F "fω") (^Arr Any (^FT "A") (^FT "A")),
    testTC "1 . (λ x ⇒ fω x) ⇐ ω.A → A" $
      check_ empty sone
        (^LamY "x" (E $ ^App (^F "fω") (^BVT 0)))
        (^Arr Any (^FT "A") (^FT "A")),
    testTCFail "1 . (λ x ⇒ fω x) ⇍ 0.A → A" $
      check_ empty sone
        (^LamY "x" (E $ ^App (^F "fω") (^BVT 0)))
        (^Arr Zero (^FT "A") (^FT "A")),
    testTCFail "1 . (λ x ⇒ fω x) ⇍ 1.A → A" $
      check_ empty sone
        (^LamY "x" (E $ ^App (^F "fω") (^BVT 0)))
        (^Arr One (^FT "A") (^FT "A")),
    note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
    testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (^F "refl") reflTy,
    testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (^FT "refl") reflTy
  ],

  "bound vars" :- [
    testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
      inferAsQ (ctx [< ("x", ^FT "A")]) sone
        (^BV 0) (^FT "A") [< One],
    testTC "x : A ⊢ 1 · x ⇐ A ⊳ 1·x" $
      checkQ (ctx [< ("x", ^FT "A")]) sone (^BVT 0) (^FT "A") [< One],
    note "f2 : 1.A → 1.A → B",
    testTC "x : A ⊢ 1 · f2 x x ⇒ B ⊳ ω·x" $
      inferAsQ (ctx [< ("x", ^FT "A")]) sone
        (^App (^App (^F "f2") (^BVT 0)) (^BVT 0)) (^FT "B") [< Any]
  ],

  "lambda" :- [
    note "linear & unrestricted identity",
    testTC "1 · (λ x ⇒ x) ⇐ A → A" $
      check_ empty sone
        (^LamY "x" (^BVT 0))
        (^Arr One (^FT "A") (^FT "A")),
    testTC "1 · (λ x ⇒ x) ⇐ ω.A → A" $
      check_ empty sone
        (^LamY "x" (^BVT 0))
        (^Arr Any (^FT "A") (^FT "A")),
    note "(fail) zero binding used relevantly",
    testTCFail "1 · (λ x ⇒ x) ⇍ 0.A → A" $
      check_ empty sone
        (^LamY "x" (^BVT 0))
        (^Arr Zero (^FT "A") (^FT "A")),
    note "(but ok in overall erased context)",
    testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
      check_ empty szero
        (^LamY "x" (^BVT 0))
        (^Arr Zero (^FT "A") (^FT "A")),
    testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯  # (type of refl)" $
      check_ empty sone
        (^LamY "A" (^LamY "x" (E $ ^App (^App (^F "refl") (^BVT 1)) (^BVT 0))))
        reflTy,
    testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
      check_ empty sone reflDef reflTy
  ],

  "pairs" :- [
    testTC "1 · (a, a) ⇐ A × A" $
      check_ empty sone
        (^Pair (^FT "a") (^FT "a")) (^And (^FT "A") (^FT "A")),
    testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
      checkQ (ctx [< ("x", ^FT "A")]) sone
        (^Pair (^BVT 0) (^BVT 0)) (^And (^FT "A") (^FT "A")) [< Any],
    testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
      check_ empty sone
        (^Pair (^FT "a") (^DLamN (^FT "a")))
        (^SigY "x" (^FT "A") (^Eq0 (^FT "A") (^BVT 0) (^FT "a")))
  ],

  "unpairing" :- [
    testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
      inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) sone
        (^CasePair One (^BV 0) (SN $ ^FT "B")
          (SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0)))
        (^FT "B") [< One],
    testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
      inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) sone
        (^CasePair Any (^BV 0) (SN $ ^FT "B")
          (SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0)))
        (^FT "B") [< Any],
    testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
      inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) szero
        (^CasePair Any (^BV 0) (SN $ ^FT "B")
          (SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0)))
        (^FT "B") [< Zero],
    testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
      infer_ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) sone
        (^CasePair Zero (^BV 0) (SN $ ^FT "B")
          (SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0))),
    testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
      inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "B"))]) sone
        (^CasePair Any (^BV 0) (SN $ ^FT "A")
          (SY [< "l", "r"] $ ^BVT 1))
        (^FT "A") [< Any],
    testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
      inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "B"))]) szero
        (^CasePair One (^BV 0) (SN $ ^FT "A")
          (SY [< "l", "r"] $ ^BVT 1))
        (^FT "A") [< Zero],
    testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
      infer_ (ctx [< ("x", ^And (^FT "A") (^FT "B"))]) sone
        (^CasePair One (^BV 0) (SN $ ^FT "A")
          (SY [< "l", "r"] $ ^BVT 1)),
    note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
    note "    ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
    testTC "0 · ‹type of fst› ⇐ ★₂" $
      check_ empty szero fstTy (^TYPE 2),
    testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $
      check_ empty sone fstDef fstTy,
    note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)",
    note "    ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
    testTC "0 · ‹type of snd› ⇐ ★₂" $
      check_ empty szero sndTy (^TYPE 2),
    testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $
      check_ empty sone sndDef sndTy,
    testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
      inferAs empty szero
        (^App (^App (^F "snd") (^TYPE 0)) (^LamY "x" (^BVT 0)))
        (^PiY Any "p" (^SigY "A" (^TYPE 0) (^BVT 0))
          (E $ ^App (^App (^App (^F "fst") (^TYPE 0)) (^LamY "x" (^BVT 0)))
                    (^BVT 0)))
  ],

  "enums" :- [
    testTC "1 · 'a ⇐ {a}" $
      check_ empty sone (^Tag "a") (^enum ["a"]),
    testTC "1 · 'a ⇐ {a, b, c}" $
      check_ empty sone (^Tag "a") (^enum ["a", "b", "c"]),
    testTCFail "1 · 'a ⇍ {b, c}" $
      check_ empty sone (^Tag "a") (^enum ["b", "c"]),
    testTC "0=1 ⊢ 1 · 'a ⇐ {b, c}" $
      check_ empty01 sone (^Tag "a") (^enum ["b", "c"])
  ],

  "enum matching" :- [
    testTC "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'tt ⇒ 'tt } ⇒ {tt}" $
      inferAs (ctx [< ("x", ^enum ["tt"])]) sone
        (^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
          (singleton "tt" (^Tag "tt")))
        (^enum ["tt"]),
    testTCFail "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'ff ⇒ 'tt } ⇏" $
      infer_ (ctx [< ("x", ^enum ["tt"])]) sone
        (^CaseEnum One (^BV 0) (SN (^enum ["tt"]))
          (singleton "ff" (^Tag "tt")))
  ],

  "equality types" :- [
    testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ Type" $
      checkType_ empty (^Eq0 (^TYPE 0) nat nat) Nothing,
    testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₁" $
      check_ empty szero (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
    testTCFail "1 · ℕ ≡ ℕ : ★₀ ⇍ ★₁" $
      check_ empty sone (^Eq0 (^TYPE 0) nat nat) (^TYPE 1),
    testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₂" $
      check_ empty szero (^Eq0 (^TYPE 0) nat nat) (^TYPE 2),
    testTC "0 · ℕ ≡ ℕ : ★₁ ⇐ ★₂" $
      check_ empty szero (^Eq0 (^TYPE 1) nat nat) (^TYPE 2),
    testTCFail "0 · ℕ ≡ ℕ : ★₁ ⇍ ★₁" $
      check_ empty szero (^Eq0 (^TYPE 1) nat nat) (^TYPE 1),
    testTCFail "0 ≡ 'beep : {beep} ⇍ Type" $
      checkType_ empty
        (^Eq0 (^enum ["beep"]) (^Zero) (^Tag "beep"))
        Nothing,
    testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
      check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A") (^FT "B")),
                     ("x", ^FT "A"), ("y", ^FT "B")]) szero
        (^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 1) (^BVT 0))
        (^TYPE 0),
    testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
      check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A") (^FT "B")),
                     ("x", ^FT "A"), ("y", ^FT "B")]) szero
        (^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 0) (^BVT 1))
        (^TYPE 0)
  ],

  "equalities" :- [
    testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
      check_ empty sone (^DLamN (^FT "a"))
        (^Eq0 (^FT "A") (^FT "a") (^FT "a")),
    testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q  # uip" $
      check_ empty szero
        (^LamY "p" (^LamY "q" (^DLamN (^BVT 1))))
        (^PiY Any "p" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
          (^PiY Any "q" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
            (^Eq0 (^Eq0 (^FT "A") (^FT "a") (^FT "a")) (^BVT 1) (^BVT 0)))),
    testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q  # uip(2)" $
      check_ empty szero
        (^LamY "p" (^LamY "q" (^DLamN (^BVT 0))))
        (^PiY Any "p" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
          (^PiY Any "q" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
            (^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,
    testTCFail "1 · zero ⇍ ℕ×ℕ" $ check_ empty sone (^Zero) (^And nat nat),
    testTC "ω·n : ℕ ⊢ 1 · succ n ⇐ ℕ" $
      check_ (ctx [< ("n", nat)]) sone (^Succ (^BVT 0)) nat,
    testTC "1 · λ n ⇒ succ n ⇐ 1.ℕ → ℕ" $
      check_ empty sone
        (^LamY "n" (^Succ (^BVT 0)))
        (^Arr One nat nat)
  ],

  "natural elim" :- [
    note "1 · λ n ⇒ case1 n return ℕ of { zero ⇒ 0; succ n ⇒ n }",
    note "    ⇐ 1.ℕ → ℕ",
    testTC "pred" $
      check_ empty sone
        (^LamY "n" (E $
          ^CaseNat One Zero (^BV 0) (SN nat)
            (^Zero) (SY [< "n", ^BN Unused] $ ^BVT 1)))
        (^Arr One nat nat),
    note "1 · λ m n ⇒ case1 m return ℕ of { zero ⇒ n; succ _, 1.p ⇒ succ p }",
    note "    ⇐ 1.ℕ → 1.ℕ → 1.ℕ",
    testTC "plus" $
      check_ empty sone
        (^LamY "m" (^LamY "n" (E $
          ^CaseNat One One (^BV 1) (SN nat)
            (^BVT 0)
            (SY [< ^BN Unused, "p"] $ ^Succ (^BVT 0)))))
        (^Arr One nat (^Arr One nat nat))
  ],

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

  "type-case" :- [
    testTC "0 · type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ } ⇒ ★₀" $
      inferAs empty szero
        (^TypeCase (^Ann nat (^TYPE 0)) (^TYPE 0) empty nat)
        (^TYPE 0)
  ],

  todo "add the examples dir to the tests"
]

{-
  "misc" :- [
    note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
    note "⊢",
    note "1 · λ x y xy ⇒ δ i ⇒ p (xy i)",
    note "  ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
    testTC "cong" $
      check_ empty sone
        ([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
        (PiY Zero "x"  (FT "A") $
         PiY Zero "y"  (FT "A") $
         PiY One  "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
         EqY "i" (E $ F "P" :@ E (BV 0 :% BV 0))
             (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
    note "0·A : Type, 0·P : ω·A → Type,",
    note "ω·p q : (1·x : A) → P x",
    note "⊢",
    note "1 · λ eq ⇒ δ i ⇒ λ x ⇒ eq x i",
    note "  ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
    testTC "funext" $
      check_ empty sone
        ([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
        (PiY One "eq"
          (PiY One "x" (FT "A")
            (Eq0 (E $ F "P" :@ BVT 0)
                 (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)))
          (Eq0 (PiY Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))),
    todo "absurd (when coerce is in)"
    -- absurd : (`true ≡ `false : {true, false}) ⇾ (0·A : ★₀) → A ≔
    --   λ e ⇒
    --     case coerce [i ⇒ case e @i return ★₀ of {`true ⇒ {tt}; `false ⇒ {}}]
    --            @0 @1 `tt
    --     return A
    --     of { }
  ]
-}