RFR: 8364991: Incorrect not-exhaustive error [v8]

[Jan Lahoda]

> Consider this code:
> 
> $ cat Test.java
> package test;
> public class Test {
>     private int test1(Root r) {
>         return switch (r) {
>             case Root(R2(R1 _), R2(R1 _)) -> 0;
>             case Root(R2(R1 _), R2(R2 _)) -> 0;
>             case Root(R2(R2 _), R2(R1 _)) -> 0;
>             case Root(R2(R2 _), R2 _) -> 0;
>         };
>     }
>     sealed interface Base {}
>     record R1() implements Base {}
>     record R2(Base b1) implements Base {}
>     record Root(R2 b2, R2 b3) {}
> }
> 
> 
> javac (JDK 25) will produce a compile-time error for this code:
> 
> $ javac test/Test.java
> .../test/Test.java:4: error: the switch expression does not cover all possible input values
>         return switch (r) {
>                ^
> 1 error
> 
> 
> This error is not correct according to the JLS. JLS defines a set of possible reductions of pattern sets, and if there exists a series of reductions from the pattern set into a pattern set that covers the selector type, the switch is exhaustive.
> 
> One such reduction is that if there's a sub-set of (record) patterns that only differ in one component ("the mismatching component"), we can replace them with a (set of) patterns where this component is reduced, and the other components are unmodified.
> 
> Such path exists here (every line shows a set of patterns that is being transformed):
> 
> Root(R2(R1 _), R2(R1 _)), Root(R2(R1 _), R2(R2 _)), Root(R2(R2 _), R2(R1 _)), Root(R2(R2 _), R2 _)
> => choosing the second component as the mismatching component, then we can reduce Root(R2(R1 _), R2(R1 _)), Root(R2(R1 _), R2(R2 _)) => Root(R2(R1 _), R2 _); as we can reduce R2(R1 _), R2(R2 _) to R2 _
> Root(R2(R1 _), R2 _), Root(R2(R2 _), R2(R1 _)), Root(R2(R2 _), R2 _)
> => choosing the first component as the mismatching component, we can reduce Root(R2(R1 _), R2 _), Root(R2(R2 _), R2 _) => Root(R2 _, R2 _)
> Root(R2 _, R2 _)
> =>
> Root _
> =>
> exhaustive
> 
> 
> The problem here is that in the first step, javac chooses this path:
> 
> Root(R2(R1 _), R2(R1 _)), Root(R2(R1 _), R2(R2 _)), Root(R2(R2 _), R2(R1 _)), Root(R2(R2 _), R2 _)
> => reduce Root(R2(R1 _), R2(R1 _)),  Root(R2(R2 _), R2(R1 _)) => Root(R2 _, R2(R1 _))
> Root(R2 _, R2(R1 _)), Root(R2(R1 _), R2(R2 _)), Root(R2(R2 _), R2 _)
> => dead end, as there are no two patterns that would have the same nested pattern in the same component
> 
> 
> If javac would do full backtracking, it could go back, and choose the other path, and find out the switch is exhaustive. But, full naive backtracking is, I think, prohibitively too slow for even relatively small swit...

Jan Lahoda has updated the pull request with a new target base due to a merge or a rebase. The pull request now contains 15 commits:

 - Merge branch 'master' into JDK-8364991
 - Merge branch 'master' into JDK-8364991
 - Merge branch 'JDK-8367499-2' into JDK-8364991
 - 8367499: Refactor exhaustiveness computation from Flow into a separate class
 - Avoiding the use of IdentityHashMap.
 - Caching isSubtype, as suggested.
 - Adding explanation to the replaces map.
 - Factoring out the 'substitutable' check, as suggested.
 - Adding tests with generic records.
 - Simplifying the code as suggested.
 - ... and 5 more: https://git.openjdk.org/jdk/compare/80fcfaf4...e6a3f0da

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

Changes: https://git.openjdk.org/jdk/pull/27247/files
  Webrev: https://webrevs.openjdk.org/?repo=jdk&pr=27247&range=07
  Stats: 299 lines in 2 files changed: 259 ins; 16 del; 24 mod
  Patch: https://git.openjdk.org/jdk/pull/27247.diff
  Fetch: git fetch https://git.openjdk.org/jdk.git pull/27247/head:pull/27247

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