#[fail "but cases for"]
def missing-b : {a, b} → {a} =
  λ x ⇒ case x return {a} of { 'a ⇒ 'a }

#[fail "duplicate arms"]
def repeat-enum-case : {a} → {a} =
  λ x ⇒ case x return {a} of { 'a ⇒ 'a; 'a ⇒ 'a }

#[fail "duplicate tags"]
def repeat-enum-type : {a, a} = 'a

#[fail "double-def.X has already been defined"]
namespace double-def {
  def0 X : ★ = {a}
  def0 X : ★ = {a}
}