Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
KacperFKorban opened this issue Sep 4, 2022 · 4 comments · Fixed by #16168
Assignees
Labels
area:pattern-matching itype:bug regression This worked in a previous version but doesn't anymore
Milestone

Comments

@KacperFKorban
Copy link
Member

KacperFKorban commented Sep 4, 2022

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 (#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.

@KacperFKorban KacperFKorban added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Sep 4, 2022
@KacperFKorban KacperFKorban added the regression This worked in a previous version but doesn't anymore label Sep 4, 2022
@prolativ
Copy link
Contributor

prolativ commented Sep 5, 2022

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?

@prolativ prolativ added area:pattern-matching and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Sep 5, 2022
@KacperFKorban
Copy link
Member Author

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
Copy link
Member

dwijnand commented Sep 7, 2022

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

@SethTisue
Copy link
Member

SethTisue commented Oct 7, 2022

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

@dwijnand dwijnand linked a pull request Oct 11, 2022 that will close this issue
dwijnand added a commit to dwijnand/scala3 that referenced this issue Dec 14, 2022
Not doing so, in a context where GADT inferrence is enabled, such as in
TypeOps.refineUsingParent, leads to false inferrences.

Doing so, and removing the previous fix for scala#15967, fixes the regression
in scala#16339, and keeps scala#15967 as well as scala#16123 (which is somewhat
related) fixed.
little-inferno pushed a commit to little-inferno/dotty that referenced this issue Jan 25, 2023
Not doing so, in a context where GADT inferrence is enabled, such as in
TypeOps.refineUsingParent, leads to false inferrences.

Doing so, and removing the previous fix for scala#15967, fixes the regression
in scala#16339, and keeps scala#15967 as well as scala#16123 (which is somewhat
related) fixed.
@Kordyjan Kordyjan added this to the 3.3.0 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:pattern-matching itype:bug regression This worked in a previous version but doesn't anymore
Projects
None yet
Development

Successfully merging a pull request may close this issue.

5 participants