[ fix #2821 ] Failing blocks should force delayed holes

src/TTImp/ProcessDecls.idr

@@ -54,7 +54,11 @@ processFailing eopts nest env fc mmsg decls
          ust <- get UST
          syn <- get Syn
          md <- get MD
+
+         -- We expect the block to fail and so the definitions introduced
+         -- in it should be discarded once we leave the block.
          defs <- branch
+
          -- We're going to run the elaboration, and then return:
          -- * Nothing     if the block correctly failed
          -- * Just err    if it either did not fail or failed with an invalid error message
@@ -65,8 +69,15 @@ processFailing eopts nest env fc mmsg decls
                    after <- getTotalityErrors
                    let errs = after \\ before
                    let (e :: es) = errs
-                     | [] => -- We have (unfortunately) succeeded
-                             pure (Just $ FailingDidNotFail fc)
+                     | [] => do -- We better have unsolved holes
+                                -- checkUserHoles True -- do we need this one too?
+
+                                 -- should we only look at the ones introduced in the block?
+                                Nothing <- checkDelayedHoles
+                                  | Just err => throw err
+
+                                -- Or we have (unfortunately) succeeded
+                                pure (Just $ FailingDidNotFail fc)
                    let Just msg = mmsg
                      | _ => pure Nothing
                    log "elab.failing" 10 $ "Failing block based on \{show msg} failed with \{show errs}"

tests/Main.idr

@@ -78,7 +78,7 @@ idrisTestsWarning = MkTestPool "Warnings" [] Nothing
 
 idrisTestsFailing : TestPool
 idrisTestsFailing = MkTestPool "Failing blocks" [] Nothing
-      ["failing001", "failing002", "failing003"
+      ["failing001", "failing002", "failing003", "failing004"
       ]
 
 idrisTestsError : TestPool

tests/idris2/failing004/Issue2821.idr

@@ -0,0 +1,12 @@
+import Data.Vect
+
+f : {n : Nat} -> Vect n Nat
+f = replicate _ 0
+
+d : Vect n Nat -> Nat
+d = foldl (+) 0
+
+failing "Unsolved hole"
+
+  z : Nat
+  z = d f

tests/idris2/failing004/expected

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

tests/idris2/failing004/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check Issue2821.idr