Integrated: 8311815: Incorrect exhaustivity computation

[Jan Lahoda]

On Thu, 13 Jul 2023 15:22:02 GMT, Jan Lahoda <jlahoda at openjdk.org> wrote:

> Consider code like:
> 
> class Test22 {
> 
>   record Pair(I i1, I i2) {}
> 
>   sealed interface I {}
> 
>   record C() implements I {}
> 
>   record D() implements I {}
> 
>   void exhaustinvenessWithInterface(Pair pairI) {
>     switch (pairI) {
>       case Pair(D fst, C snd) -> {}
>       case Pair(C fst, C snd) -> {}
>       case Pair(C fst, I snd) -> {}
>       case Pair(D fst, D snd) -> {}
>     }
>   }
> } 
> 
> 
> when evaluating exhaustivity, the outcome is wrong: if `Pair(D fst, C snd)` and `Pair(C fst, C snd)` get merged into `Pair(I _, C_)` (and the existing patterns are removed from the pattern set), the remaining patterns are `Pair(I _, C_)`, `Pair(C fst, I snd)` and `Pair(D fst, D snd)`. The existing implementation does not know how to continue from here (it would need to replace `Pair(C fst, I snd)` with `Pair(C fst, D snd)`, which would allow to unify `Pair(C fst, D snd)` and `Pair(D fst, D snd)` into `Pair(I _, D _)` and then continue, but that is tricky, as such speculation may not lead to a good result, and we would need to implement backtracking).
> 
> But, if `Pair(D fst, C snd)` and `Pair(D fst, D snd)` was merged into `Pair(D _, I _)`, it could then be merge with `Pair(C fst, I snd)` to produce `Pair(I _, I _)`.
> 
> The proposal here is aiming to allow the second path, by not removing the existing patterns when merging sealed subtypes. I.e. starting with `{Pair(D _, C _), Pair(C _, C_), Pair(C _, I _), Pair(D _, D _)}`, we would merge to `{Pair(D _, C _), Pair(C _, C_), Pair(C _, I _), Pair(D _, D _), *Pair(I _, C_)*}`, and then `{Pair(D _, C _), Pair(C _, C_), Pair(C _, I _), Pair(D _, D _), Pair(I _, C_), *Pair(D _, I _)*}`, which would then lead to `Pair(I _, I _)`, leading to `Pair` and confirmed exhaustivity.
> 
> This can be achieved easily by not removing binding in `reduceBindingPatterns`. The problem is that when we stop removing bindings, the algorithm may get into an infinite loop re-adding the same binding over and over. The solution to that is using Sets instead of Lists. To make the algorithm faster and more stable, there are two more additions: a) all record patterns covered by binding patterns are removed from the pattern set; b) `reduceNestedPatterns` attempts to produce results for all mismatching positions without returning (otherwise the algorithm may constantly only process the first mismatching position without progressing).

This pull request has now been integrated.

Changeset: a4412166
Author:    Jan Lahoda <jlahoda at openjdk.org>
URL:       https://git.openjdk.org/jdk/commit/a4412166ec8526db5e5e8e1ca324f86124055b30
Stats:     102 lines in 2 files changed: 55 ins; 24 del; 23 mod

8311815: Incorrect exhaustivity computation

Reviewed-by: vromero

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

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