[Agda] modules named `_`

[David Darais]

Hello list,

I have a proposal concerning modules named `_`.

What do you think this module does?

    module OuterModule where
      module _ (A : Set) where
        foo : A → A
        foo x = x
      module _ (A : Set) where
        foo : A → A
        foo x = x

Agda doesn't accept this, saying `foo` is already defined.

It looks like:

    module _ (A : Set) where
      foo : A → A
      foo x = x

is being desugared to something like:

    module unique$123 (A : Set) where
      foo : A → A
      foo x = x
    open unique$123 public

I consider this slightly strange behavior for someone who doesn't know this
magical desugaring, particularly for sibling modules named `_`.

What are your thoughts on requiring/allowing `open public` at the end of a
parameter list, or somewhere else, to indicate that the contents of a module
should be immediately opened after its definition? Something like:

    module _ (A : Set) open public where
      foo : A → A
      foo x = x

This would also allow for the "open after definition" functionality for named
modules, or the ability to open an unnamed module without the public modifier.
Also it would remove the confusion about what a module with name `_` means.
`module _` would then just introduce a unique name, which is a little less
surprising, and the flavor of automatic opening would be make explicit.

Cheers,
David