[ error ] Improve error messages for indentation issues

src/Idris/Parser.idr

@@ -1098,7 +1098,8 @@ mutual
                      rhs <- typeExpr pdef fname indents
                      ws <- option [] $ whereBlock fname col
                      pure (rhs, ws)
-            atEnd indents
+            b' <- bounds peek
+            mustWorkBecause b'.bounds "Not the end of a block entry, check indentation" $ atEnd indents
             (rhs, ws) <- pure b.val
             let fc = boundToFC fname (mergeBounds start b)
             pure (MkPatClause fc (uncurry applyArgs lhs) rhs ws)

tests/Main.idr

@@ -96,7 +96,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
        "perror011", "perror012", "perror013", "perror014", "perror015",
        "perror016", "perror017", "perror018", "perror019", "perror020",
        "perror021", "perror022", "perror023", "perror024", "perror025",
-       "perror026"]
+       "perror026", "perror027"]
 
 idrisTestsInteractive : TestPool
 idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing

tests/idris2/perror027/Outdent.idr

@@ -0,0 +1,5 @@
+countdown : (secs: Nat) -> IO ()
+countdown Z = putStrLn "Lift off!"
+countdown (S secs) = do putStrLn (show (S secs))
+                     usleep 1000000
+                     countdown secs

tests/idris2/perror027/expected

@@ -0,0 +1,10 @@
+1/1: Building Outdent (Outdent.idr)
+Error: Not the end of a block entry, check indentation.
+
+Outdent:4:22--4:28
+ 1 | countdown : (secs: Nat) -> IO ()
+ 2 | countdown Z = putStrLn "Lift off!"
+ 3 | countdown (S secs) = do putStrLn (show (S secs))
+ 4 |                      usleep 1000000
+                          ^^^^^^
+

tests/idris2/perror027/run

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