Fix #6687: handle gadt bounds in match type reduction

compiler/src/dotty/tools/dotc/config/ScalaSettings.scala

@@ -200,6 +200,7 @@ class ScalaSettings extends Settings.SettingGroup with CommonScalaSettings {
   val YerasedTerms: Setting[Boolean] = BooleanSetting("-Yerased-terms", "Allows the use of erased terms.")
   val YcheckInit: Setting[Boolean] = BooleanSetting("-Ycheck-init", "Check initialization of objects")
   val YrequireTargetName: Setting[Boolean] = BooleanSetting("-Yrequire-targetName", "Warn if an operator is defined without a @targetName annotation")
+  val YunsoundMatchTypes: Setting[Boolean] = BooleanSetting("-Yunsound-match-types", "Use unsound match type reduction algorithm.")
 
   /** Area-specific debug output */
   val YexplainLowlevel: Setting[Boolean] = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")

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

@@ -2388,7 +2388,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case _ => false
     }
 
-
   /** Are `tp1` and `tp2` provablyDisjoint types?
    *
    *  `true` implies that we found a proof; uncertainty defaults to `false`.
@@ -2507,17 +2506,25 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case (_, tp2: AndType) =>
         !(tp2 <:< tp1)
         && (provablyDisjoint(tp1, tp2.tp2) || provablyDisjoint(tp1, tp2.tp1))
+      case (tp1: NamedType, _) if gadtBounds(tp1.symbol) != null =>
+        provablyDisjoint(gadtBounds(tp1.symbol).hi, tp2) || provablyDisjoint(tp1.superType, tp2)
+      case (_, tp2: NamedType) if gadtBounds(tp2.symbol) != null =>
+        provablyDisjoint(tp1, gadtBounds(tp2.symbol).hi) || provablyDisjoint(tp1, tp2.superType)
       case (tp1: TypeProxy, tp2: TypeProxy) =>
-        provablyDisjoint(tp1.underlying, tp2) || provablyDisjoint(tp1, tp2.underlying)
+        provablyDisjoint(matchTypeSuperType(tp1), tp2) || provablyDisjoint(tp1, matchTypeSuperType(tp2))
       case (tp1: TypeProxy, _) =>
-        provablyDisjoint(tp1.underlying, tp2)
+        provablyDisjoint(matchTypeSuperType(tp1), tp2)
       case (_, tp2: TypeProxy) =>
-        provablyDisjoint(tp1, tp2.underlying)
+        provablyDisjoint(tp1, matchTypeSuperType(tp2))
       case _ =>
         false
     }
   }
 
+  /** Restores the buggy match type reduction under -Yunsound-match-types. */
+  private def matchTypeSuperType(tp: TypeProxy): Type =
+    if ctx.settings.YunsoundMatchTypes.value then tp.underlying else tp.superType
+
   protected def explainingTypeComparer = ExplainingTypeComparer(comparerContext)
   protected def trackingTypeComparer = TrackingTypeComparer(comparerContext)
 
@@ -2757,34 +2764,6 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
         case _ =>
           cas
       }
-      def widenAbstractTypes(tp: Type): Type = new TypeMap {
-        var seen = Set[TypeParamRef]()
-        def apply(tp: Type) = tp match {
-          case tp: TypeRef =>
-            tp.info match {
-              case info: MatchAlias =>
-                mapOver(tp)
-                  // TODO: We should follow the alias in this case, but doing so
-                  // risks infinite recursion
-              case TypeBounds(lo, hi) =>
-                if (hi frozen_<:< lo) {
-                  val alias = apply(lo)
-                  if (alias ne lo) alias else mapOver(tp)
-                }
-                else WildcardType
-              case _ =>
-                mapOver(tp)
-            }
-          case tp: TypeLambda =>
-            val saved = seen
-            seen ++= tp.paramRefs
-            try mapOver(tp)
-            finally seen = saved
-          case tp: TypeVar if !tp.isInstantiated => WildcardType
-          case tp: TypeParamRef if !seen.contains(tp) => WildcardType
-          case _ => mapOver(tp)
-        }
-      }.apply(tp)
 
       val defn.MatchCase(pat, body) = cas1
 
@@ -2799,8 +2778,6 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
               body
           }
         }
-      else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat)))
-        Some(NoType)
       else if (provablyDisjoint(scrut, pat))
         // We found a proof that `scrut` and `pat` are incompatible.
         // The search continues.

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

@@ -30,6 +30,7 @@ i7087.scala
 i7868.scala
 i7872.scala
 6709.scala
+6687.scala
 
 # Opaque type
 i5720.scala

tests/neg/6314-6.scala

@@ -0,0 +1,57 @@
+final class X
+final class Y
+
+object Test3 {
+  type Bar[A] = A match {
+    case X => String
+    case Y => Int
+  }
+
+  trait XX {
+    type Foo
+
+    val a: Bar[X & Foo] = "hello"
+    val b: Bar[Y & Foo] = 1
+
+    def apply(fa: Bar[X & Foo]): Bar[Y & Foo]
+
+    def boom: Int = apply(a)
+  }
+
+  trait YY extends XX {
+    type Foo = X & Y
+
+    def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error
+        // overriding method apply in trait XX of type (fa: String): Int;
+        //   method apply of type (fa: String): String has incompatible type
+  }
+  (new YY {}).boom
+}
+
+object Test4 {
+  type Bar[A] = A match {
+    case X => String
+    case Y => Int
+  }
+
+  trait XX {
+    type Foo
+    type FooAlias = Foo
+
+    val a: Bar[X & FooAlias] = "hello"
+    val b: Bar[Y & FooAlias] = 1
+
+    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias]
+
+    def boom: Int = apply(a)
+  }
+
+  trait YY extends XX {
+    type Foo = X & Y
+
+    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error
+        // overriding method apply in trait XX of type (fa: String): Int;
+        //   method apply of type (fa: String): String has incompatible type
+  }
+  (new YY {}).boom
+}

tests/neg/6314.scala

@@ -46,53 +46,3 @@ object Test2 {
     def right(fa: Bar[L]): Int = fa // error
   }
 }
-
-
-object Test3 {
-  type Bar[A] = A match {
-    case X => String
-    case Y => Int
-  }
-
-  trait XX {
-    type Foo
-
-    val a: Bar[X & Foo] = "hello"
-    val b: Bar[Y & Foo] = 1 // error
-
-    def apply(fa: Bar[X & Foo]): Bar[Y & Foo]
-
-    def boom: Int = apply(a) // error
-  }
-
-  trait YY extends XX {
-    type Foo = X & Y
-
-    def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa
-  }
-}
-
-object Test4 {
-  type Bar[A] = A match {
-    case X => String
-    case Y => Int
-  }
-
-  trait XX {
-    type Foo
-    type FooAlias = Foo
-
-    val a: Bar[X & FooAlias] = "hello"
-    val b: Bar[Y & FooAlias] = 1 // error
-
-    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias]
-
-    def boom: Int = apply(a) // error
-  }
-
-  trait YY extends XX {
-    type Foo = X & Y
-
-    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa
-  }
-}

tests/pos/10510.scala

@@ -0,0 +1,17 @@
+sealed trait Bool
+case object True extends Bool
+case object False extends Bool
+
+sealed trait SBool[B <: Bool]
+case object STrue extends SBool[True.type]
+case object SFalse extends SBool[False.type]
+
+type Not[B <: Bool] <: Bool = B match {
+  case True.type => False.type
+  case False.type => True.type
+}
+
+def not[B <: Bool](b: SBool[B]): SBool[Not[B]] = b match {
+  case STrue => SFalse
+  case SFalse => STrue
+}

tests/pos/6687.scala

@@ -0,0 +1,11 @@
+type T[X] = X match {
+  case String => Int
+  case Int => String
+}
+
+class Box[X](x: X)
+
+def f[X](x: Box[X]): T[X] = x match {
+  case x: Box[Int]    => ""
+  case x: Box[String] => 1
+}

tests/run-macros/tasty-simplified.check

@@ -1,4 +1,4 @@
-Functor[[A >: scala.Nothing <: scala.Any] => scala.collection.immutable.List[A]]
+Functor[Const[scala.collection.immutable.List[Dummy]]]
 Functor[Const[scala.Int]]
-Functor[Id]
-Functor[[A >: scala.Nothing <: scala.Any] => scala.Option[A]]
+Functor[Const[Dummy]]
+Functor[Const[scala.Option[Dummy]]]