Andreas Abel

So this is an intended behavior change, not a regression. This means that one has to be more careful not to have outdated build-tool products left behind from manual invocations....

@sergv wrote: > Maybe cabal should be sticter and plainly refuse to do anything if the user asked for, say, module `Foo` not listed under `autogen-modules` but cabal can only...

Ping @philderbeast .

Bisection says I introduced this bug in 180795d362f4c934a1d6409247852af68a6fae53 > Date: Mon May 18 19:47:52 2020 +0200 > > [ fixed #3933 ] duplicate @import@ now accumulates scope > > Previously,...

I think we need to clarify what it means if you `import` the same module with different restrictions. ```agda import Foo using (foo) foo1 = Foo.foo -- ok bar1 =...

There is a distinction between modules that exists on your hard drive (external modules) and modules that are scope in your current development. So if you write `import Foo using...

Ok, so at the moment we allow to accumulate modules over several imports. We even can extend local modules by imports. ```agda module _ where module N where postulate A...

> So if one writes > > ```agda > import Foo using (foo) > import Foo hiding (foo) > ``` > > that should functionally be equivalent to just `import...

This creates locally a module `M`: ```agda import Agda.Builtin.Nat as M ``` This extends it: ```agda import Agda.Builtin.Bool as M ``` Doesn't feel weird because we know it from Haskell....

I think the problem in the OP is that `import Foo as X` does not copy `Foo` into `X` but just establishes `X` as a reference to `Foo`. So `X`...