Fix existing GADT constraints with introduced pattern-bound symbols

Author: dwijnand

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

@@ -33,6 +33,18 @@ class GadtConstraint private (
     reverseMapping = reverseMapping.updated(tv.origin, sym),
   )
 
+  def replace(param: TypeParamRef, tp: Type)(using Context) =
+    var constr = constraint
+    for
+      poly <- constraint.domainLambdas
+      paramRef <- poly.paramRefs
+    do
+      val entry0 = constr.entry(paramRef)
+      val entry1 = entry0.substParam(param, tp)
+      if entry1 ne entry0 then
+        constr = constr.updateEntry(paramRef, entry1)
+    withConstraint(constr)
+
   /** Is `sym1` ordered to be less than `sym2`? */
   def isLess(sym1: Symbol, sym2: Symbol)(using Context): Boolean =
     constraint.isLess(tvarOrError(sym1).origin, tvarOrError(sym2).origin)
@@ -245,6 +257,9 @@ sealed trait GadtState {
     result
   }
 
+  def replace(param: TypeParamRef, tp: Type)(using Context) =
+    gadt = gadt.replace(param, tp)
+
   /** See [[ConstraintHandling.approximation]] */
   def approximation(sym: Symbol, fromBelow: Boolean, maxLevel: Int = Int.MaxValue)(using Context): Type = {
     approximation(gadt.tvarOrError(sym).origin, fromBelow, maxLevel).match

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

@@ -509,10 +509,15 @@ object Inferencing {
           }
         }
     }
-    val res = patternBindings.toList.map { (boundSym, _) =>
+    val res = patternBindings.toList.map { (boundSym, origin) =>
       // substitute bounds of pattern bound variables to deal with possible F-bounds
       for (wildCard, param) <- patternBindings do
         boundSym.info = boundSym.info.substParam(param, wildCard.typeRef)
+
+      // also substitute in any GADT bounds
+      // e.g. in i22879, replace the `T` in `X <: Iterable[T]` with the pattern bound `T$1`
+      ctx.gadtState.replace(origin, boundSym.typeRef)
+
       boundSym
     }
 

tests/pos/i22879.scala

@@ -0,0 +1,9 @@
+sealed trait E[S]
+final case class I[T, U <: Iterable[T]]() extends E[U]
+class Test {
+  def test[X](a: E[X]): Unit = {
+    a match {
+      case I() => ???
+    }
+  }
+}