Bugfix: Refine canWidenAbstract criterion

When reducing match types, we did not permit to widen an abstract type scrutinee together with
a non-unique type parameter instantiation. But this criterion need not apply if the
widening is in a constraint satisfiabilty check. For instance

    T <: Tuple
    X <: A *: T

    X match
      case x *: (xs <: Tuple) => ...

Here the match does not succeed since X needs to be widened to A *: T and the x parameter
cannot be uniquely instantiated. On the other hand

    A *: T match
      case x *: (xs <: Tuple) => ...

should pass since there is no widening of the scrutinee. But there is a test T <: Tuple to check
whether T can match xs. That second check should not fall under the canWidenAbstract criterion.

Note: I was not able to make a test (without the fix) fail without capture checking, maybe
because the syntax (xs <: Tuple) is actually not allowed. But it is generated after Typer.

Author: odersky

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

@@ -58,6 +58,12 @@ trait ConstraintHandling {
    */
   protected var comparedTypeLambdas: Set[TypeLambda] = Set.empty
 
+  /** Used for match type reduction: If false, we don't recognize an abstract type
+   *  to be a subtype type of any of its base classes. This is in place only at the
+   *  toplevel; it is turned on again when we add parts of the scrutinee to the constraint.
+   */
+  protected var canWidenAbstract: Boolean = true
+
   protected var myNecessaryConstraintsOnly = false
   /** When collecting the constraints needed for a particular subtyping
    *  judgment to be true, we sometimes need to approximate the constraint
@@ -839,13 +845,17 @@ trait ConstraintHandling {
     //checkPropagated(s"adding $description")(true) // DEBUG in case following fails
     checkPropagated(s"added $description") {
       addConstraintInvocations += 1
+      val saved = canWidenAbstract
+      canWidenAbstract = true
       try bound match
         case bound: TypeParamRef if constraint contains bound =>
           addParamBound(bound)
         case _ =>
           val pbound = avoidLambdaParams(bound)
           kindCompatible(param, pbound) && addBoundTransitively(param, pbound, !fromBelow)
-      finally addConstraintInvocations -= 1
+      finally
+        canWidenAbstract = saved
+        addConstraintInvocations -= 1
     }
   end addConstraint
 

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

@@ -60,8 +60,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   /** Indicates whether the subtype check used GADT bounds */
   private var GADTused: Boolean = false
 
-  protected var canWidenAbstract: Boolean = true
-
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
 

tests/pos-custom-args/captures/matchtypes.scala

@@ -0,0 +1,10 @@
+type HEAD[X <: NonEmptyTuple] = X match {
+  case x *: (_ <: NonEmptyTuple) => x
+}
+
+inline def head[A <: NonEmptyTuple](x: A): HEAD[A] = null.asInstanceOf[HEAD[A]]
+
+def show[A, T <: Tuple](x: A *: T) =
+  show1(head(x))
+  show1(x.head)
+def show1[A](x: A): String = ???