Empty exhaustive switches and the ability to refine type variables

[Tesla Zhang]

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', see https://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