fix #10511: compare enumvalues in provably disjoint

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

@@ -2404,14 +2404,20 @@ 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
    *  is either stuck or reduces to the same case.
    */
   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 +2523,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, _) =>

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"),

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)

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

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

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)