Refine criterion when to widen types

Refine criterion when to widen types in match type reduction.

We now do not widen if the compared-against type contains
variant named type parameters. This is intended to fix the
soundness problem in #17149.

Fixes #17149
Fixes #15926

Todos:

 - [ ] Check & fix neg test failures
 - [ ] Add more tests
 - [ ] Also consider approximating abstract types to lower bounds.
       This is completely missing so far. There are neither tests
       nor an implementation.
 - [ ] Update the docs on match types to explain what goes on here.

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

@@ -24,6 +24,7 @@ import typer.Applications.productSelectorTypes
 import reporting.trace
 import annotation.constructorOnly
 import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing, boxed, boxedUnlessFun, boxedIfTypeParam, isAlwaysPure}
+import NameKinds.WildcardParamName
 
 /** Provides methods to compare types.
  */
@@ -865,10 +866,28 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         fourthTry
     }
 
+    /** Can we widen an abstract type when comparing with `tp`?
+     *  This is NOT the case if one of the following is true:
+     *    - canWidenAbstract is false,
+     *    - or `tp` contains a non-wildcard type parameter of the matched-against
+     *      case lambda that appears in co- or contra-variant position
+     */
+    def widenAbstractOKFor(tp: Type): Boolean =
+      val acc = new TypeAccumulator[Boolean]:
+        override def apply(x: Boolean, t: Type) =
+          x && t.match
+            case t: TypeParamRef =>
+              variance == 0 || (t.binder ne caseLambda) || t.paramName.is(WildcardParamName)
+            case _ =>
+              foldOver(x, t)
+      canWidenAbstract && acc(true, tp)
+
     def tryBaseType(cls2: Symbol) = {
       val base = nonExprBaseType(tp1, cls2).boxedIfTypeParam(tp1.typeSymbol)
       if base.exists && (base ne tp1)
-        && (!caseLambda.exists || canWidenAbstract || tp1.widen.underlyingClassRef(refinementOK = true).exists)
+          && (!caseLambda.exists
+              || widenAbstractOKFor(tp2)
+              || tp1.widen.underlyingClassRef(refinementOK = true).exists)
       then
         isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
         && recordGadtUsageIf { MatchType.thatReducesUsingGadt(tp1) }
@@ -889,8 +908,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 || narrowGADTBounds(tp1, tp2, approx, isUpper = true))
               && (tp2.isAny || GADTusage(tp1.symbol))
 
-            (!caseLambda.exists || canWidenAbstract)
-                && isSubType(hi1.boxedIfTypeParam(tp1.symbol), tp2, approx.addLow) && (trustBounds || isSubType(lo1, tp2, approx.addLow))
+            (!caseLambda.exists || widenAbstractOKFor(tp2))
+              && isSubType(hi1.boxedIfTypeParam(tp1.symbol), tp2, approx.addLow) && (trustBounds || isSubType(lo1, tp2, approx.addLow))
             || compareGADT
             || tryLiftedToThis1
           case _ =>

compiler/test/dotc/pos-test-pickling.blacklist

@@ -48,6 +48,7 @@ i6505.scala
 i15158.scala
 i15155.scala
 i15827.scala
+i17149.scala
 
 # Opaque type
 i5720.scala

tests/neg/i17149.scala

@@ -0,0 +1,17 @@
+type Ext1[S] = S match {
+  case Seq[t] => t
+}
+type Ext2[S] = S match {
+  case Seq[_] => Int
+}
+type Ext3[S] = S match {
+  case Array[t] => t
+}
+type Ext4[S] = S match {
+  case Array[_] => Int
+}
+def foo[T <: Seq[Any], A <: Array[B], B] =
+  summon[Ext1[T] =:= T]    // error
+  summon[Ext2[T] =:= Int]  // ok
+  summon[Ext3[A] =:= B]    // ok
+  summon[Ext4[A] =:= Int]  // ok

tests/pos/i15926.scala

@@ -0,0 +1,28 @@
+
+@main def main(): Unit =
+  println(summon[Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]] =:= Minus[Succ[Succ[Zero]]]])
+
+sealed trait IntT
+sealed trait NatT extends IntT
+final case class Zero() extends NatT
+final case class Succ[+N <: NatT](n: N) extends NatT
+final case class Minus[+N <: Succ[NatT]](n: N) extends IntT
+
+type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
+  case Zero => X
+  case Succ[y] => NatSum[Succ[X], y]
+
+type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match
+  case Zero => X
+  case Succ[y] => X match
+    case Zero => Minus[Y]
+    case Succ[x] => NatDif[x, y]
+
+type Sum[X <: IntT, Y <: IntT] <: IntT = Y match
+  case Zero => X
+  case Minus[y] => X match
+    case Minus[x] => Minus[NatSum[x, y]]
+    case _ => NatDif[X, y]
+  case _ => X match
+    case Minus[x] => NatDif[Y, x]
+    case _ => NatSum[X, Y]

tests/pos/i17149.scala

@@ -0,0 +1,6 @@
+type Ext[S <: Seq[_]] = S match {
+  case Seq[t] => t
+}
+
+val _ = implicitly[Ext[Seq[Int]] =:= Int] // e.scala: Cannot prove that e.Ext[Seq[Int]] =:= Int
+val _ = summon[Ext[Seq[Int]] =:= Int]