-
Notifications
You must be signed in to change notification settings - Fork 6.1k
8367530: The exhaustiveness errors could be improved #27256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: pr/27253
Are you sure you want to change the base?
Conversation
👋 Welcome back jlahoda! A progress list of the required criteria for merging this PR into |
❗ This change is not yet ready to be integrated. |
|
Consider code like:
This is missing a case for
Root(R2(R2 _), R2(R2 _))
. javac will produce an error correctly, but the error is not very helpful:The goal of this PR is to improve the error, at least in some cases to something along these lines:
The (very simplified) way it works in a recursive (or induction) way:
This approach relies heavily on our ability to compute exhaustiveness, which is evaluated repeatedly in the process.
There are some cases where the algorithm does not produce ideal results (see the tests), but overall seems much better than what we have now.
Another significant limitation is the speed of the process. Evaluating exhaustiveness is not a fast process, and this algorithm evaluates exhaustiveness repeatedly, potentially for many combinations of patterns (esp. for record patterns). So part of the proposal here is to have a time deadline for the computation. The default is 5s, and can be changed by
-XDexhaustivityTimeout=<timeout-in-ms>
.There's also an open possibility for select tools to delay the more detailed computation to some later time, although that would need to be tried and evaluated.
Progress
Integration blocker
Issue
Reviewing
Using
git
Checkout this PR locally:
$ git fetch https://git.openjdk.org/jdk.git pull/27256/head:pull/27256
$ git checkout pull/27256
Update a local copy of the PR:
$ git checkout pull/27256
$ git pull https://git.openjdk.org/jdk.git pull/27256/head
Using Skara CLI tools
Checkout this PR locally:
$ git pr checkout 27256
View PR using the GUI difftool:
$ git pr show -t 27256
Using diff file
Download this PR as a diff file:
https://git.openjdk.org/jdk/pull/27256.diff
Using Webrev
Link to Webrev Comment