Fix regression in provablyDisjoint (cherry-picked from #12786)

Author: OlivierBlanvillain

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

@@ -2494,7 +2494,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
     def isEnumValueOrModule(ref: TermRef): Boolean =
       val sym = ref.termSymbol
-      sym.isAllOf(EnumCase, butNot=JavaDefined) || sym.is(Module)
+      val isEnumValue = sym.isAllOf(EnumCase, butNot=JavaDefined)
+      val isModule = sym.is(Module)
+      isEnumValue || isModule || (ref.info match {
+        case tp: TermRef => isEnumValueOrModule(tp)
+        case _ => false
+      })
 
     /** Can we enumerate all instantiations of this type? */
     def isClosedSum(tp: Symbol): Boolean =
@@ -2603,11 +2608,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, tp2: TypeRef) if isEnumValueOrModule(tp1) && tp2.symbol.isClass =>
+        !isSubType(tp1, tp2)
+      case (tp1: TypeRef, tp2: TermRef) if isEnumValueOrModule(tp2) && tp1.symbol.isClass =>
+        !isSubType(tp2, tp1)
       case (tp1: Type, tp2: Type) if defn.isTupleType(tp1) =>
         provablyDisjoint(tp1.toNestedPairs, tp2)
       case (tp1: Type, tp2: Type) if defn.isTupleType(tp2) =>

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
+
+  ()
+}