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 403ee42).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4