split check and checkType. UAny is kill

lib/Quox/Equal.idr

@@ -31,6 +31,10 @@ private %inline
 clashT : CanEqual q m => Term q d n -> Term q d n -> Term q d n -> m a
 clashT ty s t = throwError $ ClashT !mode ty s t
 
+private %inline
+clashTy : CanEqual q m => Term q d n -> Term q d n -> m a
+clashTy s t = throwError $ ClashTy !mode s t
+
 private %inline
 clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a
 clashE e f = throwError $ ClashE !mode e f
@@ -213,7 +217,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       Element t nt <- whnfT defs t
       ts <- ensureTyCon s
       tt <- ensureTyCon t
-      st <- either pure (const $ clashT (TYPE UAny) s t) $
+      st <- either pure (const $ clashTy s t) $
             nchoose $ sameTyCon s t
       compareType' ctx s t
 
@@ -266,7 +270,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       --
       -- no subtyping based on tag subsets, since that would need
       -- a runtime coercion
-      unless (tags1 == tags2) $ clashT (TYPE UAny) s t
+      unless (tags1 == tags2) $ clashTy s t
 
     compareType' ctx (E e) (E f) = do
       -- no fanciness needed here cos anything other than a neutral

lib/Quox/Syntax/Universe.idr

@@ -9,22 +9,18 @@ import Derive.Prelude
 %language ElabReflection
 
 
-||| `UAny` doesn't show up in programs, but when checking something is
-||| just some type (e.g. in a signature) it's checked against `Star UAny`
 public export
-data Universe = U Nat | UAny
+data Universe = U Nat
 %name Universe l
 
 %runElab derive "Universe" [Eq, Ord, Show]
 
 export
 PrettyHL Universe where
-  prettyM UAny  = pure $ hl Delim "_"
   prettyM (U l) = pure $ hl Free $ pretty l
 
 export
 prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL)
-prettyUnivSuffix UAny  = ifUnicode "_" "₋"
 prettyUnivSuffix (U l) =
   ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l)
  where

lib/Quox/Typechecker.idr

@@ -61,6 +61,24 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       let Element subj nc = pushSubsts subj in
       check' ctx sg subj ty
 
+  ||| "Ψ | Γ ⊢₀ s ⇐ ★ᵢ"
+  |||
+  ||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the
+  ||| universe doesn't matter, only that a term is _a_ type, so it is optional.
+  export covering %inline
+  checkType : TyContext q d n -> Term q d n -> Maybe Universe -> m ()
+  checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
+
+  export covering %inline
+  checkTypeC : TyContext q d n -> Term q d n -> Maybe Universe -> m ()
+  checkTypeC ctx subj l =
+    wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l
+
+  export covering %inline
+  checkTypeNoWrap : TyContext q d n -> Term q d n -> Maybe Universe -> m ()
+  checkTypeNoWrap ctx subj l =
+    let Element subj nc = pushSubsts subj in
+    checkType' ctx subj l
 
   ||| "Ψ | Γ ⊢ σ · e ⇒ A ⊳ Σ"
   |||
@@ -84,29 +102,24 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       infer' ctx sg subj
 
 
+  private covering
+  toCheckType : TyContext q d n -> SQty q ->
+                (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
+                m (CheckResult' q n)
+  toCheckType ctx sg t ty = do
+    u <- expectTYPE !ask ty
+    expectEqualQ zero sg.fst
+    checkTypeNoWrap ctx t (Just u)
+    pure $ zeroFor ctx
+
   private covering
   check' : TyContext q d n -> SQty q ->
            (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
            m (CheckResult' q n)
 
-  check' ctx sg (TYPE k) ty = do
+  check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty
-    -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
-    l <- expectTYPE !ask ty
-    expectEqualQ zero sg.fst
-    unless (k < l) $ throwError $ BadUniverse k l
-    pure $ zeroFor ctx
 
-  check' ctx sg (Pi qty arg res) ty = do
+  check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
-    l <- expectTYPE !ask ty
-    expectEqualQ zero sg.fst
-    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
-    check0 ctx arg (TYPE l)
-    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
-    case res.body of
-      Y res => check0 (extendTy arg ctx) res (TYPE l)
-      N res => check0 ctx res (TYPE l)
-    -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
-    pure $ zeroFor ctx
 
   check' ctx sg (Lam body) ty = do
     (qty, arg, res) <- expectPi !ask ty
@@ -117,17 +130,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
     popQ qty' qout
 
-  check' ctx sg (Sig fst snd) ty = do
+  check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
-    l <- expectTYPE !ask ty
-    expectEqualQ zero sg.fst
-    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
-    check0 ctx fst (TYPE l)
-    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
-    case snd.body of
-      Y snd => check0 (extendTy fst ctx) snd (TYPE l)
-      N snd => check0 ctx snd (TYPE l)
-    -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
-    pure $ zeroFor ctx
 
   check' ctx sg (Pair fst snd) ty = do
     (tfst, tsnd) <- expectSig !ask ty
@@ -139,11 +142,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
     pure $ qfst + qsnd
 
-  check' ctx sg (Enum _) ty = do
+  check' ctx sg t@(Enum _) ty = toCheckType ctx sg t ty
-    -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
-    ignore $ expectTYPE !ask ty
-    expectEqualQ zero sg.fst
-    pure $ zeroFor ctx
 
   check' ctx sg (Tag t) ty = do
     tags <- expectEnum !ask ty
@@ -152,19 +151,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
     pure $ zeroFor ctx
 
-  check' ctx sg (Eq t l r) ty = do
+  check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
-    u <- expectTYPE !ask ty
-    expectEqualQ zero sg.fst
-    -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
-    case t.body of
-      Y t => check0 (extendDim ctx) t (TYPE u)
-      N t => check0 ctx t (TYPE u)
-    -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
-    check0 ctx t.zero l
-    -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
-    check0 ctx t.one  r
-    -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
-    pure $ zeroFor ctx
 
   check' ctx sg (DLam body) ty = do
     (ty, l, r) <- expectEq !ask ty
@@ -185,6 +172,71 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
     pure infres.qout
 
+  private covering
+  checkType' : TyContext q d n ->
+               (subj : Term q d n) -> (0 nc : NotClo subj) =>
+               Maybe Universe -> m ()
+
+  checkType' ctx (TYPE k) u = do
+    -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
+    case u of
+      Just l  => unless (k < l) $ throwError $ BadUniverse k l
+      Nothing => pure ()
+
+  checkType' ctx (Pi qty arg res) u = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
+    checkTypeC ctx arg u
+    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
+    case res.body of
+      Y res => checkTypeC (extendTy arg ctx) res u
+      N res => checkTypeC ctx                res u
+    -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
+
+  checkType' ctx t@(Lam {}) u =
+    throwError $ NotType t
+
+  checkType' ctx (Sig fst snd) u = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
+    checkTypeC ctx fst u
+    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
+    case snd.body of
+      Y snd => checkTypeC (extendTy fst ctx) snd u
+      N snd => checkTypeC ctx                snd u
+    -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
+
+  checkType' ctx t@(Pair {}) u =
+    throwError $ NotType t
+
+  checkType' ctx (Enum _) u = pure ()
+    -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
+
+  checkType' ctx t@(Tag {}) u =
+    throwError $ NotType t
+
+  checkType' ctx (Eq t l r) u = do
+    -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
+    case t.body of
+      Y t => checkTypeC (extendDim ctx) t u
+      N t => checkTypeC ctx             t u
+    -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
+    check0 ctx t.zero l
+    -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
+    check0 ctx t.one  r
+    -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
+
+  checkType' ctx t@(DLam {}) u =
+    throwError $ NotType t
+
+  checkType' ctx (E e) u = do
+    -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
+    infres <- inferC ctx szero e
+    -- if Ψ | Γ ⊢ A' <: A
+    case u of
+      Just u  => subtype ctx infres.type (TYPE u)
+      Nothing => ignore $ expectTYPE !ask infres.type
+    -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
+
+
   private covering
   infer' : TyContext q d n -> SQty q ->
            (subj : Elim q d n) -> (0 nc : NotClo subj) =>
@@ -231,7 +283,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
-    check0 (extendTy pairres.type ctx) ret.term (TYPE UAny)
+    checkTypeC (extendTy pairres.type ctx) ret.term Nothing
     (tfst, tsnd) <- expectSig !ask pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
@@ -252,7 +304,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
-    check0 (extendTy tres.type ctx) ret.term (TYPE UAny)
+    checkTypeC (extendTy tres.type ctx) ret.term Nothing
     -- if for each "a ⇒ s" in arms,
     --   Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂
     -- for fixed Σ₂
@@ -280,7 +332,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
 
   infer' ctx sg (term :# type) = do
     -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
-    check0 ctx type (TYPE UAny)
+    checkTypeC ctx type Nothing
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     qout <- checkC ctx sg term type
     -- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ

lib/Quox/Typing.idr

@@ -117,6 +117,7 @@ data Error q
 
 -- first arg of ClashT is the type
 | ClashT  EqMode (Term q d n) (Term q d n) (Term q d n)
+| ClashTy EqMode (Term q d n) (Term q d n)
 | ClashE  EqMode (Elim q d n) (Elim q d n)
 | ClashU  EqMode Universe     Universe
 | ClashQ        q            q
@@ -132,6 +133,11 @@ data Error q
     (Term q d n) -- term
     (Term q d n) -- type
     (Error q)
+| WhileCheckingTy
+    (TyContext q d n)
+    (Term q d n)
+    (Maybe Universe)
+    (Error q)
 | WhileInferring
     (TyContext q d n) q
     (Elim q d n)

tests/Tests/Typechecker.idr

@@ -141,6 +141,9 @@ check_ : TyContext Three d n -> SQty Three ->
          Term Three d n -> Term Three d n -> M ()
 check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
 
+checkType_ : TyContext Three d n -> Term Three d n -> Maybe Universe -> M ()
+checkType_ ctx s u = inj $ checkType ctx s u
+
 
 -- ω is not a subject qty
 failing "Can't find an implementation"
@@ -155,14 +158,22 @@ export
 tests : Test
 tests = "typechecker" :- [
   "universes" :- [
-    testTC "0 · ★₀ ⇐ ★₁" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 1),
+    testTC "0 · ★₀ ⇐ ★₁  # by checkType" $
-    testTC "0 · ★₀ ⇐ ★₂" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 2),
+      checkType_ (ctx [<]) (TYPE 0) (Just 1),
-    testTC "0 · ★₀ ⇐ ★_" $ check_ (ctx [<]) szero (TYPE 0) (TYPE UAny),
+    testTC "0 · ★₀ ⇐ ★₁  # by check" $
-    testTCFail "0 · ★₁ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 1) (TYPE 0),
+      check_ (ctx [<]) szero (TYPE 0) (TYPE 1),
-    testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0),
+    testTC "0 · ★₀ ⇐ ★₂" $
-    testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny),
+      checkType_ (ctx [<]) (TYPE 0) (Just 2),
-    testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1),
+    testTC "0 · ★₀ ⇐ ★_" $
-    testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $ check_ (ctx01 [<]) szero (TYPE 1) (TYPE 0)
+      checkType_ (ctx [<]) (TYPE 0) Nothing,
+    testTCFail "0 · ★₁ ⇍ ★₀" $
+      checkType_ (ctx [<]) (TYPE 1) (Just 0),
+    testTCFail "0 · ★₀ ⇍ ★₀" $
+      checkType_ (ctx [<]) (TYPE 0) (Just 0),
+    testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
+      checkType_ (ctx01 [<]) (TYPE 1) (Just 0),
+    testTCFail "1 · ★₀ ⇍ ★₁  # by check" $
+      check_ (ctx [<]) sone (TYPE 0) (TYPE 1)
   ],
 
   "function types" :- [

tests/TypingImpls.idr

@@ -50,6 +50,11 @@ PrettyHL q => ToInfo (Error q) where
      ("ty",    prettyStr True ty),
      ("left",  prettyStr True s),
      ("right", prettyStr True t)]
+  toInfo (ClashTy mode s t) =
+    [("type",  "ClashTy"),
+     ("mode",  show mode),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
   toInfo (ClashE mode e f) =
     [("type",  "ClashE"),
      ("mode",  show mode),
@@ -79,6 +84,7 @@ PrettyHL q => ToInfo (Error q) where
 
   -- [todo] add nested yamls to TAP and include context here
   toInfo (WhileChecking   _ _ _ _   err) = toInfo err
+  toInfo (WhileCheckingTy _ _ _     err) = toInfo err
   toInfo (WhileInferring  _ _ _     err) = toInfo err
   toInfo (WhileComparingT _ _ _ _ _ err) = toInfo err
   toInfo (WhileComparingE _ _ _ _   err) = toInfo err