more typed equality, uip, etc

lib/Quox/Equal.idr

@@ -43,17 +43,31 @@ clashE e f = throwError $ ClashE !mode e f
 
 
 public export %inline
-isType : (t : Term {}) -> Bool
+isTyCon : (t : Term {}) -> Bool
-isType (TYPE  {}) = True
+isTyCon (TYPE  {}) = True
-isType (Pi    {}) = True
+isTyCon (Pi    {}) = True
-isType (Lam   {}) = False
+isTyCon (Lam   {}) = False
-isType (Sig   {}) = True
+isTyCon (Sig   {}) = True
-isType (Pair  {}) = False
+isTyCon (Pair  {}) = False
-isType (Eq    {}) = True
+isTyCon (Eq    {}) = True
-isType (DLam  {}) = False
+isTyCon (DLam  {}) = False
-isType (E     {}) = True
+isTyCon (E     {}) = True
-isType (CloT  {}) = False
+isTyCon (CloT  {}) = False
-isType (DCloT {}) = False
+isTyCon (DCloT {}) = False
+
+private
+isSubSing : Term {} -> Bool
+isSubSing ty =
+  let Element ty _ = pushSubsts ty in
+  case ty of
+    TYPE _            => False
+    Pi {res, _}       => isSubSing res.term
+    Lam {}            => False
+    Sig {fst, snd, _} => isSubSing fst && isSubSing snd.term
+    Pair {}           => False
+    Eq {}             => True
+    DLam {}           => False
+    E e               => False
 
 
 parameters {auto _ : HasErr q m}
@@ -64,8 +78,8 @@ parameters {auto _ : HasErr q m}
     Right n => throwError $ e t
 
   export %inline
-  ensureType : (t : Term q d n) -> m (So (isType t))
+  ensureType : (t : Term q d n) -> m (So (isTyCon t))
-  ensureType = ensure NotType isType
+  ensureType = ensure NotType isTyCon
 
 parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
   mutual
@@ -88,7 +102,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       private covering
       compare0' : TContext q 0 n ->
                   (ty, s, t : Term q 0 n) ->
-                  (0 nty : NotRedex defs ty) => (0 tty : So (isType ty)) =>
+                  (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
                   (0 ns  : NotRedex defs s)  => (0 nt  : NotRedex defs t) =>
                   m ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
@@ -103,7 +117,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           (Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
           (E e,      Lam _ b)  => eta e b
           (Lam _ b,  E e)      => eta e b
-          (E e,      E f)      => ignore $ compare0 ctx e f
+          (E e,      E f)      => compare0 ctx e f
           _ => throwError $ WrongType ty s t
 
       compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
@@ -123,7 +137,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
         -- e.g. an abstract value in an abstract type, bound variables, …
         E e <- pure s | _ => throwError $ WrongType ty s t
         E f <- pure t | _ => throwError $ WrongType ty s t
-        ignore $ compare0 ctx e f
+        compare0 ctx e f
 
     export covering
     compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
@@ -136,8 +150,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
 
     private covering
     compareType' : TContext q 0 n -> (s, t : Term q 0 n) ->
-                   (0 ns : NotRedex defs s) => (0 ts : So (isType s)) =>
+                   (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
-                   (0 nt : NotRedex defs t) => (0 tt : So (isType t)) =>
+                   (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
                    m ()
     compareType' ctx s t = do
       let err : m () = clashT (TYPE UAny) s t
@@ -170,80 +184,90 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           E f <- pure t | _ => err
           -- no fanciness needed here cos anything other than a neutral
           -- has been inlined by whnfD
-          ignore $ compare0 ctx e f
+          compare0 ctx e f
+
+    ||| assumes the elim is already typechecked! only does the work necessary
+    ||| to calculate the overall type
+    private covering
+    computeElimType : TContext q 0 n -> (e : Elim q 0 n) ->
+                      (0 ne : NotRedex defs e) =>
+                      m (Term q 0 n)
+    computeElimType ctx (F x) = do
+      defs <- lookupFree' defs x
+      pure $ defs.type.get
+    computeElimType ctx (B i) = do
+      pure $ ctx !! i
+    computeElimType ctx (f :@ s) {ne} = do
+      (_, arg, res) <- computeElimType ctx f {ne = noOr1 ne} >>= expectPi defs
+      pure $ sub1 res (s :# arg)
+    computeElimType ctx (CasePair {pair, ret, _}) = do
+      pure $ sub1 ret pair
+    computeElimType ctx (f :% p) {ne} = do
+      (ty, _, _) <- computeElimType ctx f {ne = noOr1 ne} >>= expectEq defs
+      pure $ dsub1 ty p
+    computeElimType ctx (_ :# ty) = do
+      pure ty
+
+    private covering
+    replaceEnd : TContext q 0 n ->
+                 (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
+                 m (Elim q 0 n)
+    replaceEnd ctx e p ne = do
+      (ty, l, r) <- computeElimType ctx e >>= expectEq defs
+      pure $ ends l r p :# dsub1 ty (K p)
 
     namespace Elim
+      -- [fixme] the following code ends up repeating a lot of work in the
+      -- computeElimType calls. the results should be shared better
+
       export covering %inline
-      compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m (Term q 0 n)
+      compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
       compare0 ctx e f =
         let Element e ne = whnfD defs e
             Element f nf = whnfD defs f
         in
-        compare0' ctx e f
+        -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-
+        unless (isSubSing !(computeElimType ctx e)) $ compare0' ctx e f
-      private
-      isSubSing : Term {} -> Bool
-      isSubSing (TYPE _)            = False
-      isSubSing (Pi {res, _})       = isSubSing res.term
-      isSubSing (Lam {})            = False
-      isSubSing (Sig {fst, snd, _}) = isSubSing fst && isSubSing snd.term
-      isSubSing (Pair {})           = False
-      isSubSing (Eq {})             = True
-      isSubSing (DLam {})           = False
-      isSubSing (E e)               = False
-      isSubSing (CloT tm th)        = False
-      isSubSing (DCloT tm th)       = False
 
       private covering
       compare0' : TContext q 0 n ->
                   (e, f : Elim q 0 n) ->
                   (0 ne : NotRedex defs e) => (0 nf : NotRedex defs f) =>
-                  m (Term q 0 n)
+                  m ()
-      compare0' _ e@(F x) f@(F y) = do
+      -- replace applied equalities with the appropriate end first
-        d <- lookupFree' defs x
+      -- e.g. e : Eq [i ⇒ A] s t ⊢ e 0 = s : A‹0/i›
-        let ty = d.type
+      compare0' ctx (e :% K p) f {ne} =
-        -- [fixme] there is a better way to do this for sure
+        compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
-        unless (isSubSing ty.get0 || x == y) $ clashE e f
+      compare0' ctx e (f :% K q) {nf} =
-        pure ty.get
+        compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
+
+      compare0' _ e@(F x) f@(F y) = unless (x == y) $ clashE e f
       compare0' _ e@(F _) f = clashE e f
 
-      compare0' ctx e@(B i) f@(B j) = do
+      compare0' ctx e@(B i) f@(B j) = unless (i == j) $ clashE e f
-        let ty = ctx !! i
-        -- [fixme] there is a better way to do this for sure
-        unless (isSubSing ty || i == j) $ clashE e f
-        pure ty
       compare0' _ e@(B _) f = clashE e f
 
-      compare0' ctx (e :@ s) (f :@ t) = local {mode := Equal} $ do
+      compare0' ctx (e :@ s) (f :@ t) {ne} = local {mode := Equal} $ do
-        Pi {arg, res, _} <- compare0 ctx e f
+        compare0 ctx e f
-          | ty => throwError $ ExpectedPi ty
+        (_, arg, _) <- computeElimType ctx e {ne = noOr1 ne} >>= expectPi defs
         compare0 ctx arg s t
-        pure $ sub1 res (s :# arg)
       compare0' _ e@(_ :@ _) f = clashE e f
 
       compare0' ctx (CasePair epi e _ eret _ _ ebody)
-                    (CasePair fpi f _ fret _ _ fbody) =
+                    (CasePair fpi f _ fret _ _ fbody) {ne} =
         local {mode := Equal} $ do
-          ty@(Sig {fst, snd, _}) <- compare0 ctx e f
+          compare0 ctx e f
-            | ty => throwError $ ExpectedSig ty
+          ety <- computeElimType ctx e {ne = noOr1 ne}
-          unless (epi == fpi) $ throwError $ ClashQ epi fpi
+          compareType (ctx :< ety) eret.term fret.term
-          compareType (ctx :< ty) eret.term fret.term
+          (fst, snd) <- expectSig defs ety
-          compare0 (ctx :< fst :< snd.term) (substCasePairRet ty eret)
+          compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
             ebody.term fbody.term
-          pure $ sub1 eret e
+          unless (epi == fpi) $ throwError $ ClashQ epi fpi
       compare0' _ e@(CasePair {}) f = clashE e f
 
-      compare0' ctx (e :% p) (f :% q) = local {mode := Equal} $ do
-        Eq {ty, _} <- compare0 ctx e f
-          | ty => throwError $ ExpectedEq ty
-        unless (p == q) $ throwError $ ClashD p q
-        pure $ dsub1 ty p
-      compare0' _ e@(_ :% _) f = clashE e f
-
       compare0' ctx (s :# a) (t :# b) = do
         compareType ctx a b
         compare0 ctx a s t
-        pure b
       compare0' _ e@(_ :# _) f = clashE e f
 
 
@@ -268,14 +292,15 @@ parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)}
             compareType defs (map (/// th) ctx) (s /// th) (t /// th)
 
     namespace Elim
-      -- can't return the type since it might be different in each dsubst ☹
+      ||| you don't have to pass the type in but the arguments must still be
+      ||| of the same type!!
       export covering %inline
       compare : (e, f : Elim q d n) -> m ()
       compare e f = do
         defs <- ask
         runReaderT {m} (MakeEnv {mode}) $
           for_ (splits eq) $ \th =>
-            ignore $ compare0 defs (map (/// th) ctx) (e /// th) (f /// th)
+            compare0 defs (map (/// th) ctx) (e /// th) (f /// th)
 
   namespace Term
     export covering %inline

lib/Quox/Typechecker.idr

@@ -19,37 +19,6 @@ public export
 CanTC q = CanTC' q IsGlobal
 
 
-private covering %inline
-expectTYPE : CanTC' q _ m => Term q d n -> m Universe
-expectTYPE s =
-  case whnfD !ask s of
-    Element (TYPE l) _ => pure l
-    _ => throwError $ ExpectedTYPE s
-
-private covering %inline
-expectPi : CanTC' q _ m => Term q d n ->
-           m (q, Term q d n, ScopeTerm q d n)
-expectPi ty =
-  case whnfD !ask ty of
-    Element (Pi qty _ arg res) _ => pure (qty, arg, res)
-    _ => throwError $ ExpectedPi ty
-
-private covering %inline
-expectSig : CanTC' q _ m => Term q d n ->
-            m (Term q d n, ScopeTerm q d n)
-expectSig ty =
-  case whnfD !ask ty of
-    Element (Sig _ arg res) _ => pure (arg, res)
-    _ => throwError $ ExpectedSig ty
-
-private covering %inline
-expectEq : CanTC' q _ m => Term q d n ->
-           m (DScopeTerm q d n, Term q d n, Term q d n)
-expectEq ty =
-  case whnfD !ask ty of
-    Element (Eq _ ty l r) _ => pure (ty, l, r)
-    _ => throwError $ ExpectedEq ty
-
 
 private
 popQs : HasErr q m => IsQty q =>
@@ -133,13 +102,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   check' ctx sg (TYPE l) _ ty = do
     -- if ℓ < ℓ' then Ψ | Γ ⊢ Type ℓ · 0 ⇐ Type ℓ' ⊳ 𝟎
-    l' <- expectTYPE ty
+    l' <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     unless (l < l') $ throwError $ BadUniverse l l'
     pure $ zeroFor ctx
 
   check' ctx sg (Pi qty _ arg res) _ ty = do
-    l <- expectTYPE ty
+    l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
     ignore $ check0 ctx arg (TYPE l)
@@ -151,14 +120,14 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     pure $ zeroFor ctx
 
   check' ctx sg (Lam _ body) _ ty = do
-    (qty, arg, res) <- expectPi ty
+    (qty, arg, res) <- expectPi !ask ty
     -- if Ψ | Γ, x · πσ : A ⊢ t · σ ⇐ B ⊳ Σ, x · σπ
     qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
     -- then Ψ | Γ ⊢ λx. t · σ ⇐ (x · π : A) → B ⊳ Σ
     popQ (sg.fst * qty) qout
 
   check' ctx sg (Sig _ fst snd) _ ty = do
-    l <- expectTYPE ty
+    l <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
     ignore $ check0 ctx fst (TYPE l)
@@ -170,7 +139,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     pure $ zeroFor ctx
 
   check' ctx sg (Pair fst snd) _ ty = do
-    (tfst, tsnd) <- expectSig ty
+    (tfst, tsnd) <- expectSig !ask ty
     -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ₁
     qfst <- check ctx sg fst tfst
     let tsnd = sub1 tsnd (fst :# tfst)
@@ -180,7 +149,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     pure $ qfst + qsnd
 
   check' ctx sg (Eq i t l r) _ ty = do
-    u <- expectTYPE ty
+    u <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
     -- if Ψ, i | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
     case t of
@@ -194,7 +163,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     pure $ zeroFor ctx
 
   check' ctx sg (DLam i body) _ ty = do
-    (ty, l, r) <- expectEq ty
+    (ty, l, r) <- expectEq !ask ty
     -- if Ψ, i | Γ ⊢ t · σ ⇐ A ⊳ Σ
     qout <- check (extendDim ctx) sg body.term ty.term
     let eqs = makeDimEq ctx.dctx
@@ -234,7 +203,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   infer' ctx sg (fun :@ arg) _ = do
     -- if Ψ | Γ ⊢ f · σ ⇒ (x · π : A) → B ⊳ Σ₁
     funres <- infer ctx sg fun
-    (qty, argty, res) <- expectPi funres.type
+    (qty, argty, res) <- expectPi !ask funres.type
     -- if Ψ | Γ ⊢ s · σ∧π ⇐ A ⊳ Σ₂
     --   (0∧π = σ∧0 = 0; σ∧π = σ otherwise)
     argout <- check ctx (subjMult sg qty) arg argty
@@ -250,7 +219,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ pair · 1 ⇒ (x : A) × B ⊳ Σ₁
     pairres <- infer ctx sone pair
     ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
-    (tfst, tsnd) <- expectSig pairres.type
+    (tfst, tsnd) <- expectSig !ask pairres.type
     -- if Ψ | Γ, x · π : A, y · π : B ⊢ σ body ⇐ ret[(x, y)]
     --      ⊳ Σ₂, x · π₁, y · π₂
     -- if π₁, π₂ ≤ π
@@ -263,11 +232,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       qout = pi * pairres.qout + bodyout
     }
 
-
   infer' ctx sg (fun :% dim) _ = do
     -- if Ψ | Γ ⊢ f · σ ⇒ Eq [i ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- infer ctx sg fun
-    (ty, _, _) <- expectEq type
+    (ty, _, _) <- expectEq !ask type
     -- then Ψ | Γ ⊢ f p · σ ⇒ A‹p› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 

lib/Quox/Typing.idr

@@ -177,3 +177,33 @@ substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
 substCasePairRet dty retty =
   let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
   retty.term // (arg ::: shift 2)
+
+
+parameters {auto _ : HasErr q m} (defs : Definitions' q _)
+  export covering %inline
+  expectTYPE : Term q d n -> m Universe
+  expectTYPE s =
+    case fst $ whnfD defs s of
+      TYPE l => pure l
+      _      => throwError $ ExpectedTYPE s
+
+  export covering %inline
+  expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
+  expectPi s =
+    case fst $ whnfD defs s of
+      Pi {qty, arg, res, _} => pure (qty, arg, res)
+      _                     => throwError $ ExpectedPi s
+
+  export covering %inline
+  expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
+  expectSig s =
+    case fst $ whnfD defs s of
+      Sig {fst, snd, _} => pure (fst, snd)
+      _                 => throwError $ ExpectedSig s
+
+  export covering %inline
+  expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
+  expectEq s =
+    case fst $ whnfD defs s of
+      Eq {ty, l, r, _} => pure (ty, l, r)
+      _                => throwError $ ExpectedEq s

tests/Tests.idr

@@ -1,20 +1,17 @@
 module Tests
 
 import TAP
--- import Tests.Unicode
--- import Tests.Lexer
--- import Tests.Parser
 import Tests.Reduce
 import Tests.Equal
+import Tests.Typechecker
 import System
 
 
+allTests : List Test
 allTests = [
-  -- Unicode.tests,
-  -- Lexer.tests,
-  -- Parser.tests,
   Reduce.tests,
-  Equal.tests
+  Equal.tests,
+  Typechecker.tests
 ]
 
 main = TAP.main !getTestOpts allTests

tests/Tests/Equal.idr

@@ -1,65 +1,10 @@
 module Tests.Equal
 
-import Quox.Equal as Lib
+import Quox.Equal
-import Quox.Pretty
 import Quox.Syntax.Qty.Three
+import public TypingImpls
 import TAP
 
-export
-ToInfo (Error Three) where
-  toInfo (NotInScope x) =
-    [("type", "NotInScope"),
-     ("name", show x)]
-  toInfo (ExpectedTYPE t) =
-    [("type", "ExpectedTYPE"),
-     ("got", prettyStr True t)]
-  toInfo (ExpectedPi t) =
-    [("type", "ExpectedPi"),
-     ("got", prettyStr True t)]
-  toInfo (ExpectedSig t) =
-    [("type", "ExpectedSig"),
-     ("got", prettyStr True t)]
-  toInfo (ExpectedEq t) =
-    [("type", "ExpectedEq"),
-     ("got", prettyStr True t)]
-  toInfo (BadUniverse k l) =
-    [("type", "BadUniverse"),
-     ("low",  show k),
-     ("high", show l)]
-  toInfo (ClashT mode ty s t) =
-    [("type", "ClashT"),
-     ("mode",  show mode),
-     ("ty",    prettyStr True ty),
-     ("left",  prettyStr True s),
-     ("right", prettyStr True t)]
-  toInfo (ClashE mode e f) =
-    [("type", "ClashE"),
-     ("mode",  show mode),
-     ("left",  prettyStr True e),
-     ("right", prettyStr True f)]
-  toInfo (ClashU mode k l) =
-    [("type", "ClashU"),
-     ("mode",  show mode),
-     ("left",  prettyStr True k),
-     ("right", prettyStr True l)]
-  toInfo (ClashQ pi rh) =
-    [("type", "ClashQ"),
-     ("left",  prettyStr True pi),
-     ("right", prettyStr True rh)]
-  toInfo (ClashD p q) =
-    [("type", "ClashD"),
-     ("left",  prettyStr True p),
-     ("right", prettyStr True q)]
-  toInfo (NotType ty) =
-    [("type",   "NotType"),
-     ("actual", prettyStr True ty)]
-  toInfo (WrongType ty s t) =
-    [("type", "WrongType"),
-     ("ty",    prettyStr True ty),
-     ("left",  prettyStr True s),
-     ("right", prettyStr True t)]
-
-
 0 M : Type -> Type
 M = ReaderT (Definitions Three) (Either (Error Three))
 
@@ -68,6 +13,7 @@ defGlobals = fromList
   [("A", mkAbstract Zero $ TYPE 0),
    ("B", mkAbstract Zero $ 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"))]
 
@@ -100,6 +46,7 @@ export
 tests : Test
 tests = "equality & subtyping" :- [
   note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#,
+  note #""s{…}" for term substs; "s‹…›" for dim substs"#,
 
   "universes" :- [
     testEq "★₀ ≡ ★₀" $
@@ -117,8 +64,8 @@ tests = "equality & subtyping" :- [
   ],
 
   "pi" :- [
-    note #""A ⊸ B" for (1 _ : A) → B"#,
+    note #""A ⊸ B" for (1·A) → B"#,
-    note #""A ⇾ B" for (0 _ : A) → B"#,
+    note #""A ⇾ B" for (0·A) → B"#,
     testEq "A ⊸ B ≡ A ⊸ B" $
       let tm = Arr One (FT "A") (FT "B") in
       equalT [<] (TYPE 0) tm tm,
@@ -168,32 +115,31 @@ tests = "equality & subtyping" :- [
   "lambda" :- [
     testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
       equalT [<] (Arr One (FT "A") (FT "A"))
-        (Lam "x" $ TUsed $ BVT 0)
+        (["x"] :\\ BVT 0)
-        (Lam "x" $ TUsed $ BVT 0),
+        (["x"] :\\ BVT 0),
     testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
       subT [<] (Arr One (FT "A") (FT "A"))
-        (Lam "x" $ TUsed $ BVT 0)
+        (["x"] :\\ BVT 0)
-        (Lam "x" $ TUsed $ BVT 0),
+        (["x"] :\\ BVT 0),
     testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $
       equalT [<] (Arr One (FT "A") (FT "A"))
-        (Lam "x" $ TUsed $ BVT 0)
+        (["x"] :\\ BVT 0)
-        (Lam "y" $ TUsed $ BVT 0),
+        (["y"] :\\ BVT 0),
     testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
       equalT [<] (Arr One (FT "A") (FT "A"))
-        (Lam "x" $ TUsed $ BVT 0)
+        (["x"] :\\ BVT 0)
-        (Lam "y" $ TUsed $ BVT 0),
+        (["y"] :\\ BVT 0),
     testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $
       equalT [<] (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
-        (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1)
+        (["x", "y"] :\\ BVT 1)
-        (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0),
+        (["x", "y"] :\\ BVT 0),
     testEq "λ x ⇒ [a] ≡ λ x ⇒ [a]  (TUsed vs TUnused)" $
       equalT [<] (Arr Zero (FT "B") (FT "A"))
         (Lam "x" $ TUsed   $ FT "a")
         (Lam "x" $ TUnused $ FT "a"),
-    skipWith "(no η yet)" $
     testEq "λ x ⇒ [f [x]] ≡ [f]  (η)" $
       equalT [<] (Arr One (FT "A") (FT "A"))
-        (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0)
+        (["x"] :\\ E (F "f" :@ BVT 0))
         (FT "f")
   ],
 
@@ -208,7 +154,23 @@ tests = "equality & subtyping" :- [
         (Eq0 (FT "A") (TYPE 0) (TYPE 0))
   ],
 
-  todo "dim lambda",
+  "equalities" :-
+  let refl : Term q d n -> Term q d n -> Elim q d n
+      refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x)
+  in
+  [
+    note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
+    testEq "refl [A] a ≡ refl [A] a" $
+      equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
+    testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ⊢ p ≡ q  (free)"
+           {globals =
+              let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
+              defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
+      equalE [<] (F "p") (F "q"),
+    testEq "x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x ≡ y  (bound)" $
+      let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in
+      equalE [< ty, ty] (BV 0) (BV 1) {n = 2}
+  ],
 
   "term closure" :- [
     note "𝑖, 𝑗 for bound variables pointing outside of the current expr",
@@ -230,8 +192,8 @@ tests = "equality & subtyping" :- [
         (Lam "y" $ TUnused $ FT "a"),
     testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a]  (TUsed)" $
       equalT [<] (Arr Zero (FT "B") (FT "A"))
-        (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id))
+        (CloT (["y"] :\\ BVT 1) (F "a" ::: id))
-        (Lam "y" $ TUsed $ FT "a")
+        (["y"] :\\ FT "a")
   ],
 
   todo "term d-closure",
@@ -290,48 +252,29 @@ tests = "equality & subtyping" :- [
       subE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
       equalE [<]
-        ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
+        (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
-          :@ FT "a")
         (E (FT "a" :# FT "A") :# FT "A"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a  (βυ)" $
       equalE [<]
-        ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
+        (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
-          :@ FT "a")
         (F "a"),
     testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [a]  (β↘↙)" $
       let a = FT "A"; a2a = (Arr One a a) in
       equalE [<]
-        ((Lam "g" (TUsed (E (BV 0 :@ FT "a"))) :# Arr One a2a a) :@ FT "f")
+        (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
-        ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "a"),
+        (((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
     testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
       subE [<]
-        ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
+        (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
-          :@ FT "a")
         (F "a"),
     testEq "id : A ⊸ A ≔ λ x ⇒ [x] ⊢ id [a] ≡ a"
            {globals = defGlobals `mergeLeft` fromList
               [("id", mkDef Any (Arr One (FT "A") (FT "A"))
-                               (Lam "x" (TUsed (BVT 0))))]} $
+                                (["x"] :\\ BVT 0))]} $
       equalE [<] (F "id" :@ FT "a") (F "a")
   ],
 
-  "dim application" :-
+  todo "dim application",
-  let refl : Term q d n -> Term q d n -> Elim q d n
-      refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x)
-  in
-  [
-    note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
-    testEq "refl [A] a ≡ refl [A] a" $
-      equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
-    testEq "p : (a ≡ b : A), q : (a ≡ b : A) ⊢ p ≡ q"
-           {globals =
-              let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "b") in
-              fromList [("A", mkAbstract Zero $ TYPE 0),
-                        ("a", mkAbstract Any  $ FT "A"),
-                        ("b", mkAbstract Any  $ FT "A"),
-                        ("p", def), ("q", def)]} $
-      equalE [<] (F "p") (F "q")
-  ],
 
   todo "annotation",
 

tests/Tests/Typechecker.idr

@@ -0,0 +1,138 @@
+module Tests.Typechecker
+
+import Quox.Syntax
+import Quox.Syntax.Qty.Three
+import Quox.Typechecker as Lib
+import public TypingImpls
+import TAP
+
+
+0 M : Type -> Type
+M = ReaderT (Definitions Three) $ Either (Error Three)
+
+
+
+reflTy : IsQty q => Term q d n
+reflTy =
+  Pi zero "A" (TYPE 0) $ TUsed $
+  Pi zero "x" (BVT 0)  $ TUsed $
+  Eq0 (BVT 1) (BVT 0) (BVT 0)
+
+reflDef : IsQty q => Term q d n
+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),
+   ("a", mkAbstract Any  $ FT "A"),
+   ("b", mkAbstract Any  $ FT "B"),
+   ("f", mkAbstract Any  $ Arr One (FT "A") (FT "A")),
+   ("refl", mkDef Any reflTy reflDef)]
+
+parameters (label : String) (act : Lazy (M ()))
+           {default defGlobals globals : Definitions Three}
+  testTC : Test
+  testTC = test label $ runReaderT globals act
+
+  testTCFail : Test
+  testTCFail = testThrows label (const True) $ runReaderT globals act
+
+
+ctxWith : DContext d -> Context (\i => (Term Three d i, Three)) n ->
+          TyContext Three d n
+ctxWith dctx tqctx =
+  let (tctx, qctx) = unzip tqctx in MkTyContext {dctx, tctx, qctx}
+
+ctx : Context (\i => (Term Three 0 i, Three)) n -> TyContext Three 0 n
+ctx = ctxWith DNil
+
+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)
+
+infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
+infer_ ctx sg e = ignore $ infer ctx sg e
+
+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
+
+export
+tests : Test
+tests = "typechecker" :- [
+  "universes" :- [
+    testTC "0 · ★₀ ⇐ ★₁" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 1),
+    testTC "0 · ★₀ ⇐ ★₂" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 2),
+    testTC "0 · ★₀ ⇐ ★_" $ check_ (ctx [<]) szero (TYPE 0) (TYPE UAny),
+    testTCFail "0 · ★₁ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 1) (TYPE 0),
+    testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0),
+    testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny),
+    testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1)
+  ],
+
+  "function types" :- [
+    note "A, B : ★₀;  C, D : ★₁",
+    testTC "0 · (1·A) → B ⇐ ★₀" $
+      check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
+    testTC "0 · (1·A) → B ⇐ ★₁👈" $
+      check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 1),
+    testTC "0 · (1·C) → D ⇐ ★₁" $
+      check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
+    testTCFail "0 · (1·C) → D ⇍ ★₀" $
+      check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0)
+  ],
+
+  "free vars" :- [
+    testTC "0 · A ⇒ ★₀" $
+      inferAs (ctx [<]) szero (F "A") (TYPE 0),
+    testTC "0 · A ⇐👈 ★₀" $
+      check_ (ctx [<]) szero (FT "A") (TYPE 0),
+    testTC "0 · A ⇐ ★₁👈" $
+      check_ (ctx [<]) szero (FT "A") (TYPE 1),
+    testTCFail "1👈 · A ⇏ ★₀" $
+      infer_ (ctx [<]) sone (F "A"),
+    note "refl : (0·A : ★₀) → (0·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
+    testTC "1 · refl ⇒ {type of refl}" $
+      inferAs (ctx [<]) sone (F "refl") reflTy,
+    testTC "1 · refl ⇐ {type of refl}" $
+      check_ (ctx [<]) sone (FT "refl") reflTy
+  ],
+
+  "lambda" :- [
+    testTC #"1 · (λ A x ⇒ refl A x) ⇐ {type of refl, see "free vars"}"# $
+      check_ (ctx [<]) sone
+        (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
+        reflTy
+  ],
+
+  "misc" :- [
+    testTC "funext"
+           {globals = fromList
+              [("A", mkAbstract Zero $ TYPE 0),
+               ("B", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
+               ("f", mkAbstract Any  $
+                  Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0),
+               ("g", mkAbstract Any  $
+                  Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0)]} $
+      -- 0·A : Type, 0·B : ω·A → Type,
+      -- ω·f, g : (ω·x : A) → B x
+      -- ⊢
+      -- 0·funext : (ω·eq : (0·x : A) → f x ≡ g x) → f ≡ g
+      --          = λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i
+      check_ (ctx [<]) szero
+        (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
+        (Pi Any "eq"
+            (Pi Zero "x" (FT "A") $ TUsed $
+              Eq0 (E $ F "B" :@ BVT 0)
+                  (E $ F "f" :@ BVT 0) (E $ F "g" :@ BVT 0)) $ TUsed $
+         Eq0 (Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0)
+             (FT "f") (FT "g"))
+  ]
+]

tests/TypingImpls.idr

@@ -0,0 +1,61 @@
+module TypingImpls
+
+import TAP
+import public Quox.Typing
+import public Quox.Pretty
+
+export
+PrettyHL q => ToInfo (Error q) where
+  toInfo (NotInScope x) =
+    [("type", "NotInScope"),
+     ("name", show x)]
+  toInfo (ExpectedTYPE t) =
+    [("type", "ExpectedTYPE"),
+     ("got", prettyStr True t)]
+  toInfo (ExpectedPi t) =
+    [("type", "ExpectedPi"),
+     ("got", prettyStr True t)]
+  toInfo (ExpectedSig t) =
+    [("type", "ExpectedSig"),
+     ("got", prettyStr True t)]
+  toInfo (ExpectedEq t) =
+    [("type", "ExpectedEq"),
+     ("got", prettyStr True t)]
+  toInfo (BadUniverse k l) =
+    [("type", "BadUniverse"),
+     ("low",  show k),
+     ("high", show l)]
+  toInfo (ClashT mode ty s t) =
+    [("type", "ClashT"),
+     ("mode",  show mode),
+     ("ty",    prettyStr True ty),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
+  toInfo (ClashE mode e f) =
+    [("type", "ClashE"),
+     ("mode",  show mode),
+     ("left",  prettyStr True e),
+     ("right", prettyStr True f)]
+  toInfo (ClashU mode k l) =
+    [("type", "ClashU"),
+     ("mode",  show mode),
+     ("left",  prettyStr True k),
+     ("right", prettyStr True l)]
+  toInfo (ClashQ pi rh) =
+    [("type", "ClashQ"),
+     ("left",  prettyStr True pi),
+     ("right", prettyStr True rh)]
+  toInfo (ClashD p q) =
+    [("type", "ClashD"),
+     ("left",  prettyStr True p),
+     ("right", prettyStr True q)]
+  toInfo (NotType ty) =
+    [("type",   "NotType"),
+     ("actual", prettyStr True ty)]
+  toInfo (WrongType ty s t) =
+    [("type", "WrongType"),
+     ("ty",    prettyStr True ty),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
+
+

tests/quox-tests.ipkg

@@ -6,5 +6,7 @@ executable = quox-tests
 main = Tests
 modules =
   TermImpls,
+  TypingImpls,
   Tests.Reduce,
-  Tests.Equal
+  Tests.Equal,
+  Tests.Typechecker