Space: Use RHS of & when refining subtypes

This allows for a more precise type argument to be inferred, which leads
to correct exhaustivity results.

Author: dwijnand

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

@@ -738,7 +738,7 @@ object TypeOps:
    *  If the subtyping is true, the instantiated type `p.child[Vs]` is
    *  returned. Otherwise, `NoType` is returned.
    */
-  def refineUsingParent(parent: Type, child: Symbol)(using Context): Type = {
+  def refineUsingParent(parent: Type, child: Symbol, mixins: List[Type] = Nil)(using Context): Type = {
     // <local child> is a place holder from Scalac, it is hopeless to instantiate it.
     //
     // Quote from scalac (from nsc/symtab/classfile/Pickler.scala):
@@ -753,7 +753,7 @@ object TypeOps:
     val childTp = if (child.isTerm) child.termRef else child.typeRef
 
     inContext(ctx.fresh.setExploreTyperState().setFreshGADTBounds.addMode(Mode.GadtConstraintInference)) {
-      instantiateToSubType(childTp, parent).dealias
+      instantiateToSubType(childTp, parent, mixins).dealias
     }
   }
 
@@ -764,7 +764,7 @@ object TypeOps:
    *
    *  Otherwise, return NoType.
    */
-  private def instantiateToSubType(tp1: NamedType, tp2: Type)(using Context): Type = {
+  private def instantiateToSubType(tp1: NamedType, tp2: Type, mixins: List[Type])(using Context): Type = {
     // In order for a child type S to qualify as a valid subtype of the parent
     // T, we need to test whether it is possible S <: T.
     //
@@ -881,6 +881,7 @@ object TypeOps:
     }
 
     def instantiate(): Type = {
+      for tp <- mixins.reverseIterator do protoTp1 <:< tp
       maximizeType(protoTp1, NoSpan)
       wildApprox(protoTp1)
     }

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -597,11 +597,11 @@ class SpaceEngine(using Context) extends SpaceLogic {
     }
 
   /** Decompose a type into subspaces -- assume the type can be decomposed */
-  def decompose(tp: Type): List[Typ] =
-    tp.dealias match {
+  def decompose(tp: Type): List[Typ] = trace(i"decompose($tp)", debug, show(_: Seq[Space])) {
+    def rec(tp: Type, mixins: List[Type]): List[Typ] = tp.dealias match {
       case AndType(tp1, tp2) =>
         def decomposeComponent(tpA: Type, tpB: Type): List[Typ] =
-          decompose(tpA).flatMap {
+          rec(tpA, tpB :: mixins).flatMap {
             case Typ(tp, _) =>
               if tp <:< tpB then
                 Typ(tp, decomposed = true) :: Nil
@@ -642,7 +642,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
 
         val parts = children.map { sym =>
           val sym1 = if (sym.is(ModuleClass)) sym.sourceModule else sym
-          val refined = TypeOps.refineUsingParent(tp, sym1)
+          val refined = TypeOps.refineUsingParent(tp, sym1, mixins)
 
           debug.println(sym1.show + " refined to " + refined.show)
 
@@ -663,6 +663,8 @@ class SpaceEngine(using Context) extends SpaceLogic {
 
         parts.map(Typ(_, true))
     }
+    rec(tp, Nil)
+  }
 
   /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
   def canDecompose(tp: Type): Boolean =

tests/pos/i16539.min.scala

@@ -0,0 +1,9 @@
+// scalac: -Werror
+sealed trait Tag[A]
+
+sealed trait Foo
+case class Bar[A](fn: A => Unit) extends Foo, Tag[A]
+
+class Test:
+  def pmat[A](sel: Foo & Tag[A]): Unit = sel match
+    case Bar(_) =>

tests/pos/i16539.scala

@@ -0,0 +1,17 @@
+// scalac: -Werror
+sealed trait Tag[A]
+
+enum Hidden:
+  case Reveal[A](
+    init: A,
+    reduce: (A, A) => A
+  ) extends Hidden with Tag[A]
+
+trait Handle[C]:
+  def apply[A](c: C & Tag[A]): A
+
+val x = new Handle[Hidden] {
+  def apply[A](c: Hidden & Tag[A]): A = c match {
+    case Hidden.Reveal(x, _) => x
+  }
+}