Integrated: 8325215: Incorrect not exhaustive switch error

[Jan Lahoda]

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...

This pull request has now been integrated.

Changeset: cb809f8e
Author:    Jan Lahoda <jlahoda at openjdk.org>
URL:       https://git.openjdk.org/jdk/commit/cb809f8e04c12f0d06237c9c3fd05f6c585098a6
Stats:     130 lines in 2 files changed: 128 ins; 1 del; 1 mod

8325215: Incorrect not exhaustive switch error

Reviewed-by: vromero

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

PR: https://git.openjdk.org/jdk/pull/17949