scala3 icon indicating copy to clipboard operation
scala3 copied to clipboard

Freeze GADTs more when comparing type member infos

Open dwijnand opened this issue 3 years ago • 2 comments

dwijnand avatar Aug 16 '22 16:08 dwijnand

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.

Linyxus avatar Aug 30 '22 12:08 Linyxus

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!

Linyxus avatar Aug 30 '22 12:08 Linyxus

What is the motivation for these changes?

odersky avatar Sep 29 '22 12:09 odersky

https://github.com/lampepfl/dotty/issues/15485 is the issue it fixes (in the sidebar)

dwijnand avatar Sep 29 '22 14:09 dwijnand