Fix match type reduction with avoided types #18043
Conversation
The "infoStr" I felt caused more noise and confusion, so I remove it. I also pushed the type mismatch message done 1 line, so it displays better multi-line (the "Found" and "Required" are alined).
TypeComparer's compareAtoms assumes it has an answer to subtyping if one of the types has atoms and the other doesn't. But an unreduced match alias won't have atoms, so we shouldn't bail early. Co-Authored-By: Matt Bovel <[email protected]>
If the skolem-widened scrutinees are the same and the cases correspond, then the match types are the same. Also, with inlining the type embeded in inlining's Typed expression will be without going through type-avoidance, so they won't be skolems. So we look to widen inline proxy term refs, in addition to skolems. Co-Authored-By: Matt Bovel <[email protected]>
|
I was initially worried about widening term refs and then realized that your are only doing it for inline proxies, so that is probably fine. We could add a test to make sure that term refs in scrutinees are not widened in general: val x: Int = 42
val y: Int = 43
val z: Int = 44
type IsX[T] =
T match
case x.type => true
case _ => false
def test = summon[IsX[y.type] =:= IsX[z.type]] // error
def test2 = summon[
(
y.type match
case x.type => true
case _ => false
) =:= (
z.type match
case x.type => true
case _ => false
)
] // error |
Co-Authored-By: Matt Bovel <[email protected]>
|
I unfortunately found at least one case where widening skolems is not desirable: import scala.util.Random
val x = 42
type IsX[T] =
T match
case x.type => true
case _ => false
def bothXOrNot(a: Int, b: Int)(using IsX[a.type] =:= IsX[b.type]) = ???
def test = bothXOrNot(Random.nextInt(), Random.nextInt())It compiles with your change, while it didn't compile before. Before, it would it would not find an evidence for |
From the Match Type paper, typing rule S-Match5 requires that the LHS scrutinee "Ss" is a subtype of the RHS scrutinee "Ts": Ss <: Ts. It's not required that they are the same type. This covers widening a skolem or inline proxy tp1 scrutinee, without erroneously widening the RHS tp2 scrutinee.
|
Forgot to put in the commit message: I think this code might come from before match types were made invariant. |
There was a problem hiding this comment.
As far as I am concerned, this looks great!
As discussed: allowing match types to be generally "covariant in their scrutinees" would break algorithmic subtyping transitivity, so we probably want to avoid it for now.
However, this PR only adresses a narrower case: skolems and inline proxies. As these cannot be written by users directly in match types patterns, it seems to me that it should pretty safe. I tried to come up with problematic examples but couldn't.
The bug in compareAtoms is also an important one and we should definitely merge its fix as soon as possible.
|
It fails under |
No description provided.