diff --git a/libs/base/Data/Nat/Order.idr b/libs/base/Data/Nat/Order.idr
index 5a945c05e3..55d98a1bac 100644
--- a/libs/base/Data/Nat/Order.idr
+++ b/libs/base/Data/Nat/Order.idr
@@ -58,8 +58,8 @@ decideLTE (S x)     Z  = No  zeroNeverGreater
 decideLTE (S x)   (S y) with (decEq (S x) (S y))
   decideLTE (S x)   (S y) | Yes eq      = rewrite eq in Yes (reflexive (S y))
   decideLTE (S x)   (S y) | No _ with (decideLTE x y)
-  decideLTE (S x)   (S y) | No _   | Yes nLTEm = Yes (LTESucc nLTEm)
-  decideLTE (S x)   (S y) | No _   | No  nGTm  = No (ltesuccinjective nGTm)
+    decideLTE (S x)   (S y) | No _   | Yes nLTEm = Yes (LTESucc nLTEm)
+    decideLTE (S x)   (S y) | No _   | No  nGTm  = No (ltesuccinjective nGTm)
 
 public export
 implementation Decidable 2 [Nat,Nat] LTE where
diff --git a/libs/base/Decidable/Equality.idr b/libs/base/Decidable/Equality.idr
index 034c32d4a1..02ab0b4337 100644
--- a/libs/base/Decidable/Equality.idr
+++ b/libs/base/Decidable/Equality.idr
@@ -116,8 +116,8 @@ DecEq a => DecEq (List1 a) where
   decEq (x ::: xs) (y ::: ys) with (decEq x y)
     decEq (x ::: xs) (y ::: ys) | No contra = No (contra . fst . consInjective)
     decEq (x ::: xs) (y ::: ys) | Yes eqxy with (decEq xs ys)
-    decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
-    decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys)
+      decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
+      decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys)
 
 -- TODO: Other prelude data types
 
diff --git a/libs/contrib/Data/List/Views/Extra.idr b/libs/contrib/Data/List/Views/Extra.idr
index 128335f303..48a4219505 100644
--- a/libs/contrib/Data/List/Views/Extra.idr
+++ b/libs/contrib/Data/List/Views/Extra.idr
@@ -161,12 +161,12 @@ lazyFilterRec pred (x :: xs) with (pred x)
         -> {auto prf2 : NonEmpty rest}
         -> LazyFilterRec (reverse reverseOfSkipped ++ rest)
       filterHelper revSkipped (y :: xs) with (pred y)
-      filterHelper revSkipped (y :: xs) | True =
-        Found (reverse revSkipped) y (lazyFilterRec pred xs)
-      filterHelper revSkipped (y :: []) | False =
-        rewrite sym (reverseOntoSpec [y] revSkipped) in
-          Exhausted $ reverse (y :: revSkipped)
-      filterHelper revSkipped (y :: (z :: zs)) | False =
-        rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in
+        filterHelper revSkipped (y :: xs) | True =
+          Found (reverse revSkipped) y (lazyFilterRec pred xs)
+        filterHelper revSkipped (y :: []) | False =
           rewrite sym (reverseOntoSpec [y] revSkipped) in
-            filterHelper (y :: revSkipped) (z :: zs)
+          Exhausted $ reverse (y :: revSkipped)
+        filterHelper revSkipped (y :: (z :: zs)) | False =
+          rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in
+            rewrite sym (reverseOntoSpec [y] revSkipped) in
+              filterHelper (y :: revSkipped) (z :: zs)
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 8d7a1404e4..e6abe62679 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -841,7 +841,7 @@ mutual
                             flags <- bounds (withFlags)
                             symbol "("
                             wval <- bracketedExpr fname flags indents
-                            ws <- nonEmptyBlock (clause (S withArgs) fname)
+                            ws <- mustWork $ nonEmptyBlockAfter col (clause (S withArgs) fname)
                             pure (flags, wval, forget ws))
             (flags, wval, ws) <- pure b.val
             let fc = boundToFC fname (mergeBounds start b)
diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr
index 0cd906590d..14ba13521c 100644
--- a/src/Parser/Rule/Source.idr
+++ b/src/Parser/Rule/Source.idr
@@ -438,7 +438,11 @@ blockAfter mincol item
             else blockEntries (AtPos col) item
 
 export
-blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> SourceEmptyRule (Maybe hd, List ty)
+blockWithOptHeaderAfter :
+   (column : Int) ->
+   (header : IndentInfo -> Rule hd) ->
+   (item : IndentInfo -> Rule ty) ->
+   SourceEmptyRule (Maybe hd, List ty)
 blockWithOptHeaderAfter {ty} mincol header item
     = do symbol "{"
          commit
@@ -472,3 +476,23 @@ nonEmptyBlock item
          res <- blockEntry (AtPos col) item
          ps <- blockEntries (snd res) item
          pure (fst res ::: ps)
+
+||| `nonEmptyBlockAfter col rule` parses a non-empty `rule`-block indented
+||| by at least `col` spaces (unless the block is explicitly delimited
+||| by curly braces). `rule` is a function of the actual indentation
+||| level.
+export
+nonEmptyBlockAfter : Int -> (IndentInfo -> Rule ty) -> Rule (List1 ty)
+nonEmptyBlockAfter mincol item
+    = do symbol "{"
+         commit
+         res <- blockEntry AnyIndent item
+         ps <- blockEntries (snd res) item
+         symbol "}"
+         pure (fst res ::: ps)
+  <|> do col <- column
+         let False = col <= mincol
+            | True => fail "Expected an indented non-empty block"
+         res <- blockEntry (AtPos col) item
+         ps <- blockEntries (snd res) item
+         pure (fst res ::: ps)
diff --git a/tests/Main.idr b/tests/Main.idr
index 6bad44042b..931c1fd37e 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -152,7 +152,7 @@ idrisTests = MkTestPool []
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
        -- The 'with' rule
-       "with001", "with002",
+       "with001", "with002", "with004",
        -- with-disambiguation
        "with003"]
 
diff --git a/tests/idris2/with004/Issue637-2.idr b/tests/idris2/with004/Issue637-2.idr
new file mode 100644
index 0000000000..e541889163
--- /dev/null
+++ b/tests/idris2/with004/Issue637-2.idr
@@ -0,0 +1,8 @@
+namespace A
+  export
+  foo3 : Int -> Int
+  foo3 x with (x + 1)
+  foo3 x | y = y + x
+
+foo4 : Int
+foo4 = A.foo3 5
diff --git a/tests/idris2/with004/Issue637-3.idr b/tests/idris2/with004/Issue637-3.idr
new file mode 100644
index 0000000000..5225c92716
--- /dev/null
+++ b/tests/idris2/with004/Issue637-3.idr
@@ -0,0 +1,6 @@
+foo5 : Int -> Int
+foo5 x with (x + 1)
+foo5 x | y = y + x
+
+foo6 : Int
+foo6 = 52
diff --git a/tests/idris2/with004/Issue637.idr b/tests/idris2/with004/Issue637.idr
new file mode 100644
index 0000000000..326210a6e4
--- /dev/null
+++ b/tests/idris2/with004/Issue637.idr
@@ -0,0 +1,6 @@
+foo : Int -> Int
+foo x with (x + 1)
+  foo x | y = y + x
+
+foo2 : Int
+foo2 = foo 5
diff --git a/tests/idris2/with004/expected b/tests/idris2/with004/expected
new file mode 100644
index 0000000000..d9c6fcad2d
--- /dev/null
+++ b/tests/idris2/with004/expected
@@ -0,0 +1,24 @@
+1/1: Building Issue637 (Issue637.idr)
+Main> 11
+Main> 
+Bye for now!
+1/1: Building Issue637-2 (Issue637-2.idr)
+Error: Expected an indented non-empty block.
+
+Issue637-2.idr:5:3--5:4
+ 1 | namespace A
+ 2 |   export
+ 3 |   foo3 : Int -> Int
+ 4 |   foo3 x with (x + 1)
+ 5 |   foo3 x | y = y + x
+       ^
+
+1/1: Building Issue637-3 (Issue637-3.idr)
+Error: Expected an indented non-empty block.
+
+Issue637-3.idr:3:1--3:2
+ 1 | foo5 : Int -> Int
+ 2 | foo5 x with (x + 1)
+ 3 | foo5 x | y = y + x
+     ^
+
diff --git a/tests/idris2/with004/input b/tests/idris2/with004/input
new file mode 100644
index 0000000000..25f21400d9
--- /dev/null
+++ b/tests/idris2/with004/input
@@ -0,0 +1,2 @@
+foo2
+:q
\ No newline at end of file
diff --git a/tests/idris2/with004/run b/tests/idris2/with004/run
new file mode 100755
index 0000000000..033e0f6133
--- /dev/null
+++ b/tests/idris2/with004/run
@@ -0,0 +1,5 @@
+$1 --no-color --console-width 0 --no-banner Issue637.idr < input
+$1 --no-color --console-width 0 --no-banner --check Issue637-2.idr
+$1 --no-color --console-width 0 --no-banner --check Issue637-3.idr
+
+rm -rf build