Delay building references for case blocks

...until the definition is complete. This is necessary since sometimes
information outside the case block can help resolve interfaces, and in
the simplest case, we might just have delayed resolving a default
Integer. It turns out this was also an obscure bug waiting to happen
with coverage checking of nested case blocks (so there's a test update
there too).

Fixes #443

src/Core/Coverage.idr

@@ -373,7 +373,9 @@ getMissing fc n ctree
         pure (map (apply fc (Ref fc Func n)) pats)
 
 -- For the given name, get the names it refers to which are not themselves
--- covering
+-- covering.
+-- Also need to go recursively into case blocks, since we only calculate
+-- references for them at the top level clause
 export
 getNonCoveringRefs : {auto c : Ref Ctxt Defs} ->
                      FC -> Name -> Core (List Name)
@@ -381,8 +383,19 @@ getNonCoveringRefs fc n
    = do defs <- get Ctxt
         Just d <- lookupCtxtExact n (gamma defs)
            | Nothing => throw (UndefinedName fc n)
-        filterM (notCovering defs) (mapMaybe noAssert (toList (refersTo d)))
+        let ds = mapMaybe noAssert (toList (refersTo d))
+        let cases = filter isCase !(traverse toFullNames ds)
+
+        -- Case blocks aren't recursive, so we're safe!
+        cbad <- traverse (getNonCoveringRefs fc) cases
+        topbad <- filterM (notCovering defs) ds
+        pure (topbad ++ concat cbad)
   where
+    isCase : Name -> Bool
+    isCase (NS _ n) = isCase n
+    isCase (CaseBlock _ _) = True
+    isCase _ = False
+
     noAssert : (Name, Bool) -> Maybe Name
     noAssert (n, True) = Nothing
     noAssert (n, False) = Just n

src/TTImp/ProcessDef.idr

@@ -729,13 +729,14 @@ processDef opts nest env fc n_in cs_in
          put Ctxt (record { toCompileCase $= (n ::) } defs)
 
          atotal <- toResolvedNames (NS ["Builtin"] (UN "assert_total"))
-         calcRefs False atotal (Resolved nidx)
          when (not (InCase `elem` opts)) $
-             do sc <- calculateSizeChange fc n
+             do calcRefs False atotal (Resolved nidx)
+                sc <- calculateSizeChange fc n
                 setSizeChange fc n sc
                 checkIfGuarded fc n
 
          md <- get MD -- don't need the metadata collected on the coverage check
+
          cov <- checkCoverage nidx ty mult cs
          setCovering fc n cov
          put MD md

tests/Main.idr

@@ -102,7 +102,7 @@ idrisTests
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
-       "reg029", "reg030", "reg031", "reg032",
+       "reg029", "reg030", "reg031", "reg032", "reg033",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009",

tests/idris2/coverage010/casetot.idr

@@ -15,6 +15,7 @@ main = do
       | _ => do putStrLn "One argument expected."
                 exitFailure
   let n = stringToNatOrZ arg
+  -- case block in a case block, which is needed to test this properly
   case natToFin n (length ints + 1) of
        Nothing => do putStrLn "Invalid number."
                      exitFailure

tests/idris2/coverage010/expected

@@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
 12	main : IO ()
 13	main = do
 
-	Calls non covering function Main.case block in main
+	Calls non covering function Main.case block in case block in main

tests/idris2/reg033/DerivingEq.idr

@@ -0,0 +1,51 @@
+module DerivingEq
+
+import Language.Reflection
+
+%language ElabReflection
+
+public export
+countArgs : (ty : TTImp) -> Nat
+countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
+countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy
+countArgs _ = 0
+
+-- %logging 5
+public export
+genEq : Name -> Elab (t -> t -> Bool)
+genEq typeName = do
+  let pos : FC = MkFC "generated code" (0,0) (0,0)
+  [(n, _)] <- getType typeName
+      | _ => fail "Ambiguous name"
+  constrs <- getCons n
+  let and : TTImp -> TTImp -> TTImp
+      and x y = `(~(x) && ~(y))
+      compareEq : String -> String -> TTImp
+      compareEq x y = `(~(IVar pos $ UN x) == ~(IVar pos $ UN y))
+      makeClause : Name -> Elab Clause
+      makeClause constr = do
+        [(_, ty)] <- getType constr
+            | _ => fail "ambiguous name for constr"
+        let nArgs = countArgs ty
+        let xs = map (\i => "x_" ++ show i) $ take nArgs [1..]
+        let ys = map (\i => "y_" ++ show i) $ take nArgs [1..]
+        let px = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) xs
+        let py = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) ys
+        pure $ PatClause pos `(MkPair ~(px) ~(py))
+             $ foldl and `(True) $ zipWith compareEq xs ys
+      finalClause : Clause
+      finalClause = PatClause pos `(_) `(False)
+  clauses <- traverse makeClause constrs
+  let allClauses = clauses ++ [finalClause]
+      caseExpr = ICase pos `(MkPair x y) (Implicit pos True) allClauses
+      result = `(\x, y => ~(caseExpr))
+  check result
+%logging 0
+
+-- This tree works
+
+data TreeOne a = BranchOne (TreeOne a) a (TreeOne a)
+               | Leaf
+
+Eq a => Eq (TreeOne a) where
+  (==) = %runElab genEq `{{ TreeOne }}

tests/idris2/reg033/expected

@@ -0,0 +1,2 @@
+1/2: Building DerivingEq (DerivingEq.idr)
+2/2: Building test (test.idr)

tests/idris2/reg033/run

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

tests/idris2/reg033/test.idr

@@ -0,0 +1,12 @@
+import Language.Reflection
+import DerivingEq
+
+%language ElabReflection
+
+-- This tree doesn't work
+
+data TreeTwo a = BranchTwo (TreeTwo a) a (TreeTwo a)
+               | Leaf
+
+Eq a => Eq (TreeTwo a) where
+  (==) = %runElab genEq `{{ TreeTwo }}