Using hidden parameter in the first statement of namespace will cause "Expected end of input" error

[redfish64]

https://gist.github.com/redfish64/3360283feec917651bc6f5e5be81f78a

module HiddenParamBug

interface Fooable x where
  foo : x -> Int
  
data Foo : Int -> Type where
  MkFoo : Foo v

--doesn't typecheck: Expected end of input.
namespace S  
  {v : Int} -> Fooable (Foo v) where
    foo f = v
 
--does typecheck 
namespace S1
  bar : ()
  bar = ()
  
  {v : Int} -> Fooable (Foo v) where
    foo f = v
    

--also typechecks
{v : Int} -> Fooable (Foo v) where
  foo f = v

As noted in comments, when {v : Int} -> ... appears as the first line in namespace, will fail with "Expected end of input", but if there is something beforehand, it will typecheck fine. This is also happens at top level, for example, if Foo and Fooable are created in one file and imported in another, and the implementation is the first thing defined in that file, as follows:

HiddenParamBug1.idr: https://gist.github.com/redfish64/8790abae7643d9ae875b921a9f3de6e5

module HiddenParamBug1

public export
interface Fooable x where
  foo : x -> Int
  
public export
data Foo : Int -> Type where
  MkFoo : Foo v

HiddenParamBug2.idr: https://gist.github.com/redfish64/0ebca856c145502bd73cc15439a1c6c4

module HiddenParamBug2 

import HiddenParamBug1

-- if uncommented, will typecheck
-- t : ()
-- t = ()

{v : Int} -> Fooable (Foo v) where
  foo f = v

[buzden]

Despite the error looks like a bug, you can workaround it using the implementation keyword:

namespace S  
  implementation {v : Int} -> Fooable (Foo v) where
    foo f = v

[gallais]

I see. The issue is that { can be used to delimit a block instead of indentation. So in theory you could write (it seems broken at the moment for a reason that escapes me):

namespace Absurd { data T : Type where }

In the parser we commit to a braces-delimited block as soon as we see the opening brace.

[jmanuel1]

I encountered this recently (while minimizing an example for another bug). With the following file:

{_ : x} -> Functor List where
    map f xs = ?hole

The parse error I get is:

Error: Expected '}'.

imp-with-brace-imp-at-top:1:2--1:3
 1 | {_ : x} -> Functor List where
      ^

Additionally, when I reload the file in the REPL, what I typed into the REPL is reported as the file contents.

Main> :r
Error: Expected '}'.

imp-with-brace-imp-at-top:1:2--1:3
 1 | :r
      ^