module - 导入的数据类型与本地定义的数据类型冲突，即使重命名时也是如此

Question

使用以下 Agda 代码，我在 A2 中的 B 定义上遇到错误:

module Whatever where

module A₁ where
  data B : Set where

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

错误信息是:

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

但是我在导入时将 B 重命名为 B₁，那么为什么它仍然会发生冲突？有没有办法解决这个问题？

Answer 1

问题在于数据类型定义了模块和名称。您还需要重命名该模块。这有效:

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

这允许您以模块式的方式引用构造函数，因此如果您的 Level.suc 和您的 ℕ 之间存在冲突，您可以直接编写ℕ.suc 并使其正常工作，而无需进行重命名恶作剧。