Agda-2.3.2.2: test/fail/ShouldBeEmpty.agda

module ShouldBeEmpty where

data Zero : Set where
data One : Set where
  one : One

ok : Zero -> One
ok ()

bad : One -> One
bad ()