Fixed #1077 confusing error when declarations before the toplevel module

CHANGELOG.md

@@ -156,6 +156,38 @@ Language
   ```
   Before this change, you had to write `f .true c = true`.
 
+* Rule change for omitted top-level module headers.
+  [Issue [#1077](https://github.com/agda/agda/issues/1077)]
+
+  If your file is named `Bla.agda`, then the following content
+  is rejected.
+  ```agda
+    foo = Set
+    module Bla where
+      bar = Set
+  ```
+  Before the fix of this issue, Agda would add the missing module
+  header `module Bla where` at the top of the file.
+  However, in this particular case it is more likely the user
+  put the declaration `foo = Set` before the module start in error.
+  Now you get the error
+  ```
+    Illegal declaration(s) before top-level module
+  ```
+  if the following conditions are met:
+
+    1. There is at least one non-import declaration or non-toplevel pragma
+       before the start of the first module.
+
+    2. The module has the same name as the file.
+
+    3. The module is the only module at this level
+       (may have submodules, of course).
+
+  If you should see this error, insert a top-level module
+  before the illegal declarations, or move them inside the
+  existing module.
+
 Emacs mode
 ----------
 

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -1081,7 +1081,25 @@ instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
         (outsideDecls, [ C.Module r m0 tel insideDecls ]) -> do
           -- If the module name is _ compute the name from the file path
           m <- if isNoName m0
-                then return $ C.QName $ C.Name (getRange m0) [Id $ stringToRawName $ rootNameModule file]
+                then do
+                  -- Andreas, 2017-07-28, issue #1077
+                  -- Check if the insideDecls end in a single module which has the same
+                  -- name as the file.  In this case, it is highly likely that the user
+                  -- put some non-allowed declarations before the top-level module in error.
+                  case flip span insideDecls $ \case { C.Module{} -> False; _ -> True } of
+                    (ds0, [ C.Module _ m1 _ _ ])
+                       | C.toTopLevelModuleName m1 == expectedMName
+                         -- If the anonymous module comes from the user,
+                         -- the range cannot be the beginningOfFile.
+                         -- That is the range if the parser inserted the anon. module.
+                       , r == beginningOfFile (getRange insideDecls) -> do
+
+                         traceCall (SetRange $ getRange ds0) $ typeError $ GenericError $
+                           "Illegal declaration(s) before top-level module"
+
+                    -- Otherwise, reconstruct the top-level module name
+                    _ -> return $ C.QName $ C.Name (getRange m0)
+                           [Id $ stringToRawName $ rootNameModule file]
                 -- Andreas, 2017-05-17, issue #2574, keep name as jump target!
                 -- Andreas, 2016-07-12, ALTERNATIVE:
                 -- -- We assign an anonymous file module the name expected from

test/Fail/Issue1077.agda

@@ -0,0 +1,16 @@
+-- Andreas, 2017-07-28, issue #1077
+-- Agda's reconstruction of the top-level module can be confusing
+-- in case the user puts some illegal declarations before the
+-- top level module in error.
+
+foo = Set
+
+module Issue1077 where
+
+  bar = Set
+
+-- WAS: accepted, creating modules Issue1077 and Issue1077.Issue1077
+-- with Issue1077.foo and Issue1077.Issue1077.bar
+
+-- NOW: Error
+-- Illegal declarations before top-level module

test/Fail/Issue1077.err

@@ -0,0 +1,2 @@
+Issue1077.agda:6,1-10
+Illegal declaration(s) before top-level module

test/Fail/Issue1077Main.agda

@@ -0,0 +1,10 @@
+-- Andreas, 2017-07-28, issue 1077
+
+open import Issue1077
+
+foz = foo
+baz = bar
+
+-- WAS: bar not in scope
+
+-- NOW: import fails because module Issue1077 is rejected

test/Fail/Issue1077Main.err

@@ -0,0 +1,4 @@
+Issue1077.agda:6,1-10
+Illegal declaration(s) before top-level module
+when scope checking the declaration
+  open import Issue1077

test/Succeed/Issue1077.agda

@@ -0,0 +1,19 @@
+-- Andreas, 2017-07-28, issue #1077
+
+-- Agda's reconstruction of the top-level module can be confusing
+-- in case the user puts some illegal declarations before the
+-- top level module in error.
+
+-- Thus, Agda now rejects the following if the anon. module is omitted.
+-- If the user writes the anon. module, it should be accepted,
+-- (even if it looks stupid in this case).
+
+module _ where
+
+foo = Set
+
+module Issue1077 where
+
+  bar = Set
+
+-- Should be accepted.