Fix case trees at multiplicity zero

Can't ignore a constructor a multiplicity zero if the whole function is
multiplicity zero

src/Core/CaseBuilder.idr

@@ -16,10 +16,10 @@ import Decidable.Equality
 %default covering
 
 public export
-data Phase = CompileTime | RunTime
+data Phase = CompileTime RigCount | RunTime
 
 Eq Phase where
-  CompileTime == CompileTime = True
+  CompileTime r == CompileTime r' = r == r'
   RunTime == RunTime = True
   _ == _ = False
 
@@ -253,8 +253,9 @@ clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs)
     clauseType' _                 = VarClause
 
     getClauseType : Phase -> Pat -> ArgType vars -> ClauseType
-    getClauseType CompileTime (PCon _ _ _ _ xs) (Known r t)
-        = if isErased r && all (namesIn (pvars ++ concatMap namesFrom (getPatInfo rest))) xs
+    getClauseType (CompileTime cr) (PCon _ _ _ _ xs) (Known r t)
+        = if isErased r && not (isErased cr) &&
+             all (namesIn (pvars ++ concatMap namesFrom (getPatInfo rest))) xs
              then VarClause
              else ConClause
     getClauseType phase (PAs _ _ p) t = getClauseType phase p t

src/TTImp/ProcessDef.idr

@@ -700,7 +700,7 @@ processDef opts nest env fc n_in cs_in
          let pats = map toPats (rights cs)
 
          (cargs ** (tree_ct, unreachable)) <-
-             getPMDef fc CompileTime n ty (rights cs)
+             getPMDef fc (CompileTime mult) n ty (rights cs)
 
          traverse_ warnUnreachable unreachable
 
@@ -807,7 +807,7 @@ processDef opts nest env fc n_in cs_in
         = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
              let covcs = mapMaybe id covcs'
              (_ ** (ctree, _)) <-
-                 getPMDef fc CompileTime (Resolved n) ty covcs
+                 getPMDef fc (CompileTime mult) (Resolved n) ty covcs
              log 3 $ "Working from " ++ show !(toFullNames ctree)
              missCase <- if any catchAll covcs
                             then do log 3 $ "Catch all case in " ++ show n

tests/idris2/reg022/case.idr

@@ -0,0 +1,5 @@
+-- Previously this gave an 'unreachable case warning' and evaluated
+-- to the first case! Should give foo : Nat -> Nat
+foo : (x : Nat) -> case S x of
+                        Z => Nat -> Nat
+                        (S k) => Nat

tests/idris2/reg022/expected

@@ -0,0 +1 @@
+1/1: Building case (case.idr)

tests/idris2/reg022/input

@@ -0,0 +1,2 @@
+:t foo
+:q

tests/idris2/reg022/run

@@ -0,0 +1,3 @@
+$1 --check case.idr
+
+rm -rf build