From 846bbc9ca305ff1d0b6831b680ff96213513656c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 13 Feb 2023 22:06:53 +0100
Subject: [PATCH] more tc tests

---
 tests/Tests/Typechecker.idr | 147 +++++++++++++++++++++++++++++-------
 1 file changed, 119 insertions(+), 28 deletions(-)

diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index b82b43a..6aead68 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -7,9 +7,31 @@ import public TypingImpls
 import TAP
 
 
-0 M : Type -> Type
-M = ReaderT (Definitions Three) $ Either (Error Three)
+data Error'
+  = TCError (Typing.Error Three)
+  | WrongInfer (Term Three d n) (Term Three d n)
+  | WrongQOut (QOutput Three n) (QOutput Three n)
 
+export
+ToInfo Error' where
+  toInfo (TCError e) = toInfo e
+  toInfo (WrongInfer good bad) =
+    [("type", "WrongInfer"),
+     ("wanted", prettyStr True good),
+     ("got", prettyStr True bad)]
+  toInfo (WrongQOut good bad) =
+    [("type", "WrongQOut"),
+     ("wanted", prettyStr True good),
+     ("wanted", prettyStr True bad)]
+
+0 M : Type -> Type
+M = ReaderT (Definitions Three) $ Either Error'
+
+inj : (forall m. CanTC Three m => m a) -> M a
+inj act = do
+  env <- ask
+  let res = runReaderT env act {m = Either (Typing.Error Three)}
+  either (throwError . TCError) pure res
 
 
 reflTy : IsQty q => Term q d n
@@ -23,17 +45,19 @@ reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0
 
 defGlobals : Definitions Three
 defGlobals = fromList
-  [("A", mkAbstract Zero $ TYPE 0),
-   ("B", mkAbstract Zero $ TYPE 0),
-   ("C", mkAbstract Zero $ TYPE 1),
-   ("D", mkAbstract Zero $ TYPE 1),
-   ("P", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
-   ("a", mkAbstract Any  $ FT "A"),
-   ("b", mkAbstract Any  $ FT "B"),
-   ("f", mkAbstract Any  $ Arr One (FT "A") (FT "A")),
-   ("g", mkAbstract Any  $ Arr One (FT "A") (FT "B")),
-   ("p", mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
-   ("q", mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
+  [("A",  mkAbstract Zero $ TYPE 0),
+   ("B",  mkAbstract Zero $ TYPE 0),
+   ("C",  mkAbstract Zero $ TYPE 1),
+   ("D",  mkAbstract Zero $ TYPE 1),
+   ("P",  mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
+   ("a",  mkAbstract Any  $ FT "A"),
+   ("a'", mkAbstract Any  $ FT "A"),
+   ("b",  mkAbstract Any  $ FT "B"),
+   ("f",  mkAbstract Any  $ Arr One (FT "A") (FT "A")),
+   ("g",  mkAbstract Any  $ Arr One (FT "A") (FT "B")),
+   ("f2", mkAbstract Any  $ Arr One (FT "A") $ Arr One (FT "A") (FT "A")),
+   ("p",  mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
+   ("q",  mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
    ("refl", mkDef Any reflTy reflDef)]
 
 parameters (label : String) (act : Lazy (M ()))
@@ -53,20 +77,40 @@ ctxWith dctx tqctx =
 ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n
 ctx = ctxWith DNil
 
+inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
+inferredTypeEq ctx exp got =
+  catchError
+    (inj $ equalType (makeDimEq ctx.dctx) ctx.tctx exp got)
+    (\_ : Error' => throwError $ WrongInfer exp got)
+
+qoutEq : (exp, got : QOutput Three n) -> M ()
+qoutEq qout res = unless (qout == res) $ throwError $ WrongQOut qout res
+
 inferAs : TyContext Three d n -> (sg : SQty Three) ->
           Elim Three d n -> Term Three d n -> M ()
 inferAs ctx sg e ty = do
-  ty' <- infer ctx sg e
-  catchError
-    (equalType (makeDimEq ctx.dctx) ctx.tctx ty ty'.type)
-    (\_ : Error Three => throwError $ ClashT Equal (TYPE UAny) ty ty'.type)
+  res <- inj $ infer ctx sg e
+  inferredTypeEq ctx ty res.type
+
+inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
+           Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
+inferAsQ ctx sg e ty qout = do
+  res <- inj $ infer ctx sg e
+  inferredTypeEq ctx ty res.type
+  qoutEq qout res.qout
 
 infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
-infer_ ctx sg e = ignore $ infer ctx sg e
+infer_ ctx sg e = ignore $ inj $ infer ctx sg e
+
+checkQ : TyContext Three d n -> SQty Three ->
+         Term Three d n -> Term Three d n -> QOutput Three n -> M ()
+checkQ ctx sg s ty qout = do
+  res <- inj $ check ctx sg s ty
+  qoutEq qout res
 
 check_ : TyContext Three d n -> SQty Three ->
          Term Three d n -> Term Three d n -> M ()
-check_ ctx sg s ty = ignore $ check ctx sg s ty
+check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
 
 export
 tests : Test
@@ -82,7 +126,7 @@ tests = "typechecker" :- [
   ],
 
   "function types" :- [
-    note "A, B : ★₀;  C, D : ★₁",
+    note "A, B : ★₀;  C, D : ★₁;  P : A ⇾ ★₀",
     testTC "0 · A ⊸ B ⇐ ★₀" $
       check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
     note "subtyping",
@@ -91,25 +135,52 @@ tests = "typechecker" :- [
     testTC "0 · C ⊸ D ⇐ ★₁" $
       check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
     testTCFail "0 · C ⊸ D ⇍ ★₀" $
-      check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0)
+      check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0),
+    testTC "0 · (1·x : A) → P x ⇐ ★₀" $
+      check_ (ctx [<]) szero
+        (Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
+        (TYPE 0),
+    testTCFail "0 · A ⊸ P ⇍ ★₀" $
+      check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0)
+  ],
+
+  "pair types" :- [
+    note #""A × B" for "(_ : A) × B""#,
+    testTC "0 · A × A ⇐ ★₀" $
+      check_ (ctx [<]) szero (FT "A" `And` FT "A") (TYPE 0),
+    testTCFail "1 · A × A ⇍ ★₀" $
+      check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0)
   ],
 
   "free vars" :- [
     note "A : ★₀",
     testTC "0 · A ⇒ ★₀" $
       inferAs (ctx [<]) szero (F "A") (TYPE 0),
-    note "check",
-    testTC "0 · A ⇐ ★₀" $
+    testTC "0 · [A] ⇐ ★₀" $
       check_ (ctx [<]) szero (FT "A") (TYPE 0),
     note "subtyping",
-    testTC "0 · A ⇐ ★₁" $
+    testTC "0 · [A] ⇐ ★₁" $
       check_ (ctx [<]) szero (FT "A") (TYPE 1),
     note "(fail) runtime-relevant type",
     testTCFail "1 · A ⇏ ★₀" $
       infer_ (ctx [<]) sone (F "A"),
     note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
     testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F  "refl") reflTy,
-    testTC "1 · refl ⇐ ⋯" $ check_  (ctx [<]) sone (FT "refl") reflTy
+    testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
+  ],
+
+  "bound vars" :- [
+    testTC "1·x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
+      inferAsQ {n = 1} (ctx [< (FT "A", one)]) sone
+        (BV 0) (FT "A") [< one],
+    testTC "1·x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
+      checkQ {n = 1} (ctx [< (FT "A", one)]) sone (BVT 0) (FT "A") [< one],
+    note "f2 : A ⊸ A ⊸ A",
+    testTC "ω·x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
+      inferAsQ {n = 1} (ctx [< (FT "A", Any)]) sone
+        (F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any],
+    note #"("0·x : A ⊢ 1 · x ⇒ A" won't fail because"#,
+    note  " a var's quantity is only checked once it leaves scope)"
   ],
 
   "lambda" :- [
@@ -132,11 +203,31 @@ tests = "typechecker" :- [
       check_ (ctx [<]) sone reflDef reflTy
   ],
 
+  "equalities" :- [
+    testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
+      check_ (ctx [<]) sone (DLam "i" $ DUnused $ FT "a")
+        (Eq0 (FT "A") (FT "a") (FT "a")),
+    testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
+      check_ (ctx [<]) szero
+        (Lam "p" $ TUsed $ Lam "q" $ TUnused $
+         DLam "i" $ DUnused $ BVT 0)
+        (Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
+         Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
+         Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
+    testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
+      check_ (ctx [<]) szero
+        (Lam "p" $ TUnused $ Lam "q" $ TUsed $
+         DLam "i" $ DUnused $ BVT 0)
+        (Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
+         Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
+         Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
+  ],
+
   "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)",
+    note "  ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
     testTC "cong" $
       check_ (ctx [<]) sone
         (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
@@ -146,10 +237,10 @@ tests = "typechecker" :- [
          Eq "i" (DUsed $ 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 "ω·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",
+    note "  ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
     testTC "funext" $
       check_ (ctx [<]) sone
         (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))