Agda: The handling of renamed modules should be improved

[mietek]

Let’s say we are reorganising a repository, and we rename the file “Foo.agda” to “Bar.agda”, in the filesystem. Next, we update “Everything.agda” to import Bar, and we reload the file. We get an error:

The name of the top level module does not match the file name. The module Bar should be defined in one of the following files: …

First, the error message is not very helpful. This could be improved to say “The file Bar.agda should contain the Bar top level module, but it contains the Foo top level module.”, or something to this effect.

Second, the error leaves Emacs in a black-and-white state, pointed at the import site in “Everything.agda”, which means it’s not possible to easily navigate to the problematic file, that is, “Bar.agda”. This could be improved by pointing Emacs at the problematic Foo top level module declaration, in the problematic file.

[andreasabel]

1. I think the error message is so complicated because of hierarchical modules. Of course, Agda could suggest the most likely fix.
2. The other concern is that the error is raised in the wrong location.

I addressed 2. by raising the error in the file with the wrong module name.

Wrt. 1., what currently Agda does it finds the file "Bar.agda" for the import of "Bar". Then it processes this file without considering how it got there. It realizes that the module name does not match a valid filepath (relative to the current include directories) and complains. We can distinguish whether a file load came from the top or via an import, and give different error messages for these cases.

[andreasabel]

Ok, now I addressed also 1. Required some digging through my (least) favorite Spaghetti code, which got some small clarification along the way: Agda.Interaction.Imports.
Now, Agda will suggest you name the wrongly named module as you said so in the import statement.

[nad]

I addressed 2. by raising the error in the file with the wrong module name.

The (history of the) error message for Issue2092.agda suggests otherwise. It starts in the following way:

Issue2092.agda:1,8-34

Did you change your mind?

(If anyone decides to do something about this, please wait until after I have pushed a fix for #2473.)

[nad]

(If anyone decides to do something about this, please wait until after I have pushed a fix for #2473.)

Done.