From 57912fff7034b56da4f50702456907984c6a4941 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Tue, 7 Sep 2021 14:32:18 +0200 Subject: [PATCH 1/5] Fix #13455: Also consider sealed classes closed sums --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 2 +- tests/pos/13455.scala | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 tests/pos/13455.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 45d02ca9538e..11caf581b2bd 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2528,7 +2528,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling /** Can we enumerate all instantiations of this type? */ def isClosedSum(tp: Symbol): Boolean = - tp.is(Sealed) && tp.isOneOf(AbstractOrTrait) && !tp.hasAnonymousChild + tp.is(Sealed) && !tp.hasAnonymousChild /** Splits a closed type into a disjunction of smaller types. * It should hold that `tp` and `decompose(tp).reduce(_ or _)` diff --git a/tests/pos/13455.scala b/tests/pos/13455.scala new file mode 100644 index 000000000000..62e0dae9c881 --- /dev/null +++ b/tests/pos/13455.scala @@ -0,0 +1,10 @@ +sealed class R + +type X[T] = T match { + case R => String + case (z => r) => Int +} +def x[T]: X[T] = ??? + +def i(i0: Int): Unit = ??? +val a = i(x[Int => String]) From 7d4f46eb1668a00f95fcb50e4f23051bd13902d7 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Tue, 7 Sep 2021 15:28:02 +0200 Subject: [PATCH 2/5] Update check files The warnings on master are incorrect: we know that no instance of SealedClass match the corresponding cases. --- tests/patmat/andtype-opentype-interaction.check | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/patmat/andtype-opentype-interaction.check b/tests/patmat/andtype-opentype-interaction.check index a9d8618adad0..b8f9fbc10ac9 100644 --- a/tests/patmat/andtype-opentype-interaction.check +++ b/tests/patmat/andtype-opentype-interaction.check @@ -1,5 +1,5 @@ -23: Pattern Match Exhaustivity: _: Trait & OpenTrait, _: Clazz & OpenTrait, _: AbstractClass & OpenTrait, _: SealedClass & OpenTrait -27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2 +23: Pattern Match Exhaustivity: _: Trait & OpenTrait, _: Clazz & OpenTrait, _: AbstractClass & OpenTrait +27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2 31: Pattern Match Exhaustivity: _: Trait & OpenClass 35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass 43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass From ac6a8f484a29c43fdc43ce2b67adeed9f136635f Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 23 Sep 2021 11:49:55 +0200 Subject: [PATCH 3/5] Refactor decomposition logic This commit renames isClosedSum to isDecomposable, and moves that function and the decompose function to where they are used locally. The logic in question only makes sense at the precise point where it's used (see the added comment), so having those two functions defined locally helps to avoid confusion. --- .../dotty/tools/dotc/core/TypeComparer.scala | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 11caf581b2bd..c460dc358a65 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2526,17 +2526,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case _ => false }) - /** Can we enumerate all instantiations of this type? */ - def isClosedSum(tp: Symbol): Boolean = - tp.is(Sealed) && !tp.hasAnonymousChild - - /** Splits a closed type into a disjunction of smaller types. - * It should hold that `tp` and `decompose(tp).reduce(_ or _)` - * denote the same set of values. - */ - def decompose(sym: Symbol, tp: Type): List[Type] = - sym.children.map(x => refineUsingParent(tp, x)).filter(_.exists) - def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] { override def apply(x: Boolean, t: Type) = x && { @@ -2558,6 +2547,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass => val cls1 = tp1.classSymbol val cls2 = tp2.classSymbol + def isDecomposable(tp: Symbol): Boolean = + tp.is(Sealed) && !tp.hasAnonymousChild + def decompose(sym: Symbol, tp: Type): List[Type] = + sym.children.map(x => refineUsingParent(tp, x)).filter(_.exists) if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) false else @@ -2570,9 +2563,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // subtype, so they must be unrelated by single inheritance // of classes. true - else if (isClosedSum(cls1)) + else if (isDecomposable(cls1)) + // At this point, !cls1.derivesFrom(cls2): we know that `new cls2` + // is disjoint from `tp2`. Therefore, we can safely decompose + // `cls1` using `.children`, even if `cls1` is non abstract. decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2)) - else if (isClosedSum(cls2)) + else if (isDecomposable(cls2)) decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1)) else false From 0cc29a0a81f80de680dd8eca82f84f094660b1c8 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 23 Sep 2021 18:32:10 +0200 Subject: [PATCH 4/5] Fix docs typo Co-authored-by: Dale Wijnand --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index c460dc358a65..aea0a5a57450 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2564,7 +2564,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // of classes. true else if (isDecomposable(cls1)) - // At this point, !cls1.derivesFrom(cls2): we know that `new cls2` + // At this point, !cls1.derivesFrom(cls2): we know that `cls1` // is disjoint from `tp2`. Therefore, we can safely decompose // `cls1` using `.children`, even if `cls1` is non abstract. decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2)) From 9d8c1613284d940b8fbfc67cd49a605595803c18 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Thu, 23 Sep 2021 18:34:42 +0200 Subject: [PATCH 5/5] Clarify what I ment by `new cls1` --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index aea0a5a57450..15130174f0b5 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2564,9 +2564,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // of classes. true else if (isDecomposable(cls1)) - // At this point, !cls1.derivesFrom(cls2): we know that `cls1` - // is disjoint from `tp2`. Therefore, we can safely decompose - // `cls1` using `.children`, even if `cls1` is non abstract. + // At this point, !cls1.derivesFrom(cls2): we know that direct + // instantiations of `cls1` (terms of the form `new cls1`) are not + // of type `tp2`. Therefore, we can safely decompose `cls1` using + // `.children`, even if `cls1` is non abstract. decompose(cls1, tp1).forall(x => provablyDisjoint(x, tp2)) else if (isDecomposable(cls2)) decompose(cls2, tp2).forall(x => provablyDisjoint(x, tp1))