Skip to content

Commit

Permalink
Emit exhaustivity warning despite uninhabited types
Browse files Browse the repository at this point in the history
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.

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).
  • Loading branch information
dwijnand committed Feb 1, 2021
1 parent 0ab9086 commit bbe2385
Show file tree
Hide file tree
Showing 3 changed files with 45 additions and 1 deletion.
5 changes: 4 additions & 1 deletion src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
Expand Up @@ -442,7 +442,10 @@ trait Logic extends Debugging {
// exactly one of the types (and whatever it implies, imposed separately) must be chosen
// consider X ::= A | B | C, and A => B
// coverage is formulated as: A \/ B \/ C and the implications are
v.domainSyms foreach { dsyms => addAxiom(\/(dsyms)) }
v.domainSyms foreach { dsyms =>
if (dsyms.nonEmpty) // neg/t8511 avoid adding "False" which is ANDed, wiping out the whole proposition
addAxiom(\/(dsyms))
}

// when this variable cannot be null the equality corresponding to the type test `(x: T)`, where T is x's static type,
// is always true; when the variable may be null we use the implication `(x != null) => (x: T)` for the axiom
Expand Down
11 changes: 11 additions & 0 deletions test/files/neg/t8511.check
@@ -0,0 +1,11 @@
t8511.scala:28: warning: unreachable code
???
^
t8511.scala:23: warning: match may not be exhaustive.
It would fail on the following inputs: Bar(_), Baz(), EatsExhaustiveWarning(_)
private def logic(head: Expr): String = head match {
^
warning: 1 deprecation (since 2.13.0); re-run with -deprecation for details
error: No warnings can be incurred under -Werror.
3 warnings
1 error
30 changes: 30 additions & 0 deletions test/files/neg/t8511.scala
@@ -0,0 +1,30 @@
// scalac: -Werror
sealed trait Expr
final case class Foo(other: Option[String]) extends Expr
final case class Bar(someConstant: String) extends Expr
final case class Baz() extends Expr
final case class EatsExhaustiveWarning(other: Reference) extends Expr

sealed trait Reference {
val value: String
}

object Reference {
def unapply(reference: Reference): Option[(String)] = {
Some(reference.value)
}
}

object EntryPoint {
def main(args: Array[String]) {
println("Successfully ran")
}

private def logic(head: Expr): String = head match {
case Foo(_) =>
???
// Commenting this line only causes the exhaustive search warning to be emitted
case EatsExhaustiveWarning(Reference(text)) =>
???
}
}

0 comments on commit bbe2385

Please sign in to comment.