Incorrect or missing exhaustivity warning when using type tests

[smarter]

This produces no warning, but is not exhaustive:

sealed trait Foo
final case class Bar[A](a: A) extends Foo

def test(x: Foo) = x match {
  case Bar(a: Int) =>
}

This produces both an inexhaustivity and unchecked warnng, but it is exhaustive because of erasure:

sealed trait Foo
final case class Bar[S](s: S => Unit) extends Foo

def test(x: Foo) = x match {
  case Bar(s: (Any => Unit)) =>
}

-- [E029] Pattern Match Exhaustivity Warning: try/ce.scala:19:19 ---------------
19 |def test(x: Foo) = x match {
   |                   ^
   |                   match may not be exhaustive.
   |
   |                   It would fail on pattern case: Bar(_)

longer explanation available when compiling with `-explain`
-- Warning: try/ce.scala:20:11 -------------------------------------------------
20 |  case Bar(s: (Any => Unit)) =>
   |           ^^^^^^^^^^^^^^^^
   |           the type test for Any => Unit cannot be checked at runtime

(Adding a case Bar(_) => should in fact produce an unreachability warning).

[liufengyun]

There is at some point an intentional change to not reason in erasure semantics for exhaustivity check, and leave them to typetest check in later phases.

One motivation is to better support GADT:

sealed trait Expr[T]
case class IntExpr(x: Int) extends Expr[Int]
case class BooleanExpr(b: Boolean) extends Expr[Boolean]

def foo[T](x: Expr[T], y: Expr[T]) = (x, y) match {
    case (IntExpr(_), IntExpr(_)) =>
    case (BooleanExpr(_), BooleanExpr(_)) =>
}

In the code above, if we reason in terms of type erasure, then the scrutinee has the type (Expr[_], Expr[_]) instead of (Expr[T], Expr[T]) --- we lose the constraint that the two components are of the same type.

[Swoorup]

Related: #12652 ?

[dwijnand]

What about the other case, the one about the nested a: Int going unmentioned? The exhaustivity warning not taking in account the "uncheckability" of certain type tests (i.e. the second example) seems so minor in comparison.

[liufengyun]

What about the other case, the one about the nested a: Int going unmentioned? The exhaustivity warning not taking in account the "uncheckability" of certain type tests (i.e. the second example) seems so minor in comparison.

Good catch, I missed that part. I'll propose a fix for it.