Module A.B shadows definition of B in module A, even in a module that only imports A

[gergoerdi]

Using idris2-dom, I have the following three modules:

JS/Promise.idr

module JS.Promise

Web/Fetch.idr

module Web.Fetch

import JS
import Web.Dom

%foreign "browser:lambda:r => fetch(r)"
prim__fetch : Union2 String Request -> PrimIO (Promise Response)

Main.idr

import JS.Promise
import JS
import Web.Fetch

main : IO ()
main = pure ()

(any other module not included above comes from idris2-dom)

If I try to compile Main, I get the following error from the typechecker:

Error: While processing type of prim__fetch. Undefined name Promise.

If I change Main.idr to:

-- import JS.Promise
import JS
import Web.Fetch

main : IO ()
main = pure ()

and then try rebuilding, it still fails. However, if I then delete the build/ directory and then rebuild with the JS.Promise import commented out, the compilation succeeds.

[gallais]

Can we get a MWE that does not rely on installing a 3rd party library
(or any library at all, ideally)?

[gergoerdi]

OK so this took a bit of effort to remove the external dependency, but here you go.

Create a library

lib/Lib.idr

module Lib

import public Lib.Foo

lib/Lib/Foo.idr

module Lib.Foo

export
data Foo = MkFoo

Create an executable that depends on lib

exe/Main.idr

import Lib.Foo
import Lib
import Bar

main : IO ()
main = pure ()

exe/Lib/Foo.idr

module Lib.Foo

import Lib

export blah : Foo -> Foo
blah x = x

exe/Bar.idr

module Bar

import Lib

quux : Foo -> Foo
quux x = x

[gergoerdi]

So what happens is that you can typecheck exe/Bar.idr on its own and it will work because it imports the Lib module from the library. However, once exe/Lib/Foo.idr is compiled, it "taints" the /build directory, and from now on, even exe/Bar.idr fails to typecheck. It seems tha Lib's public import of Lib.Foo is resolved incorrectly into exe/Lib/Foo.idr instead of lib/Lib/Foo.idr.

[gallais]

I don't know about "resolved incorrectly": you have conflicting module names. It's not
clear to me what the right solution is. This reminds me of #1793 although that was across
packages.

[gergoerdi]

To me, this seems definitely like a bug: exe:Bar imports Lib, which is a module only available in lib so it is not a clash. And lib:Lib's definition should not change just because we happen to also have another module called exe:Lib.Foo.

[gallais]

The current design assumes that module names are unique so this is the expected (undefined)
behaviour in case there's a clash. Now, we can of course discuss changing the design to
allow clashing module names. This will probably have to take place in a more general discussion
such as the one on library management and packaging (#1727).

[gergoerdi]

Then it should give an error. The fact that exe:Bar typechecks or not based on what happened before that wrote to /build shouldn't be the expected behaviour...