Description
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.