Remove empty capabilities for separation checking

Author: odersky

compiler/src/dotty/tools/dotc/cc/CCState.scala

@@ -81,6 +81,16 @@ class CCState:
   def start(): Unit =
     iterCount = 1
 
+  private var mySepCheck = false
+
+  /** Are we currently running separation checks? */
+  def isSepCheck = mySepCheck
+
+  def inSepCheck(op: => Unit): Unit =
+    val saved = mySepCheck
+    mySepCheck = true
+    try op finally mySepCheck = saved
+
   // ------ Global counters -----------------------
 
   /** Next CaptureSet.Var id */

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -83,6 +83,14 @@ sealed abstract class CaptureSet extends Showable:
    */
   def owner: Symbol
 
+  /** If this set is a variable: Drop capabilities that are known to be empty
+   *  This is called during separation checking so that capabilities that turn
+   *  out to be always empty because of conflicting clasisifiers don't contribute
+   *  to peaks. We can't do it before that since classifiers are set during
+   *  capture checking.
+   */
+  def dropEmpties()(using Context): this.type
+
   /** Is this capture set definitely non-empty? */
   final def isNotEmpty: Boolean = !elems.isEmpty
 
@@ -412,9 +420,15 @@ sealed abstract class CaptureSet extends Showable:
     res
 
   def transClassifiers(using Context): Classifiers =
-    if isConst then
+    def elemClassifiers =
       (ClassifiedAs(Nil) /: elems.map(_.transClassifiers))(joinClassifiers)
-    else UnknownClassifier
+    if ccState.isSepCheck then
+      dropEmpties()
+      elemClassifiers
+    else if isConst then
+      elemClassifiers
+    else
+      UnknownClassifier
 
   def tryClassifyAs(cls: ClassSymbol)(using Context): Boolean =
     elems.forall(_.tryClassifyAs(cls))
@@ -574,6 +588,8 @@ object CaptureSet:
 
     def owner = NoSymbol
 
+    def dropEmpties()(using Context) = this
+
     private var isComplete = true
 
     def setMutable()(using Context): Unit =
@@ -658,6 +674,16 @@ object CaptureSet:
 
     def isMaybeSet = false // overridden in BiMapped
 
+    private var emptiesDropped = false
+
+    def dropEmpties()(using Context): this.type =
+      if !emptiesDropped then
+        emptiesDropped = true
+        for elem <- elems do
+          if elem.isKnownEmpty then
+            elems -= empty
+      this
+
     /** A handler to be invoked if the root reference `cap` is added to this set */
     var rootAddedHandler: () => Context ?=> Unit = () => ()
 

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -2021,7 +2021,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       end checker
 
       checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
-      if ccConfig.useSepChecks then SepCheck(this).traverse(unit)
+      if ccConfig.useSepChecks then
+        ccState.inSepCheck:
+          SepCheck(this).traverse(unit)
       if !ctx.reporter.errorsReported then
         // We dont report errors here if previous errors were reported, because other
         // errors often result in bad applied types, but flagging these bad types gives

compiler/src/dotty/tools/dotc/cc/SepCheck.scala

@@ -185,7 +185,7 @@ object SepCheck:
         case newElem :: newElems1 =>
           if seen.contains(newElem) then
             recur(seen, acc, newElems1)
-          else newElem.stripReadOnly match
+          else newElem.stripRestricted.stripReadOnly match
             case elem: FreshCap =>
               if elem.hiddenSet.deps.isEmpty then recur(seen + newElem, acc + newElem, newElems1)
               else
@@ -197,7 +197,7 @@ object SepCheck:
               if newElem.isTerminalCapability
                 //|| newElem.isInstanceOf[TypeRef | TypeParamRef]
               then recur(seen + newElem, acc, newElems1)
-              else recur(seen + newElem, acc, newElem.captureSetOfInfo.elems.toList ++ newElems1)
+              else recur(seen + newElem, acc, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1)
         case Nil => acc
       recur(emptyRefs, emptyRefs, refs.toList)