Empty exhaustive switches and the ability to refine type variables

[Brian Goetz]

I think I may have misunderstood your earlier question.  An 
uninhabitable switch is one over a sealed type for which none of the 
type patterns apply, such as:

     sealed interface X<T> { }
     final class A implements X<String> {}
     final class B implements X<Integer> {}

     X<Frog> x = ...
     switch (x) {
         // none of the subtypes of X are applicable
     }

So this would fall out as a natural consequence of eliminating 
inapplicable choices.

In any case, the issues surrounding GADTs are more than just 
exhaustiveness; you mention type refinement, and there are also other 
consequences for type checking.  These are going to take a while to work 
through.  Rest assured they're on our radar.

On 3/22/2022 4:13 PM, Tesla Zhang wrote:
> Greetings,
>
> I asked if empty switch (the switched expression has an uninhabitable type so no case clause is needed) would be possible because the second preview of switch expressions allows refuting patterns, and Brian told me it's 'unlikely', seehttps://mail.openjdk.java.net/pipermail/amber-dev/2021-November/007161.html. I still don't understand why it's unlikely, because for example
>
>
> sealed interface I<T> {}
> record R() implements I<String> {}
> <T> T test(I<Integer> i) { return switch (i) { <what to do here?> }; }
>
>
> The switch should be well-typed without any case, which is a counterexample.
>
>
> Apart from that, Brian also mentioned a 'probable bug' in https://mail.openjdk.java.net/pipermail/amber-dev/2021-November/007156.html  related to casting refinable types, is that addressed now? I explored the mailing list archive but I didn't find relevant discussions. I think it would be very nice for javac to be able to refine a local type.
>
>
> Best regards,
> Tesla