#2420. Add extension types exhaustiveness tests. Maps

[sgrekhov]

No description provided.

[eernstg]

There is some amount of confusion in the @assertion and @description, that should probably be revised (perhaps some older tests have the same?).

In addition to this, I think it would be useful to take the opportunity to test that a switch expression is exhaustive when it exhausts all maps of the given type. This shows that an extension type whose representation type is Map<K, V> for some K and V is actually treated like its representation type during exhaustiveness computations.

[sgrekhov]

However, in this context it could be useful to add an extra test: Start with the same patterns, just so we have something for the exhaustiveness algorithm to work with, and then end with an exhaustive pattern like Map().

A very good idea, thank you! Added this tests and updated descriptions/assertions (including original patterns tests). Please take another look

[eernstg]

LGTM!

The whole notion of showing that a particular kind of switch expression 'cannot be exhaustive' is questionable: We're promising that we have tried all possible ways to make it exhaustive, and there is no way that works.

The reality is that any attempt to do this would potentially fail because we've forgotten a particularly smart thing that we might have done. So we've found a bunch of switch expressions that aren't exhaustive (not a hard task ;-), but it would then still be false that this kind of pattern 'cannot be exhaustive'.

We do have delicate properties like this (for example: soundness—there is no program that will make a variable of type T have a value of type S unless S <: T"), but they are really difficult to get right in an absolute sense, so we just keep trying to improve on them and eliminate failures (in this case: failures to maintain soundness).

I don't think there's a need to play around with the wording any more, but it's probably a good idea to keep in mind that this kind of quantification over all possible something (all programs, all expressions, whatever) is delicate to get right, and we may just choose to avoid promising anything of that kind, unless we specifically need to do that.