Freeze GADTs more when comparing type member infos

[dwijnand]

No description provided.

[Linyxus]

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]

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!

[dwijnand]

@odersky this is what I found works. Can you think of another way to identify when we have a member that required widening tp1 to a non-class info and thus we can't safely infer gadt constraints?

[odersky]

I can't make sense of this condition and don't understand the logic behind this. This would at least need a fat comment explaining the issue and the attempted solution.

[odersky]

What is the motivation for these changes?

[dwijnand]

#15485 is the issue it fixes (in the sidebar)

[odersky]

I can't make sense of this condition and don't understand the logic behind this. This would at least need a fat comment explaining the issue and the attempted solution.