Refine criterion when to widen types

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

@@ -64,6 +64,14 @@ trait ConstraintHandling {
    */
   protected var canWidenAbstract: Boolean = true
 
+  /**
+   * Used for match type reduction.
+   * When an abstract type may not be widened, according to `widenAbstractOKFor`,
+   * we record it in this set, so that we can ultimately fail the reduction, but
+   * with all the information that comes out from continuing to widen the abstract type.
+   */
+  protected var poisoned: Set[TypeParamRef] = Set.empty
+
   protected var myNecessaryConstraintsOnly = false
   /** When collecting the constraints needed for a particular subtyping
    *  judgment to be true, we sometimes need to approximate the constraint

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,36 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         fourthTry
     }
 
+    /** Can we widen an abstract type when comparing with `tp`?
+    *   This is the case with the following cases:
+    *    - if `canWidenAbstract` is true.
+     *
+     *  Secondly, if `tp` is a type parameter, we can widen if:
+     *    - if `tp` is not a type parameter of the matched-against case lambda
+     *    - if `tp` is an invariant or wildcard type parameter
+     *    - finally, allow widening, but record the type parameter in `poisoned`,
+     *      so that can be accounted for during the reduction step
+     */
+    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)
+              || { poisoned += t; true }
+            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 +916,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 _ =>
@@ -984,7 +1011,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
             tp1.cases.corresponds(tp2.cases)(isSubType)
           case _ => false
         }
-        recur(tp1.underlying, tp2) || compareMatch
+        (!caseLambda.exists || canWidenAbstract) && recur(tp1.underlying, tp2) || compareMatch
       case tp1: AnnotatedType if tp1.isRefining =>
         isNewSubType(tp1.parent)
       case JavaArrayType(elem1) =>
@@ -3091,6 +3118,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
   }
 
   def matchCases(scrut: Type, cases: List[Type])(using Context): Type = {
+    // a reference for the type parameters poisoned during matching
+    // for use during the reduction step
+    var poisoned: Set[TypeParamRef] = Set.empty
 
     def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
       def apply(insts: Array[Type], t: Type) = t match
@@ -3102,16 +3132,24 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
               case entry: TypeBounds =>
                 val lo = fullLowerBound(param)
                 val hi = fullUpperBound(param)
-                if isSubType(hi, lo) then lo.simplified else Range(lo, hi)
+                if !poisoned(param) && isSubType(hi, lo) then lo.simplified else Range(lo, hi)
               case inst =>
                 assert(inst.exists, i"param = $param\nconstraint = $constraint")
-                inst.simplified
+                if !poisoned(param) then inst.simplified else Range(inst, inst)
           insts
         case _ =>
           foldOver(insts, t)
 
     def instantiateParams(insts: Array[Type]) = new ApproximatingTypeMap {
       variance = 0
+
+      override def range(lo: Type, hi: Type): Type =
+        if variance == 0 && (lo eq hi) then
+          // override the default `lo eq hi` test, which removes the Range
+          // which leads to a Reduced result, instead of NoInstance
+          Range(lower(lo), upper(hi))
+        else super.range(lo, hi)
+
       def apply(t: Type) = t match {
         case t @ TypeParamRef(b, n) if b `eq` caseLambda => insts(n)
         case t: LazyRef => apply(t.ref)
@@ -3133,9 +3171,14 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
 
       def matches(canWidenAbstract: Boolean): Boolean =
         val saved = this.canWidenAbstract
+        val savedPoisoned = this.poisoned
         this.canWidenAbstract = canWidenAbstract
+        this.poisoned = Set.empty
         try necessarySubType(scrut, pat)
-        finally this.canWidenAbstract = saved
+        finally
+          poisoned = this.poisoned
+          this.poisoned = savedPoisoned
+          this.canWidenAbstract = saved
 
       def redux(canApprox: Boolean): MatchResult =
         caseLambda match

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

docs/_docs/reference/new-types/match-types.md

@@ -140,6 +140,8 @@ An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that
 appear covariantly and nonvariantly in `Is` are as small as possible and all
 type variables in `Xs` that appear contravariantly in `Is` are as large as
 possible.  Here, "small" and "large" are understood with respect to  `<:`.
+But, type parameter will not be "large" if a pattern containing it is matched
+against lambda case in co- or contra-variant position.
 
 For simplicity, we have omitted constraint handling so far. The full formulation
 of subtyping tests describes them as a function from a constraint and a pair of

tests/neg/11982.scala

@@ -4,8 +4,8 @@ type Head[X] = X match {
 }
 
 object Unpair {
-  def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1
-  unpair[Tuple2["msg", 42]]: "msg"  // error
+  def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1 // error
+  unpair[Tuple2["msg", 42]]: "msg"
 }
 
 
@@ -14,8 +14,8 @@ type Head2[X] = X match {
 }
 
 object Unpair2 {
-  def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1
-  unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg" // error
+  def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1 // error
+  unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg"
 }
 
 
@@ -35,6 +35,6 @@ type Head4[X] = X match {
 }
 
 object Unpair4 {
-  def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1
-  unpair[Foo["msg", 42]]: "msg" // error
+  def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1 // error
+  unpair[Foo["msg", 42]]: "msg"
 }

tests/neg/i13780.check

@@ -1,3 +1,23 @@
+-- [E007] Type Mismatch Error: tests/neg/i13780.scala:12:32 ------------------------------------------------------------
+12 |  def unpair[X <: Y]: Head[X] = "" // error
+   |                                ^^
+   |                                Found:    ("" : String)
+   |                                Required: Head[X]
+   |
+   |                                where:    X is a type in method unpair with bounds <: A.this.Y
+   |
+   |
+   |                                Note: a match type could not be fully reduced:
+   |
+   |                                  trying to reduce  Head[X]
+   |                                  failed since selector X
+   |                                  does not uniquely determine parameters a, b in
+   |                                    case (a, b) => a
+   |                                  The computed bounds for the parameters are:
+   |                                    a >: Any
+   |                                    b >: Any
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------
 18 |  def int[X <: Y]: Int = unpair[X]  // error
    |                         ^^^^^^^^^

tests/neg/i13780.scala

@@ -9,7 +9,7 @@ trait Z {
 
 class A extends Z {
   type Y <: Tuple2[Any, Any]
-  def unpair[X <: Y]: Head[X] = ""
+  def unpair[X <: Y]: Head[X] = "" // error
   def any[X <: Y]: Any = unpair[X]
 }
 

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.contra.scala

@@ -0,0 +1,7 @@
+trait Show[-A >: Nothing]
+
+type MT1[I <: Show[Nothing], N] = I match
+  case Show[a] => N match
+    case Int => a
+
+val a = summon[MT1[Show[String], Int] =:= String]

tests/pos/i15926.extract.scala

@@ -0,0 +1,24 @@
+// like pos/i15926.scala
+// but with the nested match type extracted
+// which is a workaround that fixed the problem
+sealed trait Nat
+final case class Zero() extends Nat
+final case class Succ[+N <: Nat]() extends Nat
+
+final case class Neg[+N <: Succ[Nat]]()
+
+type Sum[X, Y] = Y match
+  case Zero    => X
+  case Succ[y] => Sum[Succ[X], y]
+
+type IntSum[A, B] = B match
+  case Neg[b] => IntSumNeg[A, b]
+
+type IntSumNeg[A, B] = A match
+  case Neg[a] => Neg[Sum[a, B]]
+
+type One = Succ[Zero]
+type Two = Succ[One]
+
+class Test:
+  def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]]

tests/pos/i15926.min.scala

@@ -0,0 +1,22 @@
+// like pos/i15926.scala
+// but minimised to the subset of paths needed
+// to fail the specific test case
+sealed trait Nat
+final case class Zero() extends Nat
+final case class Succ[+N <: Nat]() extends Nat
+
+final case class Neg[+N <: Succ[Nat]]()
+
+type Sum[X, Y] = Y match
+  case Zero    => X
+  case Succ[y] => Sum[Succ[X], y]
+
+type IntSum[A, B] = B match
+  case Neg[b] => A match
+    case Neg[a] => Neg[Sum[a, b]]
+
+type One = Succ[Zero]
+type Two = Succ[One]
+
+class Test:
+  def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]]

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]