Make atoms computation talk about empty sets correctly

Previously we merged the atoms info of a type with an empty atoms set and a type with
no atoms, since we identified the empty set with "does not have atoms". But that
cannot type the inequality

   0 & 1 <: 0

The new scheme distinguishes the two states by using an Option[Set[Type]] in the
computations.

Author: odersky

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

@@ -440,18 +440,20 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
           (tp1.widenSingletons ne tp1) &&
           recur(tp1.widenSingletons, tp2)
 
-        if (tp2.atoms().nonEmpty && canCompare(tp2.atoms()))
-          val atoms1 = tp1.atoms(widenOK = true)
-          atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms())
-        else
-          widenOK
-          || joinOK
-          || recur(tp11, tp2) && recur(tp12, tp2)
-          || containsAnd(tp1) && recur(tp1.join, tp2)
-              // An & on the left side loses information. Compensate by also trying the join.
-              // This is less ad-hoc than it looks since we produce joins in type inference,
-              // and then need to check that they are indeed supertypes of the original types
-              // under -Ycheck. Test case is i7965.scala.
+        tp2.atoms() match
+          case Some(ts2) if canCompare(ts2) =>
+            tp1.atoms(widenOK = true) match
+              case Some(ts1) => ts1.subsetOf(ts2)
+              case none => false
+          case _ =>
+            widenOK
+            || joinOK
+            || recur(tp11, tp2) && recur(tp12, tp2)
+            || containsAnd(tp1) && recur(tp1.join, tp2)
+                // An & on the left side loses information. Compensate by also trying the join.
+                // This is less ad-hoc than it looks since we produce joins in type inference,
+                // and then need to check that they are indeed supertypes of the original types
+                // under -Ycheck. Test case is i7965.scala.
 
       case tp1: MatchType =>
         val reduced = tp1.reduced
@@ -613,9 +615,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         }
         compareTypeLambda
       case OrType(tp21, tp22) =>
-        if (tp2.atoms().nonEmpty && canCompare(tp2.atoms()))
-          val atoms1 = tp1.atoms(widenOK = true)
-          return atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms()) || isSubType(tp1, NothingType)
+        tp2.atoms() match
+          case Some(ts2) if canCompare(ts2) =>
+            val atomsFit = tp1.atoms(widenOK = true) match
+              case Some(ts1) => ts1.subsetOf(ts2)
+              case none => false
+            return atomsFit || isSubType(tp1, NothingType)
+          case none =>
 
         // The next clause handles a situation like the one encountered in i2745.scala.
         // We have:
@@ -1783,15 +1789,15 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || tp1.isRef(NothingClass) then tp2
     else
       def mergedLub(tp1: Type, tp2: Type): Type = {
-        val atoms1 = tp1.atoms(widenOK = true)
-        if (atoms1.nonEmpty && !widenInUnions) {
-          val atoms2 = tp2.atoms(widenOK = true)
-          if (atoms2.nonEmpty) {
-            if (atoms1.subsetOf(atoms2)) return tp2
-            if (atoms2.subsetOf(atoms1)) return tp1
-            if ((atoms1 & atoms2).isEmpty) return orType(tp1, tp2)
-          }
-        }
+        tp1.atoms(widenOK = true) match
+          case Some(ts1) if !widenInUnions =>
+            tp2.atoms(widenOK = true) match
+              case Some(ts2) =>
+                if ts1.subsetOf(ts2) then return tp2
+                if ts2.subsetOf(ts1) then return tp1
+                if (ts1 & ts2).isEmpty then return orType(tp1, tp2)
+              case none =>
+          case none =>
         val t1 = mergeIfSuper(tp1, tp2, canConstrain)
         if (t1.exists) return t1
 

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

@@ -1173,7 +1173,8 @@ object Types {
      *  @param widenOK  If type proxies that are upperbounded by types with atoms
      *                  have the same atoms.
      */
-    def atoms(widenOK: Boolean = false)(implicit ctx: Context): Set[Type] = dealias match {
+    def atoms(widenOK: Boolean = false)(implicit ctx: Context): Option[Set[Type]] =
+      dealias match
       case tp: SingletonType =>
         def normalize(tp: Type): Type = tp match {
           case tp: SingletonType =>
@@ -1187,16 +1188,17 @@ object Types {
             }
           case _ => tp
         }
-        val underlyingAtoms = tp.underlying.atoms(widenOK)
-        if underlyingAtoms.isEmpty && tp.isStable then Set.empty + normalize(tp)
-        else if underlyingAtoms.size == 1 || widenOK then underlyingAtoms
-        else Set.empty
+        tp.underlying.atoms(widenOK) match
+          case None if tp.isStable => Some(Set.empty + normalize(tp))
+          case s @ Some(ts) if ts.size == 1 || widenOK => s
+          case _ => None
       case tp: ExprType => tp.resType.atoms(widenOK)
       case tp: OrType => tp.atoms(widenOK) // `atoms` overridden in OrType
-      case tp: AndType => tp.tp1.atoms(widenOK) & tp.tp2.atoms(widenOK)
+      case tp: AndType =>
+        for ts1 <- tp.tp1.atoms(widenOK); ts2 <- tp.tp2.atoms(widenOK)
+        yield ts1 & ts2
       case tp: TypeProxy if widenOK => tp.underlying.atoms(widenOK)
-      case _ => Set.empty
-    }
+      case _ => None
 
     private def dealias1(keep: AnnotatedType => Context => Boolean)(implicit ctx: Context): Type = this match {
       case tp: TypeRef =>
@@ -2920,28 +2922,26 @@ object Types {
     }
 
     private var atomsRunId: RunId = NoRunId
-    private var myAtoms: Set[Type] = _
-    private var myWidenedAtoms: Set[Type] = _
+    private var myAtoms: Option[Set[Type]] = _
+    private var myWidenedAtoms: Option[Set[Type]] = _
     private var myWidened: Type = _
 
     private def ensureAtomsComputed()(implicit ctx: Context): Unit =
-      if (atomsRunId != ctx.runId) {
-        val atoms1 = tp1.atoms()
-        val atoms2 = tp2.atoms()
-        myAtoms = if (atoms1.nonEmpty && atoms2.nonEmpty) atoms1 | atoms2 else Set.empty
-        val widenedAtoms1 = tp1.atoms(widenOK = true)
-        val widenedAtoms2 = tp2.atoms(widenOK = true)
-        myWidenedAtoms = if (widenedAtoms1.nonEmpty && widenedAtoms2.nonEmpty) widenedAtoms1 | widenedAtoms2 else Set.empty
+      if atomsRunId != ctx.runId then
+        myAtoms =
+          for ts1 <- tp1.atoms(); ts2 <- tp2.atoms()
+          yield ts1 | ts2
+        myWidenedAtoms =
+          for ts1 <- tp1.atoms(widenOK = true); ts2 <- tp2.atoms(widenOK = true)
+          yield ts1 | ts2
         val tp1w = tp1.widenSingletons
         val tp2w = tp2.widenSingletons
         myWidened = if ((tp1 eq tp1w) && (tp2 eq tp2w)) this else tp1w | tp2w
         atomsRunId = ctx.runId
-      }
 
-    override def atoms(widenOK: Boolean)(implicit ctx: Context): Set[Type] = {
+    override def atoms(widenOK: Boolean)(implicit ctx: Context): Option[Set[Type]] =
       ensureAtomsComputed()
       if widenOK then myAtoms else myWidenedAtoms
-    }
 
     override def widenSingletons(implicit ctx: Context): Type = {
       ensureAtomsComputed()

tests/pos/i8128.scala

@@ -1,5 +1,5 @@
 object Test {
-  def id: (x: 1 | 0) => x.type = ???
+  def id: (x: 1 | 0) => x.type = ??? // x => x does not work yet
   id(0): 0   // ok
 
   def id2: Function1[1 | 0, 1 | 0] {
@@ -11,4 +11,9 @@ object Test {
     def apply(x: 1 | 0): x.type
   } = ???
   id3(0): 0  // ok
+
+  var x: 0 = 0
+  var y: (1 & 0) | 0 = 0
+  x = y
+  y = x
 }