"with" sometimes requires indentation and sometimes doesn't

[redfish64]

Not really sure if this is worth fixing, but the behavior is a little confusing.

https://gist.github.com/redfish64/2e74e64f052fd0e8e1fdfd84c3ae27f9

foo : Int -> Int
foo x with (x + 1)
  foo x | y = y + x

foo2 : Int
foo2 = foo 5

namespace A
  --typechecks by virtue of being at the last thing defined in the namespace identation block
  export
  foo3 : Int -> Int
  foo3 x with (x + 1)
  foo3 x | y = y + x
 
--and still works as expected 
foo4 : Int
foo4 = A.foo3 2

--same as foo3
foo5 : Int -> Int
foo5 x with (x + 1)
foo5 x | y = y + x

--fails to typecheck only due to the lack of indenting of the last foo5 line
foo6 : Int
foo6 = 52

Steps to Reproduce

Typecheck

Expected Behavior

foo3 to produce a typecheck error, or foo5 not to.

Observed Behavior

foo3 typechecks, yet foo5 doesn't.

- + Errors (1)
 `-- WithBug.idr line 24 col 5:
     Parse
     error at line 24:6:
     Wrong number of 'with' arguments (next
     tokens: [symbol :, identifier Int, identifier foo6, symbol =, literal 52, end
              of
              input])

[jasoncarr0]

This probably ought to count as a pretty terrible frontend bug.

When I got it I didn't realize at all that with needed the indentation. What this presented to me was that every time I tried to define anything at all after my with clause, I got the error message:

Parse error: Wrong number of 'with' arguments (next tokens: [symbol :, ... as though my definition was being parsed as part of the same branch.