Skip to content
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

Emit exhaustivity warning despite uninhabited types #9474

Merged
merged 1 commit into from Feb 3, 2021

Conversation

@dwijnand
Copy link
Member

@dwijnand dwijnand commented Feb 1, 2021

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

@scala-jenkins scala-jenkins added this to the 2.13.5 milestone Feb 1, 2021
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).
@dwijnand dwijnand force-pushed the patmat-unapply-uninhabited-sealed branch from bbe2385 to 335aae6 Feb 3, 2021
@dwijnand dwijnand requested review from lrytz, retronym and SethTisue Feb 3, 2021
lrytz
lrytz approved these changes Feb 3, 2021
Copy link
Member

@lrytz lrytz left a comment

LGTM, thanks for the good explanation 👍

}

object EntryPoint {
def main(args: Array[String]) {
Copy link
Member

@lrytz lrytz Feb 3, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

procedure syntax

@dwijnand dwijnand merged commit 039aec1 into scala:2.13.x Feb 3, 2021
3 checks passed
@dwijnand dwijnand deleted the patmat-unapply-uninhabited-sealed branch Feb 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
3 participants