RFR: 8325215: Incorrect not exhaustive switch error

[Vicente Romero]

On Wed, 21 Feb 2024 14:48:54 GMT, Jan Lahoda <jlahoda at openjdk.org> wrote:

> Consider code like:
> 
> public class Test {
> 
>     sealed interface A permits T, U {}
>     sealed interface B permits V, W {}
>     static final class T implements A {}
>     static final class U implements A {}
>     static final class V implements B {}
>     static final class W implements B {}
>     final static record R(A a, B b) {}
> 
>     static int r(R r) {
>         return switch (r) {
>             case R(A a, V b) -> 1;
>             case R(T a, W b) -> 2;
>             case R(U a, W b) -> 3;
>         };
>     }
> }
> 
> 
> javac will correctly consider this to be exhaustive, as `R(T a, W b)` and `R(U a, W b)` can be merged into `R(A a, W b)`, and then `R(A a, V b)` and `R(A a, W b)` are merge into `R(A a, B b)` and then into `R`.
> 
> But, if we replace `R(T a, W b)` with a more general `R(T a, B b)`, which matches everything that `R(T a, W b)` does:
> 
> public class Test {
> 
>     sealed interface A permits T, U {}
>     sealed interface B permits V, W {}
>     static final class T implements A {}
>     static final class U implements A {}
>     static final class V implements B {}
>     static final class W implements B {}
>     final static record R(A a, B b) {}
> 
>     static int r(R r) {
>         return switch (r) {
>             case R(A a, V b) -> 1;
>             case R(T a, B b) -> 2;
>             case R(U a, W b) -> 3;
>         };
>     }
> }
> 
> 
> Leads to:
> 
> $ javac /tmp/Test.java
> /tmp/Test.java:12: error: the switch expression does not cover all possible input values
>         return switch (r) {
>                ^
> 1 error
> 
> 
> The issue is that the exhaustivity algorithm is no longer able to merge `R(T a, B b)` and `R(U a, W b)` into `R(A a, W b)`, as the second nested pattern is not the same.
> 
> The rules permit replacing patterns with more strict patterns, i.e. it is permitted to replace `R(T a, B b)` with `R(T a, W b)`, and hence proceed with the merging as in the original case. The trouble is that doing such conversions may lead to high computational complexity.
> 
> The proposal in this patch is to replace all binding patterns in all patterns with their transitive permitted subtypes, but only once, and only if the algorithm fails to determine the exhaustiveness using the standing approach. This may lead to a potentially significant performance penalty, but only in case where the algorithm would mark the switch exhaustive.
> 
> The main alternative to this proposal would be to allow the algorithm to see `B` and `W` as equivalent when attempting to merge  `R(T a, B b)` and `R(U a, W b)`. But, currently, this equivalence ch...

lgtm

-------------

Marked as reviewed by vromero (Reviewer).

PR Review: https://git.openjdk.org/jdk/pull/17949#pullrequestreview-1897020897