Fix #14726: call exclusiveLower before addLess during unification

compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala

@@ -352,6 +352,9 @@ trait ConstraintHandling {
     val pKept    = if level1 <= level2 then p1 else p2
     val pRemoved = if level1 <= level2 then p2 else p1
 
+    val down = constraint.exclusiveLower(p2, p1)
+    val up = constraint.exclusiveUpper(p1, p2)
+
     constraint = constraint.addLess(p2, p1, direction = if pKept eq p1 then KeepParam2 else KeepParam1)
 
     val boundKept    = constraint.nonParamBounds(pKept).substParam(pRemoved, pKept)
@@ -371,9 +374,6 @@ trait ConstraintHandling {
       if !isSub(lo, hi) then
         boundRemoved = TypeBounds(lo & hi, hi)
 
-    val down = constraint.exclusiveLower(p2, p1)
-    val up = constraint.exclusiveUpper(p1, p2)
-
     val newBounds = (boundKept & boundRemoved).bounds
     constraint = constraint.updateEntry(pKept, newBounds).replace(pRemoved, pKept)
 

tests/pos/i14726-upper.scala

@@ -0,0 +1,21 @@
+def test0[A >: Int] = {
+  def test1[X, B >: X <: X] = {
+    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 Int <: (A <: B <:) X for X.
+            val t0: X = 0
+          case _ =>
+        }
+      case _ =>
+    }
+  }
+}

tests/pos/i14726.scala

@@ -0,0 +1,21 @@
+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   // should work too
+          val t2: Int = t0 : A  // works
+        case _ =>
+      }
+    case _ =>
+  }
+}