Imported datatype clashes with locally defined one, even when renamed

Question

With the following Agda code, I get an error on the definition of B in A₂:

module Whatever where

module A₁ where
  data B : Set where

module A₂ where
  open A₁ renaming (B to B₁)
  data B : Set where

The error message is:

Duplicate definition of module B. Previous definition of datatype
module B at /home/cactus/prog/agda/modules.agda:4,8-9
when scope checking the declaration
  data B where

But I am renaming B to B₁ on the import, so why does it still clash? And is there a way around it?

Answer 1

The problem is that data types define a module and a name. You need to rename the module, too. This works:

module Cactus where

module A₁ where
  data B : Set where

module A₂ where
  open A₁ renaming (B to B₁; module B to B₁)
  data B : Set where

This allows you to refer to constructors in a module-ish way, so if you have a conflict between Level.suc and your ℕ one, you can just write ℕ.suc and have it work without having to go through renaming shenanigans.

Answer 2

It seems an Agda bug to me. You can report the bug in http://code.google.com/p/agda/issues/list.