From dd0c9f2216d5bd02b94b16aefe073918fd4190b6 Mon Sep 17 00:00:00 2001
From: Dale Wijnand <dale.wijnand@gmail.com>
Date: Thu, 22 Dec 2022 10:56:52 +0000
Subject: [PATCH] Space: Use RHS of & when refining subtypes

This allows for a more precise type argument to be inferred, which leads
to correct exhaustivity results.
---
 .../src/dotty/tools/dotc/core/TypeOps.scala     |  7 ++++---
 .../tools/dotc/transform/patmat/Space.scala     | 10 ++++++----
 tests/pos/i16539.min.scala                      |  9 +++++++++
 tests/pos/i16539.scala                          | 17 +++++++++++++++++
 4 files changed, 36 insertions(+), 7 deletions(-)
 create mode 100644 tests/pos/i16539.min.scala
 create mode 100644 tests/pos/i16539.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index ffcdcbe9e869..c42c09a875b0 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/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)
     }
diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index c15eb413e083..7bd18b466518 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/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 =
diff --git a/tests/pos/i16539.min.scala b/tests/pos/i16539.min.scala
new file mode 100644
index 000000000000..d02e34461ab6
--- /dev/null
+++ b/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(_) =>
diff --git a/tests/pos/i16539.scala b/tests/pos/i16539.scala
new file mode 100644
index 000000000000..c5cf45b214ef
--- /dev/null
+++ b/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
+  }
+}