Defer param replacement when inferring GADT constraints

When we're infering the GADT constraints from comparing the type
arguments of pattern type `Foo[C, C]` against the type arguments of
scrutinee type `Foo[X, String]` we end up eagerly instantiating `C` to
`X` and then recording in the GADT constraints that `X =:= String`.

However, later when the SpaceEngine decomposes the scrutinee type
`Foo[X, String]` it discovers `Bar[String]`, but that doesn't match the
pattern type `Bar[X]`, because the GADT constraints are no longer
present.

Not replacing, though, seems to require (pos/gadt-TypeSafeLambda.scala)
not considering the widening of a type parameter to its equal bounds as
an approximation.

Author: dwijnand

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

@@ -252,7 +252,8 @@ trait ConstraintHandling {
       val bound = legalBound(param, rawBound, isUpper)
       val oldBounds @ TypeBounds(lo, hi) = constraint.nonParamBounds(param)
       val equalBounds = (if isUpper then lo else hi) eq bound
-      if equalBounds && !bound.existsPart(_ eq param, StopAt.Static) then
+      val isGadt = ctx.mode.is(Mode.GadtConstraintInference)
+      if equalBounds && !isGadt && !bound.existsPart(_ eq param, StopAt.Static) then
         // The narrowed bounds are equal and not recursive,
         // so we can remove `param` from the constraint.
         constraint = constraint.replace(param, bound)
@@ -267,8 +268,12 @@ trait ConstraintHandling {
           homogenizeArgs = Config.alignArgsInAnd
           try
             trustBounds = false
-            if isUpper then oldBounds.derivedTypeBounds(lo, hi & bound)
-            else oldBounds.derivedTypeBounds(lo | bound, hi)
+            if isUpper then
+              if isGadt && !hi.isAny && hi.isValueTypeOrWildcard && bound.isValueTypeOrWildcard then oldBounds.derivedTypeBounds(lo, AndType(hi, bound))
+              else oldBounds.derivedTypeBounds(lo, hi & bound)
+            else
+              if isGadt && !lo.isNothingType && lo.isValueTypeOrWildcard && bound.isValueTypeOrWildcard then oldBounds.derivedTypeBounds(OrType(lo, bound, soft = true), hi)
+              else oldBounds.derivedTypeBounds(lo | bound, hi)
           finally
             homogenizeArgs = savedHomogenizeArgs
             trustBounds = savedTrustBounds

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

@@ -1201,7 +1201,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       def compareLower(tycon2bounds: TypeBounds, tyconIsTypeRef: Boolean): Boolean =
         if ((tycon2bounds.lo `eq` tycon2bounds.hi) && !tycon2bounds.isInstanceOf[MatchAlias])
           if (tyconIsTypeRef) recur(tp1, tp2.superTypeNormalized)
-          else isSubApproxHi(tp1, tycon2bounds.lo.applyIfParameterized(args2))
+          else recur(tp1, tycon2bounds.lo.applyIfParameterized(args2))
         else
           fallback(tycon2bounds.lo)
 

tests/pos/i15289.scala

@@ -0,0 +1,31 @@
+// scalac: -Werror
+sealed abstract class Foo[A, B]
+final case class Bar[C](baz: C) extends Foo[C, C]
+
+class Test:
+  def m1[X](f1: Foo[X, String]): String = f1 match { case Bar(_) => "" } // ""
+  def m2[X](f2: Foo[X, String]): X      = f2 match { case Bar(x) => x  } // x: X
+  def m3[X](f3: Foo[X, String]): String = f3 match { case Bar(x) => x  } // x.asInstanceOf[x.type & String]: String
+  def m4[X](f4: Foo[X, String]): X      = f4 match { case Bar(_) => "" } // "".asInstanceOf[("" & String & X) @uncheckedStable]
+
+// ptc: Bar[C] aka Foo[C, C] vs Foo[X, String]
+// ptc:  C >: X       ~>  cstr: C >: X
+// ptc:  C <: X       ~>  cstr: C := X
+// C instantiated with X, so now C shows up as X
+// ptc:  X >: String  ~>  gadt: X >: String
+// ptc:  X <: String  ~>  gadt: X := String
+// ptc: Bar[X]
+// max: Bar[X]
+
+// what's more correct?
+// * unapp arg tpe = Bar[X]       gadt: X =:= String
+// * unapp arg tpe = Bar[String]  gadt: X =:= String
+
+// after fix:
+// ptc: Bar[C] aka Foo[C, C] vs Foo[X, String]
+// ptc:  C >: X       ~>  cstr: C >:  X
+// ptc:  C <: X       ~>  cstr: C =:= X
+// ptc:  C >: String  ~>  cstr: C >: X | String <: X           gadt: X >:  String
+// ptc:  C <: String  ~>  cstr: C >: X | String <: X & String  gadt: X =:= String
+// ptc: Bar[C]
+// max: Bar[String]