Don't build run time case trees for Rig0 defs

They might match on runtime-erased things (which is okay, since they're
erased too!) and if we try building the tree, it'll report an error
incorrectly. Fixes #229

src/Core/CaseBuilder.idr

@@ -559,7 +559,8 @@ sameType fc phase fn env [] = pure ()
 sameType {ns} fc phase fn env (p :: xs)
     = do defs <- get Ctxt
          case getFirstArgType p of
-              Known _ t => sameTypeAs !(nf defs env t) (map getFirstArgType xs)
+              Known _ t => sameTypeAs phase !(nf defs env t)
+                                      (map getFirstArgType xs)
               ty => throw (CaseCompile fc fn DifferingTypes)
   where
     firstPat : NamedPats ns (np :: nps) -> Pat
@@ -574,17 +575,17 @@ sameType {ns} fc phase fn env (p :: xs)
     headEq _ (NErased _ _) RunTime = True
     headEq _ _ _ = False
 
-    sameTypeAs : NF ns -> List (ArgType ns) -> Core ()
-    sameTypeAs ty [] = pure ()
-    sameTypeAs ty (Known Rig0 t :: xs)
+    sameTypeAs : Phase -> NF ns -> List (ArgType ns) -> Core ()
+    sameTypeAs _ ty [] = pure ()
+    sameTypeAs RunTime ty (Known Rig0 t :: xs)
           = throw (CaseCompile fc fn (MatchErased (_ ** (env, mkTerm _ (firstPat p)))))
                 -- Can't match on erased thing
-    sameTypeAs ty (Known c t :: xs)
+    sameTypeAs p ty (Known c t :: xs)
           = do defs <- get Ctxt
                if headEq ty !(nf defs env t) phase
-                  then sameTypeAs ty xs
+                  then sameTypeAs p ty xs
                   else throw (CaseCompile fc fn DifferingTypes)
-    sameTypeAs ty _ = throw (CaseCompile fc fn DifferingTypes)
+    sameTypeAs p ty _ = throw (CaseCompile fc fn DifferingTypes)
 
 -- Check whether all the initial patterns are the same, or are all a variable.
 -- If so, we'll match it to refine later types and move on

src/TTImp/ProcessDef.idr

@@ -522,17 +522,19 @@ mkRunTime n
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
               | _ => pure ()
-         let PMDef r cargs tree_ct _ pats = definition gdef
-              | _ => pure () -- not a function definition
-         let ty = type gdef
-         (rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty
-                                        !(traverse (toClause (location gdef)) pats)
-         log 5 $ "Runtime tree for " ++ show (fullname gdef) ++ ": " ++ show tree_rt
-         let Just Refl = nameListEq cargs rargs
-                 | Nothing => throw (InternalError "WAT")
-         addDef n (record { definition = PMDef r cargs tree_ct tree_rt pats
-                          } gdef)
-         pure ()
+         -- If it's erased at run time, don't build the tree
+         when (not (multiplicity gdef == Rig0)) $ do
+           let PMDef r cargs tree_ct _ pats = definition gdef
+                | _ => pure () -- not a function definition
+           let ty = type gdef
+           (rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty
+                                          !(traverse (toClause (location gdef)) pats)
+           log 5 $ "Runtime tree for " ++ show (fullname gdef) ++ ": " ++ show tree_rt
+           let Just Refl = nameListEq cargs rargs
+                   | Nothing => throw (InternalError "WAT")
+           addDef n (record { definition = PMDef r cargs tree_ct tree_rt pats
+                            } gdef)
+           pure ()
   where
     toClause : FC -> (vars ** (Env Term vars, Term vars, Term vars)) ->
                Core Clause

tests/Main.idr

@@ -73,7 +73,7 @@ idrisTests
        "record001", "record002",
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
-       "reg008",
+       "reg008", "reg009",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006",

tests/idris2/reg009/Case.idr

@@ -0,0 +1,6 @@
+import Decidable.Equality
+
+0 foo : (i, j : Nat) -> Bool
+foo i j = case decEq i j of
+            Yes pf => True
+            No  pf => False

tests/idris2/reg009/expected

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

tests/idris2/reg009/run

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