module Bug where module P where postulate a : Set open P open P public b : Set b = a Bug.agda:10,5-6 Ambiguous name a. It could refer to any one of _.a bound at Bug.agda:4,13-14 P.a bound at Bug.agda:4,13-14 when scope checking a
The construction above is actually useful. Consider the following:
private open module P = ... open P public using (f)
Another recently introduced problem:
module Bug where module A where postulate a : Set module B where open A public module C where open A public open B open C d : Set d = a Bug.agda:16,5-6 Ambiguous name a. It could refer to any one of B.a bound at Bug.agda:4,13-14 C.a bound at Bug.agda:4,13-14 when scope checking a
This used to work and it is very inconvenient if it does not.
Powered by PmWiki