RFR: 8364991: Incorrect not-exhaustive error

[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 switches. The implementation approach javac is using so far is that it does not remove some of the reduced patterns from the set. So, it can use the pattern again, and hence basically pick a different reduction path. But, it fails here, and if we would keep the relevant patterns here in the set, the overall performance would be too bad.

So, this PR proposes that, when reducing a sub-set of patterns to another set of patterns, javac keeps a record that the new pattern(s) originate in specific original pattern(s), and if it needs to, it will look into this record when searching for possible reductions. javac does "fast reduction rounds" normally using hashes, but if it fails to find reductions using the fast approach, it switches to a (much) slower approach that uses plain subtyping instead of hashes. The new approach to search for reductions proposed herein is part of this slow round only.

So, basically, the new chain after this PR is roughly:

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 _)
=> javac does not find anything it can reduce in the first stage, and will look at the original patterns. It will find out that Root(R2 _, R2(R1 _)) originates in Root(R2(R1 _), R2(R1 _)),  Root(R2(R2 _), R2(R1 _)), and that it could reduce (second component mismatching): Root(R2(R1 _), R2(R1 _)), Root(R2(R1 _), R2(R2 _)) => Root(R2(R1 _), R2 _)
Root(R2 _, R2(R1 _)), Root(R2(R1 _), R2 _), Root(R2(R2 _), R2 _)
=> as before, 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(R1 _)), Root(R2 _, R2 _)
=>
Root _
=>
exhaustive

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

Commit messages:
 - Adding test.
 - Adjusting to spec.
 - Merge branch 'master' into JDK-8364991
 - Improving test debuggability.
 - 8364991: Incorrect not-exhaustive error

Changes: https://git.openjdk.org/jdk/pull/27247/files
  Webrev: https://webrevs.openjdk.org/?repo=jdk&pr=27247&range=00
  Issue: https://bugs.openjdk.org/browse/JDK-8364991
  Stats: 155 lines in 2 files changed: 130 ins; 0 del; 25 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