From 1092804726bef7d8093ab553947d036b8ebd3e67 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 20 Dec 2022 15:26:31 +0000
Subject: [PATCH] [ fix #2821 ] Failing blocks should force delayed holes

---
 src/TTImp/ProcessDecls.idr            | 15 +++++++++++++--
 tests/Main.idr                        |  2 +-
 tests/idris2/failing004/Issue2821.idr | 12 ++++++++++++
 tests/idris2/failing004/expected      |  1 +
 tests/idris2/failing004/run           |  3 +++
 5 files changed, 30 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/failing004/Issue2821.idr
 create mode 100644 tests/idris2/failing004/expected
 create mode 100755 tests/idris2/failing004/run

diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr
index d762c14e2..779e289a9 100644
--- a/src/TTImp/ProcessDecls.idr
+++ b/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}"
diff --git a/tests/Main.idr b/tests/Main.idr
index a0711a99e..5039944c8 100644
--- a/tests/Main.idr
+++ b/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
diff --git a/tests/idris2/failing004/Issue2821.idr b/tests/idris2/failing004/Issue2821.idr
new file mode 100644
index 000000000..272ab1f5f
--- /dev/null
+++ b/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
diff --git a/tests/idris2/failing004/expected b/tests/idris2/failing004/expected
new file mode 100644
index 000000000..88ea364fc
--- /dev/null
+++ b/tests/idris2/failing004/expected
@@ -0,0 +1 @@
+1/1: Building Issue2821 (Issue2821.idr)
diff --git a/tests/idris2/failing004/run b/tests/idris2/failing004/run
new file mode 100755
index 000000000..2161d97f2
--- /dev/null
+++ b/tests/idris2/failing004/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check Issue2821.idr
\ No newline at end of file