Patmat exhaustivity checks do not consider all possible type children

[abgruszecki]

There are (at least) two cases in which children of a type are not considered in patmat exhaustivity checks. I'm making a single issue, since it seems that the solution will have to handle both of these problems at once.

When compiling the following code:

sealed trait IntegralNumber

object IntegralNumber {
  object NaN extends IntegralNumber
  object NotNaN extends IntegralNumber

  sealed abstract class FiniteNumberImpl[N](val value: N) extends IntegralNumber
  sealed class IntNumber(value: Int) extends FiniteNumberImpl[Int](value)

  def test(o: IntegralNumber) = o match {
    case NaN => -1
  }

}

the following warning is emitted:

10 |  def test(o: IntegralNumber) = o match {
   |                                ^
   |                                match may not be exhaustive.
   |
   |                                It would fail on: NotNaN

Note that IntNumber is valid input to test. This happens, since SpaceEngine#refine initializes FiniteNumberImp[N] to FiniteNumberImpl[Any], and then (correctly) when FiniteNumberImpl[Any] is decomposed, IntNumber is ousted.

On a somewhat related note, traits also are ousted too eagerly when refined types are involved. When compiling the following code:

sealed trait T
object O1 extends T
object O2 extends T { val x: Int = 0 }

sealed trait TT extends T
object O3 extends TT { val x: Int = 0 }

sealed trait Eliminated extends T

object O {
  def m(t: T { val x: Int }) = t match {
    case _: Eliminated => ;
  }
}

the following warning is emitted:

11 |  def m(t: T { val x: Int }) = t match {
   |                               ^
   |                               match may not be exhaustive.
   |
   |                               It would fail on: O2

This happens, since SpaceEngine#refine cannot instantiate TT such that it is a subtype of T { val x: Int } and removes it, even though its children can (and do) fulfill the refinement.

@liufengyun - this is as far as I've gotten with this issue. I tried to adjust instantiate to handle these cases correctly, but that seems a bit too difficult for me now.

[liufengyun]

Thanks for reporting @AleksanderBG . The first case is a regression when we switch to instantiation of children based on type inference.

The second is indeed due to the fact that refine ousted too early. If a child is Trait, then we should keep that child without checking.