20070530-2

module q where

postulate A : Set
postulate B : Set


module r where
  A : Set -- this is allowed
--  A = B -- this complains about A being ambiguous
  r.A = B -- this complains about A being ambiguous

{-
/home/patrikj/src/Agda2/examples/AIM5/PolyDep/Homogenous/q.agda:10,3-10
Ambiguous name A. It could refer to any one of
  q.r.A
  bound at
  /home/patrikj/src/Agda2/examples/AIM5/PolyDep/Homogenous/q.agda:8,3-4
  q.A
  bound at
  /home/patrikj/src/Agda2/examples/AIM5/PolyDep/Homogenous/q.agda:3,11-12
when scope checking the definition
  r.A = B
-}



{-
-- Same problem here
C : Set
C = s.A
  module s where
    A : Set
    s.A = B
-}

-- But this is allowed
D : Set
D = let A : Set
        A = B
    in A

Notes

• Update: Fixed. Now an error is reported when a definition shadows a name.