Merge pull request #13031 from Linyxus/fix-param-unification

Fix ordering propagation during parameter unification in constraint solver

Author: abgruszecki

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

@@ -197,6 +197,7 @@ trait ConstraintHandling {
   private def unify(p1: TypeParamRef, p2: TypeParamRef)(using Context): Boolean = {
     constr.println(s"unifying $p1 $p2")
     assert(constraint.isLess(p1, p2))
+    constraint = constraint.addLess(p2, p1)
     val down = constraint.exclusiveLower(p2, p1)
     val up = constraint.exclusiveUpper(p1, p2)
     constraint = constraint.unify(p1, p2)

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

@@ -355,8 +355,27 @@ class OrderingConstraint(private val boundsMap: ParamBounds,
     else {
       assert(contains(param1), i"$param1")
       assert(contains(param2), i"$param2")
-      val newUpper = param2 :: exclusiveUpper(param2, param1)
-      val newLower = param1 :: exclusiveLower(param1, param2)
+      // Is `order` called during parameter unification?
+      val unifying = isLess(param2, param1)
+      val newUpper = {
+        val up = exclusiveUpper(param2, param1)
+        if unifying then
+          // Since param2 <:< param1 already holds now, filter out param1 to avoid adding
+          //   duplicated orderings.
+          param2 :: up.filterNot(_ eq param1)
+        else
+          param2 :: up
+      }
+      val newLower = {
+        val lower = exclusiveLower(param1, param2)
+        if unifying then
+          // Do not add bounds for param1 since it will be unified to param2 soon.
+          // And, similarly filter out param2 from lowerly-ordered parameters
+          //   to avoid duplicated orderings.
+          lower.filterNot(_ eq param2)
+        else
+          param1 :: lower
+      }
       val current1 = newLower.foldLeft(current)(upperLens.map(this, _, _, newUpper ::: _))
       val current2 = newUpper.foldLeft(current1)(lowerLens.map(this, _, _, newLower ::: _))
       current2

tests/pos/gadt-param-unification.scala

@@ -0,0 +1,6 @@
+trait Expr[T]
+final class Lit[T] extends Expr[T]
+
+def foo[X, T1 >: X, T2](m: Expr[T2]): T2 = m match {
+  case _: Lit[T1] => ??? : X
+}