Avoid unsound GADT constraints derived from subtyping relations between singletons and refined types

[Linyxus]

This PR freezes GADT constraints when comparing the type member bounds of singleton types and refined types, since the GADT constraints derived from the comparison can be overly-strong (unsound).

The following code snippet is unsound, but accepted by the compiler.

trait Foo {
  type A >: Nothing <: Any
}

enum SUB[-A, +B]:
  case Refl[X]() extends SUB[X, X]

import SUB._

def test[X](foo: Foo, e: SUB[foo.type, Foo {type A <: X}], x: Any): X = e match
  case Refl() =>
    // Here we try to infer GADT constraints from
    // the subtyping relation foo.type <:< Foo { type A <: X }.
    // This will try to infer constr from [ >: Nothing <: Any ] <:< [ >: Nothing <: X ],
    // which results in the unsound constraint Any <: X.

    // We can set foo = new Foo { type A = Nothing } and X = Nothing,
    // to get the unsound subtyping constraint Any <: Nothing.
    x

val foo = new Foo { type A = Nothing }

def unsound(x: Any): Nothing =
  test[Nothing](foo, Refl(), x)

In the above code snippet, we will try to extract GADT constraint from the subtyping relation foo.type <:< Foo {type A <: X}. When comparing these two types, the type comparer will try to compare the bounds of the type member This: isSubType [ >: Nothing <: Any ] <: [ >: Nothing <: X ], which will give us the constraint Any <: X. However, deriving GADT constraints from this comparison can be unsound, since, by comparing the type member bounds of foo.type and Foo {type A <: X}, what we do is essentially upcasting the singleton type foo.type to Foo and compare Foo#This to (Foo {type A <: X})#This. We can not extract GADT constraints from this since the LHS is upcasted.

Therefore, we may have to freeze GADT constraints under such conditions to avoid deriving unsound constraints.

[abgruszecki]

This LGTM to me. I'll have to discuss with @smarter whether this problem can affect type inference or not.

[abgruszecki]

Ok, we'll be merging this. Thanks, @Linyxus!

We discussed this with Guillaume and this is one of those wonderful puzzlers where TypeComparer does something unsound for GADTs, but OK for type inference.

[dwijnand]

Interesting! How did you come about that test case, @Linyxus? I presume it's a minimisation from something, right?

[Linyxus]

@dwijnand Yes. I was preparing the merge of path-dependent GADT reasoning (#14754) and found that the test i2941 was broken:

trait FooBase {
  type Bar >: Null <: BarBase { type This <: FooBase.this.Bar }
  type This >: this.type <: FooBase { type This <: FooBase.this.This }

  def derived(bar: Bar): This = ???
}

trait BarBase {
  type This >: Null <: BarBase { type This <: BarBase.this.This }
}

object Test {
  def bad(foo: FooBase): FooBase = foo match {
    case foo: FooBase =>
      foo.derived(???)  // Triggers infinite loop in TypeAssigner.avoid()
  }
}

When inspecting the trace I noticed that the GADT solver will derive the constraint foo.This >: FooBase { type This <: foo.This } <: FooBase { type This <: foo.This } (from the subtyping relation foo.type <:< FooBase { type This <: foo.This }), which is wrong. And this is how I found this issue. :D

[LPTK]

We discussed this with Guillaume and this is one of those wonderful puzzlers where TypeComparer does something unsound for GADTs, but OK for type inference.

For those interested, this is the reason.

It's not a surprise that the type comparer does some things wrong for GADTs, because it was apparently written with type inference in mind, not GADT reasoning. I suspect there are many other similar soundness problems hiding in it because of this.

[abgruszecki]

Yes, I'm slowly becoming more and more convinced that with the current approach we will just have endless soundness problems with GADTs. What's surprising is that I (still) cannot find a coherent pattern that would tell me when TypeComparer sets some approximation mode and when it doesn't.