Q:

Imported datatype clashes with locally defined one, even when renamed

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?

A:

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.

