Importing module with wrong namespace causes internal error instead of user-friendly error.

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.

https://wiki.portal.chalmers.se/agda/pmwiki.php

Other

2.41k stars 339 forks source link

Importing module with wrong namespace causes internal error instead of user-friendly error. #7208

Closed m0rphism closed 2 months ago

m0rphism commented 3 months ago

Here is a minimal example:

Create the file A/B.agda and leave it empty.
Create the file A/C.agda with the following content:
```
module A.C where
import A.B
```

Typechecking A/C.agda produces the following internal error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Syntax/Abstract/Name.hs:150:44 in
Agda-2.6.5-9de5304dbca416633306287fb48f814746080b835e6ca9fe1e2f2405d4e3158f:Agda.Syntax.Abstract.Name

Expected behavior: Agda should inform me that A/B.agda exists, but that its module name defaults to B, whereas it should be A.B.

Agda Versions: Bug occurs with both Agda 2.6.4.3 and the current master (commit 403ee4263).

andreasabel commented 3 months ago

Ouch! The internal error is here: https://github.com/agda/agda/blob/403ee4263e0f14222956e398d2610ae1a4f05467/src/full/Agda/Syntax/Abstract/Name.hs#L149-L154 However, the cause is probably in our dreaded imports logic.

andreasabel commented 3 months ago

Agda 2.6.1 still says:

The file /Users/abel/play/agda/bugs/Issue7208/A.agda can be
accessed via several project roots. Both A and Issue7208.A point to
this file.
when scope checking the declaration
  import Issue7208.A

andreasabel commented 3 months ago

Bisection says: 6c29efdc8c0eb1d1fbaf2d2ef5a5eefb704a9525 is the first bad commit @rwe Date: Tue Nov 24 15:26:01 2020 -0800

imports/refact: Move ifile module name validation into getStoredInterface

Interfaces made with `createInterface` will already have been checked by
the scope checker, and cached interfaces will already have been either
there or here.

src/full/Agda/Interaction/Imports.hs | 14 +++++++-------

andreasabel commented 3 months ago

This commit does not cleanly revert, so one has to understand what is going on to restore the proper error. But blaming this commit might help understanding.