Introduce empty type

Motivation

It would be nice to have an uninhabited type. After the introduction of lightweight entrypoints feature it would allow for better modularity.

In particular, imagine a contract template in some language over Michelson:

parameter or (int %callA) (or (nat %callB) p)
storage ...
code { UNPAIR; IF_LEFT {doA} { IF_LEFT {doB} {doOther} } }

This contract defines a set of his own basic entrypoints (callA and callB) common for several concrete contracts, and leaves a place for other entrypoints via p type variable and doOther implementation - this concept has already been proposed. A common use case for these entrypoints includes implementing one or several interfaces like FA1.2.

However, sometimes we want to provide no extra entrypoints, and currently there is no way to reflect this properly in types, we need some sort of empty sum type for that. If we use p = unit, then it won't be immediately obvious for the caller of the contract that this entrypoint should not be used, and implementor of the contract will have to resort to some FAILWITH in case the invalid call has happened after all.

I understand that this motivation is minor, but on the other hand, this feature is very small as well: it requires only addition of one type and one instruction, and it makes the type system again expressive enough to cover all imaginary use cases.

Feature set

• empty type

  • Constructors: none
  • Scope: can appear everywhere (constants, storage, parameter, PACK, UNPACK).

• ABSURD instruction

  • Signature: empty : 'S -> 'S1