From 3202767850d6561cde162795f8214729a5654e2f Mon Sep 17 00:00:00 2001 From: Jamie Thompson Date: Mon, 28 Dec 2020 11:17:26 +0000 Subject: [PATCH 1/5] fix #10511: compare enumvalues in provably disjoint --- .../dotty/tools/dotc/core/TypeComparer.scala | 7 +++++ tests/neg/i10511.scala | 18 +++++++++++ tests/pos/i10511.scala | 16 ++++++++++ tests/run/i10511.scala | 31 +++++++++++++++++++ 4 files changed, 72 insertions(+) create mode 100644 tests/neg/i10511.scala create mode 100644 tests/pos/i10511.scala create mode 100644 tests/run/i10511.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 7bb942e9ab6a..4447cbecab7f 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2412,6 +2412,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling */ def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean = { // println(s"provablyDisjoint(${tp1.show}, ${tp2.show})") + + def isEnumValueOrModule(ref: TermRef): Boolean = + val sym = ref.termSymbol + sym.isAllOf(EnumCase, butNot=JavaDefined) || sym.is(Module) + /** Can we enumerate all instantiations of this type? */ def isClosedSum(tp: Symbol): Boolean = tp.is(Sealed) && tp.isOneOf(AbstractOrTrait) && !tp.hasAnonymousChild @@ -2517,6 +2522,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling 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: TermRef, tp2: TermRef) if isEnumValueOrModule(tp1) && isEnumValueOrModule(tp2) => + tp1.termSymbol != tp2.termSymbol case (tp1: TypeProxy, tp2: TypeProxy) => provablyDisjoint(matchTypeSuperType(tp1), tp2) || provablyDisjoint(tp1, matchTypeSuperType(tp2)) case (tp1: TypeProxy, _) => diff --git a/tests/neg/i10511.scala b/tests/neg/i10511.scala new file mode 100644 index 000000000000..4ceaae4141e4 --- /dev/null +++ b/tests/neg/i10511.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 +} + +def not[B <: Bool & Singleton](b: B): Not[B] = b match { + case b: False.type => True // error + case b: True.type => False // error +} + +val f: Not[False.type] = False // error: Found: (Bool.False : Bool) Required: (Bool.True : Bool) diff --git a/tests/pos/i10511.scala b/tests/pos/i10511.scala new file mode 100644 index 000000000000..e9fddaff186b --- /dev/null +++ b/tests/pos/i10511.scala @@ -0,0 +1,16 @@ +enum Bool { + case True + case False +} + +import Bool._ + +type Not[B <: Bool] = B match { + case True.type => False.type + case False.type => True.type +} + +val t: True.type = True +val f: False.type = False + +val g: Not[False.type] = t diff --git a/tests/run/i10511.scala b/tests/run/i10511.scala new file mode 100644 index 000000000000..f1548ea7482a --- /dev/null +++ b/tests/run/i10511.scala @@ -0,0 +1,31 @@ +enum Bool { + case True + case False + + // just to make sure we are using reference equality + override def equals(a: Any) = false + +} + +import Bool._ + +type Not[B <: Bool] = B match { + case True.type => False.type + case False.type => True.type +} + +def not[B <: Bool & Singleton](b: B): Not[B] = b match { + case b: True.type => False + case b: False.type => True +} + +@main def Test = + + val t: True.type = True + val f: False.type = False + + val t1: Not[False.type] = t + val f1: Not[True.type] = f + + assert(not(True).asInstanceOf[AnyRef] eq False) + assert(not(False).asInstanceOf[AnyRef] eq True) From fa919f528be0f6e981d101f4a11fe74b8b609fef Mon Sep 17 00:00:00 2001 From: Jamie Thompson Date: Mon, 28 Dec 2020 14:42:48 +0000 Subject: [PATCH 2/5] add transitivity test --- .../dotty/tools/dotc/CompilationTests.scala | 1 + tests/pos-special/i10511-transitivity.scala | 20 +++++++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 tests/pos-special/i10511-transitivity.scala diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala index 742469bdcf22..96ee3f89848a 100644 --- a/compiler/test/dotty/tools/dotc/CompilationTests.scala +++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala @@ -52,6 +52,7 @@ class CompilationTests { compileFile("tests/pos-special/notNull.scala", defaultOptions.and("-Yexplicit-nulls")), compileDir("tests/pos-special/adhoc-extension", defaultOptions.and("-source", "3.1", "-feature", "-Xfatal-warnings")), compileFile("tests/pos-special/i7575.scala", defaultOptions.andLanguageFeature("dynamics")), + compileFile("tests/pos-special/i10511-transitivity.scala", defaultOptions), // avoid pickling test compileFile("tests/pos-special/kind-projector.scala", defaultOptions.and("-Ykind-projector")), compileFile("tests/run/i5606.scala", defaultOptions.and("-Yretain-trees")), compileFile("tests/pos-custom-args/i5498-postfixOps.scala", defaultOptions withoutLanguageFeature "postfixOps"), diff --git a/tests/pos-special/i10511-transitivity.scala b/tests/pos-special/i10511-transitivity.scala new file mode 100644 index 000000000000..87ad2226afee --- /dev/null +++ b/tests/pos-special/i10511-transitivity.scala @@ -0,0 +1,20 @@ +enum Bool { + case True + case False +} + +import Bool._ + +type Not[B <: Bool] = B match { + case True.type => False.type + case False.type => True.type +} + +val t: True.type = True +val f: False.type = False + +val t1: Not[f.type] = t // transitivity +val f1: Not[t.type] = f // transitivity + +val t2: Not[f1.type] = t1 // transitivity x2 +val f2: Not[t1.type] = f1 // transitivity x2 From 7377ee3a9e212bdc4995411e629eb7701ac41ee7 Mon Sep 17 00:00:00 2001 From: Jamie Thompson Date: Tue, 29 Dec 2020 11:31:01 +0000 Subject: [PATCH 3/5] update comment --- compiler/src/dotty/tools/dotc/core/TypeComparer.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 4447cbecab7f..ac0305deac42 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2404,7 +2404,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling * 1. Single inheritance of classes * 2. Final classes cannot be extended * 3. ConstantTypes with distinct values are non intersecting - * 4. There is no value of type Nothing + * 4. TermRefs with distinct values are non intersecting + * 5. There is no value of type Nothing * * Note on soundness: the correctness of match types relies on on the * property that in all possible contexts, the same match type expression From 8b5f2dafa97a30686a2d8c047a332350d3ac603e Mon Sep 17 00:00:00 2001 From: Jamie Thompson Date: Wed, 30 Dec 2020 10:46:22 +0000 Subject: [PATCH 4/5] address feedback --- .../dotty/tools/dotc/CompilationTests.scala | 1 - docs/docs/reference/new-types/match-types.md | 4 ++-- tests/pos-special/i10511-transitivity.scala | 20 ------------------- tests/pos/i10511.scala | 6 ++++++ 4 files changed, 8 insertions(+), 23 deletions(-) delete mode 100644 tests/pos-special/i10511-transitivity.scala diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala index 96ee3f89848a..742469bdcf22 100644 --- a/compiler/test/dotty/tools/dotc/CompilationTests.scala +++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala @@ -52,7 +52,6 @@ class CompilationTests { compileFile("tests/pos-special/notNull.scala", defaultOptions.and("-Yexplicit-nulls")), compileDir("tests/pos-special/adhoc-extension", defaultOptions.and("-source", "3.1", "-feature", "-Xfatal-warnings")), compileFile("tests/pos-special/i7575.scala", defaultOptions.andLanguageFeature("dynamics")), - compileFile("tests/pos-special/i10511-transitivity.scala", defaultOptions), // avoid pickling test compileFile("tests/pos-special/kind-projector.scala", defaultOptions.and("-Ykind-projector")), compileFile("tests/run/i5606.scala", defaultOptions.and("-Yretain-trees")), compileFile("tests/pos-custom-args/i5498-postfixOps.scala", defaultOptions withoutLanguageFeature "postfixOps"), diff --git a/docs/docs/reference/new-types/match-types.md b/docs/docs/reference/new-types/match-types.md index 72ee3f87384c..b849b9b7e237 100644 --- a/docs/docs/reference/new-types/match-types.md +++ b/docs/docs/reference/new-types/match-types.md @@ -48,7 +48,7 @@ Recursive match type definitions can also be given an upper bound, like this: ```scala type Concat[Xs <: Tuple, +Ys <: Tuple] <: Tuple = Xs match - case Unit => Ys + case EmptyTuple => Ys case x *: xs => x *: Concat[xs, Ys] ``` @@ -126,6 +126,7 @@ Disjointness proofs rely on the following properties of Scala types: 1. Single inheritance of classes 2. Final classes cannot be extended 3. Constant types with distinct values are nonintersecting +4. Singleton paths to distinct values are nonintersecting, such as `object` definitions or singleton enum cases. Type parameters in patterns are minimally instantiated when computing `S <: Pi`. An instantiation `Is` is _minimal_ for `Xs` if all type variables in `Xs` that @@ -240,4 +241,3 @@ main differences here are: whereas match types also work for type parameters and abstract types. - Match types support direct recursion. - Conditional types distribute through union types. - diff --git a/tests/pos-special/i10511-transitivity.scala b/tests/pos-special/i10511-transitivity.scala deleted file mode 100644 index 87ad2226afee..000000000000 --- a/tests/pos-special/i10511-transitivity.scala +++ /dev/null @@ -1,20 +0,0 @@ -enum Bool { - case True - case False -} - -import Bool._ - -type Not[B <: Bool] = B match { - case True.type => False.type - case False.type => True.type -} - -val t: True.type = True -val f: False.type = False - -val t1: Not[f.type] = t // transitivity -val f1: Not[t.type] = f // transitivity - -val t2: Not[f1.type] = t1 // transitivity x2 -val f2: Not[t1.type] = f1 // transitivity x2 diff --git a/tests/pos/i10511.scala b/tests/pos/i10511.scala index e9fddaff186b..386899d047a7 100644 --- a/tests/pos/i10511.scala +++ b/tests/pos/i10511.scala @@ -14,3 +14,9 @@ val t: True.type = True val f: False.type = False val g: Not[False.type] = t + +val t1: Not[f.type] = t // transitivity +val f1: Not[t.type] = f // transitivity + +val t2: Not[f1.type] = t1 // transitivity x2 +val f2: Not[t1.type] = f1 // transitivity x2 From b0aeefc327eddf361b3aeb2d1298feca0bd8d174 Mon Sep 17 00:00:00 2001 From: Jamie Thompson Date: Wed, 30 Dec 2020 13:25:47 +0000 Subject: [PATCH 5/5] do not run FromTasty on i10511 --- compiler/test/dotc/pos-from-tasty.blacklist | 3 +++ 1 file changed, 3 insertions(+) diff --git a/compiler/test/dotc/pos-from-tasty.blacklist b/compiler/test/dotc/pos-from-tasty.blacklist index 51fb4980f30c..b0ea2e35caec 100644 --- a/compiler/test/dotc/pos-from-tasty.blacklist +++ b/compiler/test/dotc/pos-from-tasty.blacklist @@ -8,3 +8,6 @@ t802.scala # missing position rbtree.scala + +# transitive reduction of match types +i10511.scala