Missing unreachable case warnings

[smarter]

Given:

trait Foo
class One extends Foo
class Two extends Foo
class Three extends Foo

object Test {
  def test(f: Foo) = f match {
    case f: Foo =>
    case f: One =>
    case f: Two =>
    case f: Three =>
  }
}

We should get three warnings since the three last cases are not reachable, but we only get one for the last case:

-- [E120] Only null matched Warning: try/caseun.scala:11:9 ---------------------
11 |    case f: Three =>
   |         ^^^^^^^^
   |         Only null is matched. Consider using `case null =>` instead.

(The warning itself is a bit confusing but that's a separate issue: #4660)

[liufengyun]

@smarter Current implementation only check for the last case because the computation is a little expensive (much more than unreachable case analysis). We can still do the analysis for all cases, and see how it impacts performance.

[abeln]

I think there are several things going on here:

• The code in Space.scala actually does the unreachability check (I think) for every case and not only the last one: see https://github.com/lampepfl/dotty/blob/efb8115982cbb18aa7eed05f10b13b654e80acb5/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala#L964

• The question is why is it then not triggered for the second and third cases above? A little bit of debugging shows that there's a mismatch between the projection and intersection operations on spaces.

        val curr = project(pat)

        debug.println(s"---------------reachable? ${show(curr)}")
        debug.println(s"prev: ${show(prevs)}")

        var covered = simplify(intersect(curr, targetSpace))
        debug.println(s"covered: $covered")

The code above is what runs in a loop for the reachability checks.
When we project the pattern, the space we get is of the form Typ(x), but after the intersection we get an Or(x, null) space.

Looking at how we explicitly add a nullType to targetSpace https://github.com/lampepfl/dotty/blob/efb8115982cbb18aa7eed05f10b13b654e80acb5/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala#L928), it seems that the intention is that Typ(x) types, when viewed as sets, don't include null. This also matches the definition of isSubType.

However, within intersect and specifically intersectUnrelatedAtomicTypes, there's a precondition that uses the weaker <:< (normal subtyping) relation, instead of isSubType.

  override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
    val and = AndType(tp1, tp2)
    // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
    // Then, no leaf of the and-type tree `and` is a subtype of `and`.
val res = inhabited(and)

This means that when we intersect Typ(Foo) with nullType, we end up constructing an AndType in intersectUnrelatedAtomicTypes (because neither is a subtype in the isSubType sense), but the AndType ends being just nullType (because it uses the regular notion of subtyping).

One solution, it seems to me, is to handle the null case separately when intersecting things, as in the proposed commit above: abeln@7d7a7d1

Incidentally, that also fixes #4660 as well.

@liufengyun does that make sense? What do you guys think?

[liufengyun]

Thanks a lot for the in-depth diagnosis @abeln , I think that is the right fix. Could you please make a PR?