Agda: Confusing error when inserting declaration before top-level module

[andreasabel]

Consider this valid Agda program:

module Issue2808 where
record Issue2808 : Set where

Now, if I accidentially put a declaration before the top level module header,

postulate A : Set
module Issue2808 where
record Issue2808 : Set where

I get this confusing error:

Duplicate definition of module Issue2808. Previous definition of
module Issue2808 at ...
when scope checking the declaration
  record Issue2808 where

The problem is that then Agda interprets the input as

module _ where
postulate A : Set
module Issue2808 where
record Issue2808 : Set where

I come to the conviction that allowing to omit the top-level module header completely was a mistake...

Related: #1077

[andreasabel]

I think we should row back a bit and require at least a module _ where top-level header.

I suppose big developments would not be affected, as there anyway modules have sensible names.

[nad]

I have previously suggested that one should only be allowed to omit the name for top-level modules, not for imported modules.

[andreasabel]

Since @UlfNorell had reservations about the rowing back, I fixed this in the minimal way by widening the fix for #1077 to the following situation:

-- module _ where  -- If this is added, we get the error about duplicate module

postulate A : Set  -- Accepted if this is deleted

module Issue2808 where

record Issue2808 : Set where

-- Expected error: (at the postulate)
-- Illegal declaration(s) before top-level module