Emit exhaustivity warning despite uninhabited types #9474
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
An abstract sealed class with no subtypes is uninhabited (ignoring null
for 1 second). Previously the pattern matcher added an eq axiom of
"False" in this case, which wipes out the whole formula as the axioms
are AND-ed together and with the rest of the pure prop formula.
Keeping the definitions of enumerateSubtypes and domain/domainSyms as
they are, I believe it's correct to fix this locally to removeVarEq.
The branch is dead (indeed it gets a reachability warning) but that
shouldn't preclude the emission of exhaustivity warnings.
However, we should continue to wipe out the formula when the domain is
that of the scrutinee variable. While I was at it I made the variable
ordering insertion order, which makes it deterministic.
One additional consideration is modelNull/NullConst. When that is
present then the domain symbols won't be empty as it will contain the
symbol reflecting the proposition that the variable may be null. In a
such case it's right to continue to add it as an axiom, because even
"uninhabited" types may be inhabited by "null" (sadly).
Fixes scala/bug#8511