Potentially spurious exhaustivity warning when matching on a type with contravariant type param

[KacperFKorban]

Compiler version

3.2.1-RC1-bin-20220831-398b72e-NIGHTLY compiles without warnings with 3.2.0-RC1

Minimized code

sealed trait T[-U]
final case class C[U]() extends T[U]

def f[U](ua: T[U]) = ua match {
  case ua: C[U] @unchecked => ???
}

Output

[warn] ./turboliftbug.scala:4:22: match may not be exhaustive.
[warn] 
[warn] It would fail on pattern case: C()
[warn] def f[U](ua: T[U]) = ua match {
[warn]                      ^^

Expectation

No warning. (possibly)

I'm not 100% sure if the warning is correct or not. But this is a CB (https://github.com/lampepfl/dotty/issues/15949) fail, so decided to create an issue either way.

My reasoning is: Since C.U is invariant and T.U is contravariant, then the match can still fail on C[Any]. Though scala 2.13.8 doesn't give a warning here.

[prolativ]

Calling f(C()) seems not to fail work at runtime. So to me it seems the warning should not be there. @dwijnand could you confirm that?

[KacperFKorban]

It might be the case that the calculated spaces are correct in theory, but because the test for C[U] cannot be checked it ends up being exhaustive.

[dwijnand]

Yeah, the space engine doesn't seem to take in consideration that we want to ignore the type argument component.

[SethTisue]

I agree that no exhaustivity warning should be issued, regardless of whether @unchecked is present. For two reasons:

1. There is no possibility of a runtime MatchError. The whole point of an exhaustivity warning is to alert you to a possible MatchError, but there isn't one.
2. If I write C[U], then despite the U being uncheckable, the compiler will believe me and assume that in the case body, ua has type C[U]. It's making that assumption anyway, so it seems logical to me for the same assumption to also be made in exhaustivity checking.

(Perhaps 1 merely restates @prolativ, and 2 merely restates @KacperFKorban.)