add enums, which also need whnf to be fallible :(

lib/Quox/Equal.idr

@@ -1,5 +1,6 @@
 module Quox.Equal
 
+import Quox.BoolExtra
 import public Quox.Typing
 import public Control.Monad.Either
 import public Control.Monad.Reader
@@ -47,6 +48,8 @@ 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 (E     {}) = True
@@ -63,6 +66,8 @@ sameTyCon (Pi   {}) (Pi   {}) = True
 sameTyCon (Pi   {}) _         = False
 sameTyCon (Sig  {}) (Sig  {}) = True
 sameTyCon (Sig  {}) _         = False
+sameTyCon (Enum {}) (Enum {}) = True
+sameTyCon (Enum {}) _         = False
 sameTyCon (Eq   {}) (Eq   {}) = True
 sameTyCon (Eq   {}) _         = False
 sameTyCon (E    {}) (E    {}) = True
@@ -78,20 +83,23 @@ parameters (defs : Definitions' q g)
   ||| * a pair type is a subsingleton if both its elements are.
   ||| * all equality types are subsingletons because uip is admissible by
   |||   boundary separation.
+  ||| * an enum type is a subsingleton if it has zero or one tags.
   public export
-  isSubSing : Term q 0 n -> Bool
+  isSubSing : HasErr q m => Term q 0 n -> m Bool
-  isSubSing ty =
+  isSubSing ty = do
-    let Element ty nc = whnf defs ty in
+    Element ty nc <- whnfT defs ty
     case ty of
-      TYPE _          => False
+      TYPE _          => pure False
       Pi   {res, _}   => isSubSing res.term
-      Lam  {}         => False
+      Lam  {}         => pure False
-      Sig  {fst, snd} => isSubSing fst && isSubSing snd.term
+      Sig  {fst, snd} => isSubSing fst <&&> isSubSing snd.term
-      Pair {}         => False
+      Pair {}         => pure False
-      Eq   {}         => True
+      Enum tags       => pure $ length (SortedSet.toList tags) <= 1
-      DLam {}         => False
+      Tag  {}         => pure False
+      Eq   {}         => pure True
+      DLam {}         => pure False
       E    (s :# _)   => isSubSing s
-      E    _          => False
+      E    _          => pure False
 
 
 parameters {auto _ : HasErr q m}
@@ -116,9 +124,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
       compare0 ctx ty s t =
         wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do
-          let Element ty nty = whnf defs ty
+          Element ty nty <- whnfT defs ty
-              Element s  ns  = whnf defs s
+          Element s  ns  <- whnfT defs s
-              Element t  nt  = whnf defs t
+          Element t  nt  <- whnfT defs t
           tty <- ensureTyCon ty
           compare0' ctx ty s t
 
@@ -170,6 +178,17 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
             compare0 ctx fst sFst tFst
             compare0 ctx (sub1 snd (sFst :# fst)) sSnd tSnd
 
+          (E e, E f) => compare0 ctx e f
+          _ => throwError $ WrongType ty s t
+
+      compare0' ctx ty@(Enum tags) s t = local {mode := Equal} $
+        case (s, t) of
+          -- --------------------
+          --  Γ ⊢ `t = `t : {ts}
+          --
+          -- t ∈ ts is in the typechecker, not here, ofc
+          (Tag t1, Tag t2) => unless (t1 == t2) $ clashT ty s t
+          (E e,    E f)    => compare0 ctx e f
           _                => throwError $ WrongType ty s t
 
       compare0' _ (Eq {}) _ _ =
@@ -190,8 +209,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
     export covering %inline
     compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
     compareType ctx s t = do
-      let Element s ns = whnf defs s
+      Element s ns <- whnfT defs s
-          Element t nt = whnf defs t
+      Element t nt <- whnfT defs t
       ts <- ensureTyCon s
       tt <- ensureTyCon t
       st <- either pure (const $ clashT (TYPE UAny) s t) $
@@ -241,6 +260,14 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
         Term.compare0 ctx sTy.zero sl tl
         Term.compare0 ctx sTy.one  sr tr
 
+    compareType' ctx s@(Enum tags1) t@(Enum tags2) = do
+      -- ------------------
+      --  Γ ⊢ {ts} <: {ts}
+      --
+      -- no subtyping based on tag subsets, since that would need
+      -- a runtime coercion
+      unless (tags1 == tags2) $ clashT (TYPE UAny) s t
+
     compareType' ctx (E e) (E f) = do
       -- no fanciness needed here cos anything other than a neutral
       -- has been inlined by whnf
@@ -263,6 +290,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       pure $ sub1 res (s :# arg)
     computeElimType ctx (CasePair {pair, ret, _}) _ = do
       pure $ sub1 ret pair
+    computeElimType ctx (CaseEnum {tag, ret, _}) _ = do
+      pure $ sub1 ret tag
     computeElimType ctx (f :% p) ne = do
       (ty, _, _) <- expectEq defs !(computeElimType ctx f (noOr1 ne))
       pure $ dsub1 ty p
@@ -289,10 +318,10 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
       compare0 ctx e f =
         wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do
-          let Element e ne = whnf defs e
+          Element e ne <- whnfT defs e
-              Element f nf = whnf defs f
+          Element f nf <- whnfT defs f
           -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-          unless (isSubSing defs !(computeElimType ctx e ne)) $
+          unless !(isSubSing defs !(computeElimType ctx e ne)) $
             compare0' ctx e f ne nf
 
       private covering
@@ -331,9 +360,26 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           (fst, snd) <- expectSig defs ety
           Term.compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
             ebody.term fbody.term
-          unless (epi == fpi) $ throwError $ ClashQ epi fpi
+          expectEqualQ epi fpi
       compare0' _ e@(CasePair {}) f _ _ = clashE e f
 
+      compare0' ctx (CaseEnum epi e eret earms)
+                    (CaseEnum fpi f fret farms) ne nf =
+        local {mode := Equal} $ do
+          compare0 ctx e f
+          ety <- computeElimType ctx e (noOr1 ne)
+          compareType (ctx :< ety) eret.term fret.term
+          for_ !(expectEnum defs ety) $ \t =>
+            compare0 ctx (sub1 eret $ Tag t :# ety)
+              !(lookupArm t earms) !(lookupArm t farms)
+          expectEqualQ epi fpi
+        where
+          lookupArm : TagVal -> CaseEnumArms q d n -> m (Term q d n)
+          lookupArm t arms = case lookup t arms of
+            Just arm => pure arm
+            Nothing  => throwError $ TagNotIn t (fromList $ keys arms)
+      compare0' _ e@(CaseEnum {}) f _ _ = clashE e f
+
       compare0' ctx (s :# a) (t :# b) _ _ =
           Term.compare0 ctx !(bigger a b) s t
         where

lib/Quox/Pretty.idr

@@ -35,6 +35,7 @@ data HL
 | Dim  | DVar | DVarErr
 | Qty
 | Syntax
+| Tag
 %runElab derive "HL" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 public export
@@ -212,6 +213,7 @@ termHL DVarErr = color BrightGreen   <+> underline
 termHL Qty     = color BrightMagenta <+> bold
 termHL Free    = color BrightWhite
 termHL Syntax  = color BrightCyan
+termHL Tag     = color BrightBlue
 
 export %inline
 prettyTerm : PrettyOpts -> PrettyHL a => a -> IO Unit

lib/Quox/Reduce.idr

@@ -5,6 +5,7 @@ import Quox.Syntax
 import Quox.Definition
 import Data.Vect
 import Data.Maybe
+import Data.List
 
 %default total
 
@@ -71,6 +72,10 @@ mutual
       nclo $ Sig (a // th // ph) (b // th // ph)
     pushSubstsWith th ph (Pair s t) =
       nclo $ Pair (s // th // ph) (t // th // ph)
+    pushSubstsWith th ph (Enum tags) =
+      nclo $ Enum tags
+    pushSubstsWith th ph (Tag tag) =
+      nclo $ Tag tag
     pushSubstsWith th ph (Eq ty l r) =
       nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph)
     pushSubstsWith th ph (DLam body) =
@@ -95,6 +100,9 @@ mutual
       nclo $ (f // th // ph) :@ (s // th // ph)
     pushSubstsWith th ph (CasePair pi p r b) =
       nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph)
+    pushSubstsWith th ph (CaseEnum pi t r arms) =
+      nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
+               (map (\b => b // th // ph) arms)
     pushSubstsWith th ph (f :% d) =
       nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =
@@ -106,29 +114,39 @@ mutual
 
 
 
+||| errors that might happen if you pass an ill typed expression into
+||| whnf. don't do that please
+public export
+data WhnfErr = MissingEnumArm TagVal (List TagVal)
+
+
 public export
 0 RedexTest : TermLike -> Type
 RedexTest tm = forall q, d, n, g. Definitions' q g -> tm q d n -> Bool
 
 public export
-interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm where
+interface Whnf (0 tm : TermLike)
+               (0 isRedex : RedexTest tm)
+               (0 err : Type) | tm
+where
   whnf : (defs : Definitions' q g) ->
-         tm q d n -> Subset (tm q d n) (No . isRedex defs)
+         tm q d n -> Either err (Subset (tm q d n) (No . isRedex defs))
 
 public export
-0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
+0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex err =>
                       Definitions' q g -> Pred (tm q d n)
 IsRedex  defs = So . isRedex defs
 NotRedex defs = No . isRedex defs
 
 public export
-0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} -> Whnf tm isRedex =>
+0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
+             Whnf tm isRedex err =>
              (q : Type) -> (d, n : Nat) -> {g : _} ->
              (defs : Definitions' q g) -> Type
 NonRedex tm q d n defs = Subset (tm q d n) (NotRedex defs)
 
 public export %inline
-nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
+nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex err) =>
        (t : tm q d n) -> (0 nr : NotRedex defs t) =>
        NonRedex tm q d n defs
 nred t = Element t nr
@@ -149,6 +167,11 @@ isPairHead : Elim {} -> Bool
 isPairHead (Pair {} :# Sig {}) = True
 isPairHead _                   = False
 
+public export %inline
+isTagHead : Elim {} -> Bool
+isTagHead (Tag t :# Enum _) = True
+isTagHead _ = False
+
 public export %inline
 isE : Term {} -> Bool
 isE (E _) = True
@@ -170,6 +193,8 @@ mutual
     isRedexE defs f || isLamHead f
   isRedexE defs (CasePair {pair, _}) =
     isRedexE defs pair || isPairHead pair
+  isRedexE defs (CaseEnum {tag, _}) =
+    isRedexE defs tag || isTagHead tag
   isRedexE defs (f :% _) =
     isRedexE defs f || isDLamHead f
   isRedexE defs (t :# a) =
@@ -186,25 +211,25 @@ mutual
 
 mutual
   export covering
-  Whnf Elim Reduce.isRedexE where
+  Whnf Elim Reduce.isRedexE WhnfErr where
     whnf defs (F x) with (lookupElim x defs) proof eq
       _ | Just y  = whnf defs y
-      _ | Nothing = Element (F x) $ rewrite eq in Ah
+      _ | Nothing = pure $ Element (F x) $ rewrite eq in Ah
 
-    whnf _ (B i) = nred $ B i
+    whnf _ (B i) = pure $ nred $ B i
 
-    whnf defs (f :@ s) =
+    whnf defs (f :@ s) = do
-      let Element f fnf = whnf defs f in
+      Element f fnf <- whnf defs f
       case nchoose $ isLamHead f of
         Left _ =>
           let Lam body :# Pi {arg, res, _} = f
               s = s :# arg
           in
           whnf defs $ sub1 body s :# sub1 res s
-        Right nlh => Element (f :@ s) $ fnf `orNo` nlh
+        Right nlh => pure $ Element (f :@ s) $ fnf `orNo` nlh
 
-    whnf defs (CasePair pi pair ret body) =
+    whnf defs (CasePair pi pair ret body) = do
-      let Element pair pairnf = whnf defs pair in
+      Element pair pairnf <- whnf defs pair
       case nchoose $ isPairHead pair of
         Left _ =>
           let Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} = pair
@@ -213,10 +238,24 @@ mutual
           in
           whnf defs $ subN body [fst, snd] :# sub1 ret pair
         Right np =>
-          Element (CasePair pi pair r ret x y body) $ pairnf `orNo` np
+          pure $ Element (CasePair pi pair ret body)
+                         (pairnf `orNo` np)
 
-    whnf defs (f :% p) =
+    whnf defs (CaseEnum pi tag ret arms) = do
-      let Element f fnf = whnf defs f in
+      Element tag tagnf <- whnf defs tag
+      case nchoose $ isTagHead tag of
+        Left t =>
+          let Tag t :# Enum ts = tag
+              ty = sub1 ret tag
+          in
+          case lookup t arms of
+            Just arm => whnf defs $ arm :# ty
+            Nothing  => Left $ MissingEnumArm t (keys arms)
+        Right nt =>
+          pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
+
+    whnf defs (f :% p) = do
+      Element f fnf <- whnf defs f
       case nchoose $ isDLamHead f of
         Left _ =>
           let DLam body :# Eq {ty = ty, l, r, _} = f
@@ -224,34 +263,36 @@ mutual
           in
           whnf defs $ body :# dsub1 ty p
         Right ndlh =>
-          Element (f :% p) $ fnf `orNo` ndlh
+          pure $ Element (f :% p) $ fnf `orNo` ndlh
 
-    whnf defs (s :# a) =
+    whnf defs (s :# a) = do
-      let Element s snf = whnf defs s in
+      Element s snf <- whnf defs s
       case nchoose $ isE s of
-        Left  _  => let E e = s in Element e $ noOr2 snf
+        Left  _  => let E e = s in pure $ Element e $ noOr2 snf
-        Right ne =>
+        Right ne => do
-          let Element a anf = whnf defs a in
+          Element a anf <- whnf defs a
-          Element (s :# a) $ ne `orNo` snf `orNo` anf
+          pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf
 
     whnf defs (CloE  el th) = whnf defs $ pushSubstsWith' id th el
     whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el
 
   export covering
-  Whnf Term Reduce.isRedexT where
+  Whnf Term Reduce.isRedexT WhnfErr where
-    whnf _ t@(TYPE {}) = nred t
+    whnf _ t@(TYPE {}) = pure $ nred t
-    whnf _ t@(Pi   {}) = nred t
+    whnf _ t@(Pi   {}) = pure $ nred t
-    whnf _ t@(Lam  {}) = nred t
+    whnf _ t@(Lam  {}) = pure $ nred t
-    whnf _ t@(Sig  {}) = nred t
+    whnf _ t@(Sig  {}) = pure $ nred t
-    whnf _ t@(Pair {}) = nred t
+    whnf _ t@(Pair {}) = pure $ nred t
-    whnf _ t@(Eq   {}) = nred t
+    whnf _ t@(Enum {}) = pure $ nred t
-    whnf _ t@(DLam {}) = nred t
+    whnf _ t@(Tag  {}) = pure $ nred t
+    whnf _ t@(Eq   {}) = pure $ nred t
+    whnf _ t@(DLam {}) = pure $ nred t
 
-    whnf defs (E e) =
+    whnf defs (E e) = do
-      let Element e enf = whnf defs e in
+      Element e enf <- whnf defs e
       case nchoose $ isAnn e of
-        Left  _  => let tm :# _ = e in Element tm $ noOr1 $ noOr2 enf
+        Left  _  => let tm :# _ = e in pure $ Element tm $ noOr1 $ noOr2 enf
-        Right na => Element (E e) $ na `orNo` enf
+        Right na => pure $ Element (E e) $ na `orNo` enf
 
     whnf defs (CloT  tm th) = whnf defs $ pushSubstsWith' id th tm
     whnf defs (DCloT tm th) = whnf defs $ pushSubstsWith' th id tm

lib/Quox/Syntax/Dim.idr

@@ -61,7 +61,7 @@ PrettyHL (Dim n) where
 ||| - `r` if `p` is `K One`;
 ||| - `x` otherwise.
 public export
-endsOr : a -> a -> Lazy a -> Dim n -> a
+endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
 endsOr l r x (K e) = ends l r e
 endsOr l r x (B _) = x
 

lib/Quox/Syntax/Term/Base.idr

@@ -18,6 +18,8 @@ import Data.Nat
 import public Data.So
 import Data.String
 import Data.Vect
+import public Data.SortedMap
+import public Data.SortedSet
 
 %default total
 
@@ -30,6 +32,9 @@ public export
 0 TSubstLike : Type
 TSubstLike = Type -> Nat -> Nat -> Nat -> Type
 
+public export
+0 TagVal : Type
+TagVal = String
 
 infixl 8 :#
 infixl 9 :@, :%
@@ -57,6 +62,11 @@ mutual
     ||| pair value
     Pair : (fst, snd : Term q d n) -> Term q d n
 
+    ||| enumeration type
+    Enum : (cases : SortedSet TagVal) -> Term q d n
+    ||| enumeration value
+    Tag : (tag : TagVal) -> Term q d n
+
     ||| equality type
     Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> Term q d n
     ||| equality term
@@ -92,6 +102,12 @@ mutual
                (body : ScopeTermN 2 q d n) ->
                Elim q d n
 
+    ||| enum matching
+    CaseEnum : (qty : q) -> (tag : Elim q d n) ->
+               (ret : ScopeTerm q d n) ->
+               (arms : CaseEnumArms q d n) ->
+               Elim q d n
+
     ||| dim application
     (:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
 

lib/Quox/Syntax/Term/Pretty.idr

@@ -85,6 +85,11 @@ prettyCase pi elim r ret arms =
      hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
      hsep [ofD,     !(prettyArms arms)]]
 
+-- [fixme] put delimiters around tags that aren't simple names
+export
+prettyTag : TagVal -> Doc HL
+prettyTag t = hl Tag $ "`" <+> fromString t
+
 
 mutual
   export covering
@@ -101,6 +106,10 @@ mutual
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs t in
       prettyTuple $ s :: init ++ [last]
+    prettyM (Enum tags) =
+      pure $ braces . aseparate comma $ map prettyTag $ Prelude.toList tags
+    prettyM (Tag t) =
+      pure $ prettyTag t
     prettyM (Eq (S _ (N ty)) l r) =
       parensIfM Eq !(withPrec InEq $ pure $
         sep [!(prettyM l) <++> !eqndD,
@@ -137,6 +146,9 @@ mutual
       pat <- (parens . separate commaD . map (hl TVar)) <$>
              traverse prettyM [x, y]
       prettyCase pi p r ret [([x, y], pat, body)]
+    prettyM (CaseEnum pi t (S [r] ret) arms) =
+      prettyCase pi t r ret
+        [([], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
       prettyApps fun args

lib/Quox/Typechecker.idr

@@ -139,6 +139,19 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
     pure $ qfst + qsnd
 
+  check' ctx sg (Enum _) ty = do
+    -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
+    ignore $ expectTYPE !ask ty
+    expectEqualQ zero sg.fst
+    pure $ zeroFor ctx
+
+  check' ctx sg (Tag t) ty = do
+    tags <- expectEnum !ask ty
+    -- if t ∈ ts
+    unless (t `elem` tags) $ throwError $ TagNotIn t tags
+    -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
+    pure $ zeroFor ctx
+
   check' ctx sg (Eq t l r) ty = do
     u <- expectTYPE !ask ty
     expectEqualQ zero sg.fst
@@ -215,21 +228,48 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   infer' ctx sg (CasePair pi pair ret body) = do
     -- if 1 ≤ π
     expectCompatQ one pi
-    -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
+    -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
-    pairres <- inferC ctx sone pair
+    pairres <- inferC ctx sg pair
+    -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
     check0 (extendTy pairres.type ctx) ret.term (TYPE UAny)
     (tfst, tsnd) <- expectSig !ask pairres.type
-    -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐ ret[(x, y)] ⊳ Σ₂, ρ₁·x, ρ₂·y
+    -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
+    --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ π
     let bodyctx = extendTyN [< tfst, tsnd.term] ctx
         bodyty  = substCasePairRet pairres.type ret
     bodyout <- popQs [< pi, pi] !(checkC bodyctx sg body.term bodyty)
-    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
+    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,
       qout = pi * pairres.qout + bodyout
     }
 
+  infer' ctx sg (CaseEnum pi t ret arms) {n} = do
+    -- if 1 ≤ π
+    expectCompatQ one pi
+    -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
+    tres <- inferC ctx sg t
+    -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
+    check0 (extendTy tres.type ctx) ret.term (TYPE UAny)
+    -- if for each "a ⇒ s" in arms,
+    --   Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σ₂
+    -- for fixed Σ₂
+    armres <- for (SortedMap.toList arms) $ \(a, s) =>
+      checkC ctx sg s (sub1 ret (Tag a :# tres.type))
+    armout <- allEqual armres
+    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂
+    pure $ InfRes {
+      type = sub1 ret t,
+      qout = pi * tres.qout + armout
+    }
+   where
+    allEqual : List (QOutput q n) -> m (QOutput q n)
+    allEqual [] = pure $ zeroFor ctx
+    allEqual lst@(x :: xs) =
+      if all (== x) xs then pure x
+      else throwError $ BadCaseQtys lst
+
   infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun

lib/Quox/Typing.idr

@@ -111,8 +111,11 @@ data Error q
 = ExpectedTYPE (Term q d n)
 | ExpectedPi   (Term q d n)
 | ExpectedSig  (Term q d n)
+| ExpectedEnum (Term q d n)
 | ExpectedEq   (Term q d n)
 | BadUniverse  Universe Universe
+| TagNotIn     TagVal (SortedSet TagVal)
+| BadCaseQtys  (List (QOutput q n))
 
 -- first arg of ClashT is the type
 | ClashT EqMode (Term q d n) (Term q d n) (Term q d n)
@@ -145,6 +148,9 @@ data Error q
     (Elim q d n) (Elim q d n)
     (Error q)
 
+| WhnfError WhnfErr
+
+
 public export
 0 HasErr : Type -> (Type -> Type) -> Type
 HasErr q = MonadError (Error q)
@@ -204,30 +210,42 @@ substCasePairRet dty retty =
 
 
 parameters {auto _ : HasErr q m} (defs : Definitions' q _)
+  export covering %inline
+  whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfErr =>
+          tm q d n -> m (NonRedex tm q d n defs)
+  whnfT = either (throwError . WhnfError) pure . whnf defs
+
   export covering %inline
   expectTYPE : Term q d n -> m Universe
   expectTYPE s =
-    case fst $ whnf defs s of
+    case fst !(whnfT 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 $ whnf defs s of
+    case fst !(whnfT 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 $ whnf defs s of
+    case fst !(whnfT s) of
       Sig {fst, snd, _} => pure (fst, snd)
       _                 => throwError $ ExpectedSig s
 
+  export covering %inline
+  expectEnum : Term q d n -> m (SortedSet TagVal)
+  expectEnum s =
+    case fst !(whnfT s) of
+      Enum tags => pure tags
+      _         => throwError $ ExpectedEnum 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 $ whnf defs s of
+    case fst !(whnfT s) of
       Eq {ty, l, r, _} => pure (ty, l, r)
       _                => throwError $ ExpectedEq s

tests/TermImpls.idr

@@ -37,6 +37,12 @@ mutual
     Pair fst1 snd1 == Pair fst2 snd2 = fst1 == fst2 && snd1 == snd2
     Pair {} == _ = False
 
+    Enum ts1 == Enum ts2 = ts1 == ts2
+    Enum _ == _ = False
+
+    Tag t1 == Tag t2 = t1 == t2
+    Tag _ == _ = False
+
     Eq ty1 l1 r1 == Eq ty2 l2 r2 =
       ty1 == ty2 && l1 == l2 && r1 == r2
     Eq {} == _ = False
@@ -74,6 +80,10 @@ mutual
       q1 == q2 && p1 == p2 && r1 == r2 && b1 == b2
     CasePair {} == _ = False
 
+    CaseEnum q1 t1 r1 a1 == CaseEnum q2 t2 r2 a2 =
+      q1 == q2 && t1 == t2 && r1 == r2 && a1 == a2
+    CaseEnum {} == _ = False
+
     (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
     (_ :% _) == _ = False
 

tests/Tests/Reduce.idr

@@ -36,7 +36,6 @@ tests = "whnf" :- [
       E $ F "f" :@ FT "a"
   ],
 
-
   "neutrals" :- [
     testNoStep "x" {n = 1} $ BV 0,
     testNoStep "a"         $ F "a",

tests/TypingImpls.idr

@@ -4,6 +4,14 @@ import TAP
 import public Quox.Typing
 import public Quox.Pretty
 
+
+export
+ToInfo WhnfErr where
+  toInfo (MissingEnumArm t ts) =
+    [("type", "MissingEnumArm"),
+     ("tag", show t),
+     ("list", show ts)]
+
 export
 PrettyHL q => ToInfo (Error q) where
   toInfo (NotInScope x) =
@@ -18,6 +26,9 @@ PrettyHL q => ToInfo (Error q) where
   toInfo (ExpectedSig t) =
     [("type", "ExpectedSig"),
      ("got",  prettyStr True t)]
+  toInfo (ExpectedEnum t) =
+    [("type", "ExpectedEnum"),
+     ("got",  prettyStr True t)]
   toInfo (ExpectedEq t) =
     [("type", "ExpectedEq"),
      ("got",  prettyStr True t)]
@@ -25,6 +36,14 @@ PrettyHL q => ToInfo (Error q) where
     [("type", "BadUniverse"),
      ("low",  show k),
      ("high", show l)]
+  toInfo (TagNotIn t ts) =
+    [("type", "TagNotIn"),
+     ("tag", show t),
+     ("set", show $ SortedSet.toList ts)]
+  toInfo (BadCaseQtys qouts) =
+    ("type", "BadCaseQtys") ::
+    [(show i, prettyStr True q) | (i, q) <- zip [0 .. length qouts] qouts]
+
   toInfo (ClashT mode ty s t) =
     [("type",  "ClashT"),
      ("mode",  show mode),
@@ -63,3 +82,5 @@ PrettyHL q => ToInfo (Error q) where
   toInfo (WhileInferring  _ _ _     err) = toInfo err
   toInfo (WhileComparingT _ _ _ _ _ err) = toInfo err
   toInfo (WhileComparingE _ _ _ _   err) = toInfo err
+
+  toInfo (WhnfError err) = toInfo err