scala3
scala3 copied to clipboard
Freeze GADTs more when comparing type member infos
Thanks for the fix!
Although this does fix the issues, I think that freezing the GADT constraints when RHS is not an alias cannot cover all unsoundness problems here--since the root cause of the unsoundness is that tp1.member here could upcast LHS implicitly. For example, we could make a slightly different example:
enum SUB[-A, +B]:
case Refl[C]() extends SUB[C, C]
trait Foo { type A }
def foo[L, H, X <: Foo { type A >: L <: H }](e: SUB[X, Foo { type A = Int }], i: Int): L = e.match {
case SUB.Refl() => i
}
val e0: SUB[Foo { type A = Int }, Foo { type A = Int }] =
SUB.Refl[Foo { type A = Int }]()
def boom(i: Int): String = foo[Nothing, Any, Foo { type A = Int }](e0, i) : Nothing // cast Int to String!
Comparing X <:< Foo { type A = Int } upcasts the LHS implicitly and results in unsound bounds, although the type member on RHS is a type alias. The safest way may be the one originally implemented in this PR--freezing the type member whenever comparing type member infos, but this seems overly restrictive and breaks existing code. So I think maybe we should merge this fix now before we find out a proper way to check whether tp1.member upcasts tp1 implicitly.
Btw, I think we should keep the tp1IsSingleton check, since this at least prevents the unsound cases brought by upcasting singleton types. The following code, which is modified from the code in #14728, becomes a false positive example in this PR:
enum SUB[-A, +B]:
case Refl[C]() extends SUB[C, C]
trait Foo { type A }
def foo[L, H](x: Foo { type A >: L <: H }, e: SUB[x.type, Foo { type A = Int }], i: Int): L = e.match {
case SUB.Refl() => i
}
val x0 = new Foo { type A = Int }
val e0: SUB[x0.type, Foo { type A = Int }] = SUB.Refl[x0.type]()
def boom(i: Int): String = foo[Nothing, Any](x0, e0, i) : Nothing // cast Int to String!
What is the motivation for these changes?
https://github.com/lampepfl/dotty/issues/15485 is the issue it fixes (in the sidebar)