void.ktn

// Uninhabited type, value-kinded
type Void {}
// or:
// type synonym Void as type (VOID);

// Uninhabited type, poly-kinded
type VOID<K> as K {}
// or (wibbles):
// type VOID as <K> K {}
// type<K> VOID as K {}

// Unary constructive negation
type synonym Not<T> (T -> Void)

// Variadic/polymorphic constructive negation
type synonym NOT<...R> (...R -> VOID);
// or:
// type synonym NOT<K as kind, X as K> (X -> VOID)

// Ex falso quodlibet
define impossible<...R, ...S> (...R, Void -> ...S):
  // Note no ‘+Fail’ because all 0 cases are matched.
  match {}

// A functor of void must be empty
define vacuous<F<_>, A> (F<Void> -> F<A> where Functor<F>):
  \impossible map

// Various instances (non-exhaustive)
instance show (Void -> Text): impossible
instance compare (Void, Void -> Ordering): impossible