errors/NoRHSRequiresAbsurdPattern.agda:11,1-6
The right-hand side can only be omitted if there is an absurd
pattern, () or {}, in the left-hand side.
when checking that the clause bad h has type {A : Set} -> Zero -> A