SI-6008 use static knowledge of success of type tests

augment the equality axioms to take into account that
a type test against the static type of a variable succeeds unless the variable is null

for exhaustivity we disregard null, so the type test always succeeds
during unreachability we model this knowledge as the obvious implication

3 files changed, 14 insertions, 1 deletions

diff --git a/test/files/neg/exhausting.check b/test/files/neg/exhausting.check
index 7140b99428..0f0d13cb33 100644
--- a/test/files/neg/exhausting.check
+++ b/test/files/neg/exhausting.check
@@ -7,7 +7,7 @@ It would fail on the following input: Nil
   def fail2[T](xs: List[T]) = xs match {
                               ^
 exhausting.scala:32: error: match may not be exhaustive.
-It would fail on the following input: List(<not in (1, 2)>)
+It would fail on the following input: List((x: Int forSome x not in (1, 2)))
   def fail3a(xs: List[Int]) = xs match {
                               ^
 exhausting.scala:39: error: match may not be exhaustive.
diff --git a/test/files/pos/t6008.flags b/test/files/pos/t6008.flags
new file mode 100644
index 0000000000..e8fb65d50c
--- /dev/null
+++ b/test/files/pos/t6008.flags
@@ -0,0 +1 @@
+-Xfatal-warnings
\ No newline at end of file
diff --git a/test/files/pos/t6008.scala b/test/files/pos/t6008.scala
new file mode 100644
index 0000000000..84ae19b211
--- /dev/null
+++ b/test/files/pos/t6008.scala
@@ -0,0 +1,12 @@
+// none of these should complain about exhaustivity
+class Test {
+  // It would fail on the following inputs: (_, false), (_, true)
+  def x(in: (Int, Boolean)) = in match { case (i: Int, b: Boolean) => 3 }
+
+  // There is no warning if the Int is ignored or bound without an explicit type:
+  def y(in: (Int, Boolean)) = in match { case (_, b: Boolean) => 3 }
+
+  // Keeping the explicit type for the Int but dropping the one for Boolean presents a spurious warning again:
+  // It would fail on the following input: (_, _)
+  def z(in: (Int, Boolean)) = in match { case (i: Int, b) => 3 }
+}
\ No newline at end of file