Emit exhaustivity warning despite uninhabited types

src/compiler/scala/tools/nsc/transform/patmat/Logic.scala

@@ -410,7 +410,7 @@ trait Logic extends Debugging  {
     def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop]) = {
       val start = if (StatisticsStatics.areSomeColdStatsEnabled) statistics.startTimer(statistics.patmatAnaVarEq) else null
 
-      val vars = new mutable.HashSet[Var]
+      val vars = new mutable.LinkedHashSet[Var]
 
       object gatherEqualities extends PropTraverser {
         override def apply(p: Prop) = p match {
@@ -437,12 +437,25 @@ trait Logic extends Debugging  {
 
       debug.patmat("removeVarEq vars: "+ vars)
       vars.foreach { v =>
+        val isScrutineeVar = v == vars.head
+
         // if v.domainSyms.isEmpty, we must consider the domain to be infinite
         // otherwise, since the domain fully partitions the type of the value,
         // 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 the domain is knonw to be empty
+          // only add that axiom if the var is the scrutinee
+          // which has the effect of wiping out the whole formula
+          // (because `\/(Set.empty) == False`)
+          // otherwise it's just a subvariable of a match expression
+          // which has no domain (i.e. an unreachable branch)
+          // but it shouldn't wipe out the whole exhaustivity check
+          // neg/t8511 vs (pos/t6146 or neg/virtpatmat_exhaust_compound.scala)
+          if (isScrutineeVar || dsyms.nonEmpty)
+            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

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

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)) =>
+      ???
+  }
+}