From 4d4296e74a84281619b0b70b3e834b0878bce38b Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Fri, 4 Oct 2019 18:38:07 +0200 Subject: [PATCH 1/5] Simplify MT reduction algorithm By removing the widenAbstractTypes step, which is subsumed by the provably empty test. --- .../dotty/tools/dotc/core/TypeComparer.scala | 30 ---------- tests/neg/6314-6.scala | 57 +++++++++++++++++++ tests/neg/6314.scala | 50 ---------------- 3 files changed, 57 insertions(+), 80 deletions(-) create mode 100644 tests/neg/6314-6.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 4c85c684d144..aae819880ee2 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2757,34 +2757,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 +2771,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. diff --git a/tests/neg/6314-6.scala b/tests/neg/6314-6.scala new file mode 100644 index 000000000000..6c400ab46d97 --- /dev/null +++ b/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 +} diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala index 03e3d22a26c0..beee41c48e9a 100644 --- a/tests/neg/6314.scala +++ b/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 - } -} From 51c4f85289adde76b2820a36ebc88ca53fab4e99 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Mon, 7 Oct 2019 16:37:42 +0200 Subject: [PATCH 2/5] Use .superType instead of .underlying Underlying breaks kinds (the underlying of an AppliedType is a HKTypeLambda). The edited test case was making use of that bug to implement an impossible match type. Indeed, that test is trying to distinguish f[Dummy] (for some f) and Int But there is no way to tell that these two types are disjoint. In fact they are not, since `type F[X] = Any` matches the `f[Dummy]` pattern and overlaps with `Int`. --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 6 +++--- tests/run-macros/tasty-simplified.check | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index aae819880ee2..abe3810fb0ab 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2508,11 +2508,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling !(tp2 <:< tp1) && (provablyDisjoint(tp1, tp2.tp2) || provablyDisjoint(tp1, tp2.tp1)) case (tp1: TypeProxy, tp2: TypeProxy) => - provablyDisjoint(tp1.underlying, tp2) || provablyDisjoint(tp1, tp2.underlying) + provablyDisjoint(tp1.superType, tp2) || provablyDisjoint(tp1, tp2.superType) case (tp1: TypeProxy, _) => - provablyDisjoint(tp1.underlying, tp2) + provablyDisjoint(tp1.superType, tp2) case (_, tp2: TypeProxy) => - provablyDisjoint(tp1, tp2.underlying) + provablyDisjoint(tp1, tp2.superType) case _ => false } diff --git a/tests/run-macros/tasty-simplified.check b/tests/run-macros/tasty-simplified.check index ae73a625ac58..55e725e10f17 100644 --- a/tests/run-macros/tasty-simplified.check +++ b/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]]] From ece0c3362b555ba46814be1476cc2e9275396d93 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Wed, 9 Oct 2019 10:39:08 +0200 Subject: [PATCH 3/5] Fix #6687: handle gadtBounds in MT reduction --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 5 ++++- compiler/test/dotc/pos-test-pickling.blacklist | 1 + tests/pos/6687.scala | 11 +++++++++++ 3 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 tests/pos/6687.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index abe3810fb0ab..9be73bf75dd3 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/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,6 +2506,10 @@ 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.superType, tp2) || provablyDisjoint(tp1, tp2.superType) case (tp1: TypeProxy, _) => diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist index 5c6a4a1876f7..05f7cda9154d 100644 --- a/compiler/test/dotc/pos-test-pickling.blacklist +++ b/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 diff --git a/tests/pos/6687.scala b/tests/pos/6687.scala new file mode 100644 index 000000000000..0a5aeaf35c19 --- /dev/null +++ b/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 +} From 03b2d428319b33ea0930166ef7820e467e64239b Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Wed, 9 Dec 2020 19:08:37 +0100 Subject: [PATCH 4/5] Fix #10510: Add regression test --- tests/pos/10510.scala | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/pos/10510.scala diff --git a/tests/pos/10510.scala b/tests/pos/10510.scala new file mode 100644 index 000000000000..8ce44c290586 --- /dev/null +++ b/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 +} From 54fe387d5771c33ed5b6aafeb4cd1492aa50d52f Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Tue, 15 Dec 2020 09:44:51 +0100 Subject: [PATCH 5/5] Keep the unsound behavior under a -Y flag --- community-build/community-projects/shapeless | 2 +- .../src/dotty/tools/dotc/config/ScalaSettings.scala | 1 + compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 10 +++++++--- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/community-build/community-projects/shapeless b/community-build/community-projects/shapeless index 98a211b44ef4..9a9b53f8d388 160000 --- a/community-build/community-projects/shapeless +++ b/community-build/community-projects/shapeless @@ -1 +1 @@ -Subproject commit 98a211b44ef412673a68189d66f50b1b04806b10 +Subproject commit 9a9b53f8d388028b2d2922d1fca951cad68e5516 diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala index 14a1ad51c81e..9976e0a8cc36 100644 --- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala +++ b/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.") diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 9be73bf75dd3..dd8843e05638 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2511,16 +2511,20 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling 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.superType, tp2) || provablyDisjoint(tp1, tp2.superType) + provablyDisjoint(matchTypeSuperType(tp1), tp2) || provablyDisjoint(tp1, matchTypeSuperType(tp2)) case (tp1: TypeProxy, _) => - provablyDisjoint(tp1.superType, tp2) + provablyDisjoint(matchTypeSuperType(tp1), tp2) case (_, tp2: TypeProxy) => - provablyDisjoint(tp1, tp2.superType) + 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)