GADT upper bounds are not properly propagated during unification

[Linyxus]

Compiler version

3.1.2-RC2

Minimized code

Under certain conditions involving parameter unification, the GADT bounds will not get fully propagated.
In the following example, we have three type parameters X, A and B, with bound A: >: X <: X and B: <: Int.
In the snippet, we first add the ordering B <: A, then the ordering A <: B.
When we add the ordering A <: B, the upper bound <: Int should be propagated to X, since we have X <: A <: B <: Int.
However, that is not the case. The bound is not propagated in the GADT solver, and we have to explicitly cast X to A to make use of the bound X <: Int.

def test[X, A >: X <: X, B <: Int] = {
  enum Expr[+T]:
    case TagA() extends Expr[A]
    case TagB() extends Expr[B]

  import Expr._

  def foo(e1: Expr[A], e2: Expr[B]) = e1 match {
    case TagB() => // add GADT constr: B <: A
      e2 match {
        case TagA() =>
          // add GADT constr: A <: B
          //   should propagate bound X (<: A <: B) <: Int for X.
          val t0: X = ???
          val t1: Int = t0   // error
          val t2: Int = t0 : A  // cast explicitly, works
        case _ =>
      }
    case _ =>
  }
}

The problem happens during the unification of type parameters. When adding the constraint A <: B, the constraint handler checks that B <: A already holds, and it will unify A into B.
Ideally, the handler should propagate the upper bound of B (<: Int) to the parameters known to be the subtype of A (X in our case). To do this, the handler will first query all parameters less than A (except for those already known to be less than B, to avoid propgating bounds repeatedly) with the exclusiveLower function, then propagate the upper bounds of B to these parameters.

The problem is that, in the current implementation, we call exclusiveLower(A, B) after we call addLess(A, B). addLess(A, B) will order all lower parameters to be lower than B, which means that the result of exclusiveLower(A, B) will be List(B) instead of List(X, B).

To fix the problem we could call exclusiveLower before we call addLess.

Output

[info] running (fork) dotty.tools.dotc.Main -classpath /Users/linyxus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.8/scala-library-2.13.8.jar:/Users/linyxus/Workspace/dotty/library/../out/bootstrap/scala3-library-bootstrapped/scala-3.1.3-RC1-bin-SNAPSHOT-nonbootstrapped/scala3-library_3-3.1.3-RC1-bin-SNAPSHOT.jar -color:never issues/gadt-unify.scala
-- [E007] Type Mismatch Error: issues/gadt-unify.scala:15:24 --------------------------------------------------------------------------------------------------------------------------------------------------------
15 |          val t1: Int = t0   // error
   |                        ^^
   |                        Found:    (t0 : X)
   |                        Required: Int
   |
   |                        where:    X is a type in method test which is an alias of B
   |
   | longer explanation available when compiling with `-explain`
1 error found
[error] Nonzero exit code returned from runner: 1
[error] (scala3-compiler / Compile / runMain) Nonzero exit code returned from runner: 1
[error] Total time: 2 s, completed Mar 21, 2022, 4:56:21 PM

Expectation

The 15th line should also work, without casting explicitly.