Type-emptiness testing should produce witness

[jclark]

In a case where a type S is expected to be a subtype of type T, we test whether the set difference of S and T is empty, and then give an error if not. This results in an error message that is not very informative, particularly when S and T are complicated.

We can do better by making the API that tests whether a set is empty produce a witness (or perhaps multiple witnesses) in the case that it is not empty. The witness is a value (a shape) that is in the set. The error message can then include a description of the witness in the error message.

[jclark]

Draft PR in #1040