ShouldBeEmpty.agda:12,1-7
One should be empty, but the following constructor patterns are
valid:
  one
when checking that the clause bad () has type One → One