Anonymous top module confuses Agda

[GoogleCodeExporter]

As expected, true is not in scope when trying to bind it to 'test':

module _ where

open import Common.Equality

module _ where
  open import Common.Prelude

test = true  -- fails as expected

However, if I delete the top-level anonymous module header, it is:

open import Common.Equality

module _ where
  open import Common.Prelude

test = true  -- works, but should fail

I would expect a parse error, as first stuff is indented, and then not.
However, it seems to be legal Agda:

module IndentationInTopModule where

  indented = Set

not-indented = Set

  -- again-indented = Set  -- Parse error

This parses: you can indent in the top module, then unindent. But if you
indent again, you get a parse error!?

Note that this is not allowed in inner modules!

module InnerModule where

    ind = Set

  not = Set  -- fails

    again-indented = Set

My opinion: Also in the top level module, if you start indented, you need to
continue indented. There should not be a special treatment of the top module
other than you can omit the indentation altogether.

Original issue reported on code.google.com by andreas....@gmail.com on 8 Dec 2014 at 2:34

[GoogleCodeExporter]

Doesn't seem to be special treatment of the top module, rather it seems to be
special treatment of zero indentation.

Like you say, this is okay:

module m where
 a = Set
b = Set

and it's only when it becomes

module m where
 a = Set
b = Set
 c = Set

that a parse error occurs. However, this fails:

module m where
  a = Set
 b = Set

Original comment by Whee...@gmail.com on 24 Apr 2015 at 2:10

[GoogleCodeExporter]

But in your first example, only 'a' is part of 'm', 'b' is in the top-level module, which also contains 'm'. And if 'm' is the top-level module, you have the bug I am complaining about.

Original comment by andreas....@gmail.com on 24 Apr 2015 at 3:12

[andreasabel]

Issue rediscovered by a user in
https://lists.chalmers.se/pipermail/agda/2016/008463.html

[andreasabel]

It seems that the weird behavior is introduced by the following code in Parser.y:

-- | Insert a top-level module if there is none.
figureOutTopLevelModule :: [Declaration] -> [Declaration]
figureOutTopLevelModule ds =
  case span isAllowedBeforeModule ds of
    (ds0, Module r m tel ds1 : ds2) -> ds0 ++ [Module r m tel $ ds1 ++ ds2]
    (ds0, ds1)                      -> ds0 ++ [Module (getRange ds1) (QName noName_) [] ds1]

case 1: If there are no non-import statements before the first module, we add the declarations ds2 following the first module to the first module declarations ds1. This makes code like

module File where
  ds1
ds2

legal when it really should be a parse error. In general, either ds1 or ds2 should be empty for this to be legal.

[andreasabel]

Issue was introduced by f304322 which fixed #953.