20070627-1

 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