Rewrite the exhaustiveness specification. (#2948)

* Rewrite the exhaustiveness specification.

This is based on Johnni's excellent implementation. I tried to follow
the semantics of the implementation as closely as I could, and mostly
stuck to the terminology too. The main change is that the implementation
uses "type" to also sort of do some restriction stuff, and I tried to
keep that separate here such that a "type" on a space always refers to
a static type.

* Revise.

* Fixes from Sergey.

Author: munificent