From bbe2385363cfaf70a0026fca28e592f71e67a659 Mon Sep 17 00:00:00 2001
From: Dale Wijnand <dale.wijnand@gmail.com>
Date: Mon, 1 Feb 2021 14:42:42 +0000
Subject: [PATCH] Emit exhaustivity warning despite uninhabited types

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).
---
 .../tools/nsc/transform/patmat/Logic.scala    |  5 +++-
 test/files/neg/t8511.check                    | 11 +++++++
 test/files/neg/t8511.scala                    | 30 +++++++++++++++++++
 3 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 test/files/neg/t8511.check
 create mode 100644 test/files/neg/t8511.scala

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 593ceb92ea19..41f7a4f84414 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -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
diff --git a/test/files/neg/t8511.check b/test/files/neg/t8511.check
new file mode 100644
index 000000000000..1b9d60455acb
--- /dev/null
+++ b/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
diff --git a/test/files/neg/t8511.scala b/test/files/neg/t8511.scala
new file mode 100644
index 000000000000..6d96eda0b0e0
--- /dev/null
+++ b/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)) =>
+      ???
+  }
+}