Constructors can be marked as erased

[nad]

The following code is accepted:

open import Agda.Builtin.Bool

data D : Set where
  c₁ : D
  @0 c₂ : D

d : D
d = c₂

f : D → Bool
f c₁ = true
f c₂ = false

Limited testing suggests that the @0 annotation does not have any effect on type-checking or compilation.