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.
Page last modified on June 27, 2007, at 09:53 am
Powered by
PmWiki