[ fix #637 ] force indentation after a with

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

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
 

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)

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)

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)

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"]
 

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

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

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

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
+     ^
+

tests/idris2/with004/input

@@ -0,0 +1,2 @@
+foo2
+:q

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