From bda342d797348c1309a4cc8b1e97b6f17618246d Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Fri, 11 Jun 2021 11:18:42 +0200 Subject: [PATCH 1/5] Fix regression in provablyDisjoint --- .../dotty/tools/dotc/core/TypeComparer.scala | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 38fd65cb4c54..a6a6aeb5d21a 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2497,9 +2497,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean = trace(i"provable disjoint $tp1, $tp2", matchTypes) { // println(s"provablyDisjoint(${tp1.show}, ${tp2.show})") - def isEnumValueOrModule(ref: TermRef): Boolean = + def isEnumValue(ref: TermRef): Boolean = val sym = ref.termSymbol - sym.isAllOf(EnumCase, butNot=JavaDefined) || sym.is(Module) + sym.isAllOf(EnumCase, butNot=JavaDefined) + + def isEnumValueOrModule(ref: TermRef): Boolean = + isEnumValue(ref) || ref.termSymbol.is(Module) || (ref.info match { + case tp: TermRef => isEnumValueOrModule(tp) + case _ => false + }) /** Can we enumerate all instantiations of this type? */ def isClosedSum(tp: Symbol): Boolean = @@ -2608,11 +2614,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling provablyDisjoint(tp1, gadtBounds(tp2.symbol).hi) || provablyDisjoint(tp1, tp2.superType) case (tp1: TermRef, tp2: TermRef) if isEnumValueOrModule(tp1) && isEnumValueOrModule(tp2) => tp1.termSymbol != tp2.termSymbol - case (tp1: TermRef, tp2: TypeRef) if isEnumValueOrModule(tp1) && !tp1.classSymbols.exists(_.derivesFrom(tp2.classSymbol)) => - // Note: enum values may have multiple parents - true - case (tp1: TypeRef, tp2: TermRef) if isEnumValueOrModule(tp2) && !tp2.classSymbols.exists(_.derivesFrom(tp1.classSymbol)) => - true + case (tp1: TermRef, _) if isEnumValue(tp1) => + false + case (_, tp2: TermRef) if isEnumValue(tp2) => + false case (tp1: Type, tp2: Type) if defn.isTupleType(tp1) => provablyDisjoint(tp1.toNestedPairs, tp2) case (tp1: Type, tp2: Type) if defn.isTupleType(tp2) => From d52b3656e4caca7591d5e5223caf9055bc57780f Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Fri, 11 Jun 2021 11:32:03 +0200 Subject: [PATCH 2/5] Add test case --- tests/neg/12549.scala | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/neg/12549.scala diff --git a/tests/neg/12549.scala b/tests/neg/12549.scala new file mode 100644 index 000000000000..4e2a5531efa0 --- /dev/null +++ b/tests/neg/12549.scala @@ -0,0 +1,18 @@ +enum Bool { + case True + case False +} + +import Bool.* + +type Not[B <: Bool] = B match { + case True.type => False.type + case False.type => True.type + case _ => "unreachable" +} + +def foo[B <: Bool & Singleton]: Unit = { + implicitly[Not[B] =:= "unreachable"] // error + + () +} From 395cebe6c4660675ec10870ef9a3a98b85af543c Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Wed, 28 Jul 2021 15:37:15 +0200 Subject: [PATCH 3/5] Move fullyInstantiated to outer scope --- .../dotty/tools/dotc/core/TypeComparer.scala | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index a6a6aeb5d21a..efec6bca9462 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2518,6 +2518,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling 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 && { + t match { + case tp: TypeRef if tp.symbol.isAbstractOrParamType => false + case _: SkolemType | _: TypeVar => false + case _ => foldOver(x, t) + } + } + }.apply(true, tp) + (tp1.dealias, tp2.dealias) match { case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol == defn.SingletonClass || tp2.symbol == defn.SingletonClass => false @@ -2563,21 +2574,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // doesn't have type tags, meaning that users cannot write patterns // that do type tests on higher kinded types. def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = - covariantDisjoint(tp1, tp2, tparam) || !isSameType(tp1, tp2) && { - // We can only trust a "no" from `isSameType` when both - // `tp1` and `tp2` are fully instantiated. - def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] { - override def apply(x: Boolean, t: Type) = - x && { - t match { - case tp: TypeRef if tp.symbol.isAbstractOrParamType => false - case _: SkolemType | _: TypeVar => false - case _ => foldOver(x, t) - } - } - }.apply(true, tp) - fullyInstantiated(tp1) && fullyInstantiated(tp2) - } + covariantDisjoint(tp1, tp2, tparam) || + !isSameType(tp1, tp2) && + fullyInstantiated(tp1) && // We can only trust a "no" from `isSameType` when + fullyInstantiated(tp2) // both `tp1` and `tp2` are fully instantiated. args1.lazyZip(args2).lazyZip(tycon1.typeParams).exists { (arg1, arg2, tparam) => From ab1d64d27041ce11832f056b60755f2c7c809265 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Fri, 30 Jul 2021 11:33:19 +0200 Subject: [PATCH 4/5] Restore TermRef test when tp2 is fully instantiated --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index efec6bca9462..46b9a485e053 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2614,10 +2614,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling provablyDisjoint(tp1, gadtBounds(tp2.symbol).hi) || provablyDisjoint(tp1, tp2.superType) case (tp1: TermRef, tp2: TermRef) if isEnumValueOrModule(tp1) && isEnumValueOrModule(tp2) => tp1.termSymbol != tp2.termSymbol - case (tp1: TermRef, _) if isEnumValue(tp1) => - false - case (_, tp2: TermRef) if isEnumValue(tp2) => - false + case (tp1: TermRef, tp2: TypeRef) if isEnumValue(tp1) => + fullyInstantiated(tp2) && !tp1.classSymbols.exists(_.derivesFrom(tp2.symbol)) + case (tp1: TypeRef, tp2: TermRef) if isEnumValue(tp2) => + fullyInstantiated(tp1) && !tp2.classSymbols.exists(_.derivesFrom(tp1.symbol)) case (tp1: Type, tp2: Type) if defn.isTupleType(tp1) => provablyDisjoint(tp1.toNestedPairs, tp2) case (tp1: Type, tp2: Type) if defn.isTupleType(tp2) => From 4d6d72d4ecbe3e7d8ecb8edc6d5b8c4d3d23ae0e Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Fri, 30 Jul 2021 17:59:57 +0200 Subject: [PATCH 5/5] Give on disjointness when seeing a Singleton type on either side --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 46b9a485e053..eee0e802528c 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2530,7 +2530,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling }.apply(true, tp) (tp1.dealias, tp2.dealias) match { - case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol == defn.SingletonClass || tp2.symbol == defn.SingletonClass => + case (tp1: TypeRef, _) if tp1.symbol == defn.SingletonClass => + false + case (_, tp2: TypeRef) if tp2.symbol == defn.SingletonClass => false case (tp1: ConstantType, tp2: ConstantType) => tp1 != tp2