Expected "the type test for <blah> cannot be checked at runtime" warning but none were produced

[winestone]

Compiler version

3.2.1 from https://repo1.maven.org/maven2/org/scala-lang/scala3-compiler_3/3.2.1/scala3-compiler_3-3.2.1.jar

Minimized code

Given some generic class (in this case Wrapper) and some other type (in this case Color but I think this doesn't matter too much):

case class Wrapper[A](value: A)
enum Color:
  case Red, Green

The following code doesn't produce any warnings I think but I expect "the type test for <blah> cannot be checked at runtime":

def test_wrong(x: Wrapper[Color]): Option[Wrapper[Color.Red.type]] =
  x match
    case x: Wrapper[Color.Red.type] => Some(x)
    case _                          => None

def test_wrong_seq(xs: Seq[Wrapper[Color]]): Seq[Wrapper[Color.Red.type]] =
  xs.collect { case x: Wrapper[Color.Red.type] => x }

Output

println(test_wrong_seq(Seq(Wrapper(Color.Red), Wrapper(Color.Green))))
// outputs: List(Wrapper(Red), Wrapper(Green))

The output is expected but no warnings is not expected.

Expectation

What I expect when pattern matching on the type is:

def test_correct(x: Wrapper[Color]): Option[Wrapper[Color.Red.type]] =
  x match
    case x: Wrapper[Color.Red.type]   => Some(x)
    case x: Wrapper[Color.Green.type] => None

gives "the type test for <blah> cannot be checked at runtime":

[warn] -- [E029] Pattern Match Exhaustivity Warning: Example.scala:147:6
[warn] 147 |      x match
[warn]     |      ^
[warn]     |      match may not be exhaustive.
[warn]     |
[warn]     |      It would fail on pattern case: Wrapper(_)
[warn]     |
[warn]     | longer explanation available when compiling with `-explain`
[warn] -- [E030] Match case Unreachable Warning: Example.scala:152:13
[warn] 152 |        case x: Wrapper[Color.Red.type] => Some(x)
[warn]     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^
[warn]     |             Unreachable case
[warn] -- Unchecked Warning: Example.scala:148:13
[warn] 148 |        case x: Wrapper[Color.Red.type]   => Some(x)
[warn]     |             ^
[warn]     |the type test for Wrapper[(Color.Red : => Color)] cannot be checked at runtime
[warn] -- Unchecked Warning: Example.scala:149:13
[warn] 149 |        case x: Wrapper[Color.Green.type] => None
[warn]     |             ^
[warn]     |the type test for Wrapper[(Color.Green : => Color)] cannot be checked at runtime

Hopefully this isn't a duplicate! I did some searching but I could always have missed something.

[SethTisue]

Dale and I looked at this for a while today. Yes, we agree it's a bug. Unfortunately we had to stop before we reached any very definite conclusions about what's going on, and we won't be able to get back to it until later this month.

[dwijnand]

So many parts to this.

1. Anonymous partial function syntax is desugared to have a @unchecked annotated selector, which makes sense in terms of not having it emit exhaustivity and reachability warnings, but a compiler inserted @unchecked there shouldn't also suppress type test warnings - but it does at the moment.

2. If you write out the match part, as in xs.collect { x => x match .. then you... still don't get the unchecked warning. You get instead an unreachable warning (like above) on case x: Wrapper[Color.Red.type]. And once you get an unreachable warning, you don't also see the uncheckable warning because it's on the same position (and there's "isHidden" logic against that).

3. Why the unreachable warning? Well, when calculating the values (i.e. the space engine logic) that case Wrapper[Color.Red.type] covers against a Wrapper[Color] scrutinee, well the intersection is empty, because, as a HK type invariant in its type parameter, neither is a subtype of the other. Then provablyDisjoint is run and.. well they're declared disjoint, with this prose:

        // In the invariant case, we also use a stronger notion of disjointness:
        // we consider fully instantiated types not equal wrt =:= to be disjoint
        // (under any context). This is fine because it matches the runtime
        // semantics of pattern matching. To implement a pattern such as
        // `case Inv[T] => ...`, one needs a type tag for `T` and the compiler
        // is used at runtime to check it the scrutinee's type is =:= to `T`.
        // Note that this is currently a theoretical concern since Dotty
        // doesn't have type tags, meaning that users cannot write patterns
        // that do type tests on higher kinded types.
        def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =

4. So then why do we see the uncheckable warnings in test_correct? Well, because we only emit unreachable warnings if and when we finally hit a case that can prove isn't empty. In test_wrong we have a default case, so once we hit that, we unbuffer the unreachable warning we determined on the first case. In test_correct, both (i.e. all) cases are unreachable, so we don't emit any warnings, because we can't really say "this case is unreachable because it's already handled by this other one". The example we have in the compiler is Tree.ThisTree is a subtype of Tree and has no subtypes, but we often pattern match it against various Tree subclasses - those are unreachable cases.

To be continued...

[SethTisue]

It's part 1 that concerns me by far the most, though the rest is concerning as well. Throwing an @unchecked blanket over the whole thing is... alarming to me.

Do we need to introduce @uncheckedExhaustivity, or is there some existing thing we can reuse? (Or can the fact that the context is a partial function be determined without having to annotate at all...?)