Refine FrozenState categorizations

 - In ++, use a FrozenSepState in order not to pollute hidden sets
 - This avoids two spurious separation failures in stdlib

Author: odersky

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

@@ -16,6 +16,7 @@ import config.Feature
 import collection.mutable
 import CCState.*
 import reporting.Message
+import CaptureSet.Frozen
 
 private val Captures: Key[CaptureSet] = Key()
 
@@ -244,7 +245,7 @@ extension (tp: Type)
    *  the two capture sets are combined.
    */
   def capturing(cs: CaptureSet)(using Context): Type =
-    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK)
+    if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, Frozen.All).isOK)
         && !cs.keepAlways
     then tp
     else tp match

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

@@ -134,7 +134,7 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def invalidateCaches() =
     myCaptureSetRunId = NoRunId
 
-  import CaptureSet.{VarState, FrozenSepState}
+  import CaptureSet.{VarState, FrozenAllState}
 
   /**  x subsumes x
    *   x =:= y       ==>  x subsumes y
@@ -150,7 +150,7 @@ trait CaptureRef extends TypeProxy, ValueType:
    *
    *   TODO: Move to CaptureSet
    */
-  final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = FrozenSepState): Boolean =
+  final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = FrozenAllState): Boolean =
 
     def subsumingRefs(x: Type, y: Type): Boolean = x match
       case x: CaptureRef => y match

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

@@ -142,7 +142,7 @@ sealed abstract class CaptureSet extends Showable:
    *  capture set.
    */
   protected final def addNewElem(elem: CaptureRef)(using Context, VarState): CompareResult =
-    if elem.isMaxCapability || summon[VarState].isInstanceOf[FrozenState] then
+    if elem.isMaxCapability || summon[VarState].isInstanceOf[FrozenVarState] then
       addThisElem(elem)
     else
       addThisElem(elem).orElse:
@@ -173,7 +173,7 @@ sealed abstract class CaptureSet extends Showable:
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
    *                 as frozen.
    */
-  def accountsFor(x: CaptureRef)(using ctx: Context, vs: VarState = FrozenSepState): Boolean =
+  def accountsFor(x: CaptureRef)(using ctx: Context, vs: VarState = FrozenAllState): Boolean =
 
     /** Like `refs.exists(p)`, but testing fresh cap instances in refs last */
     def existsElem(refs: SimpleIdentitySet[CaptureRef], p: CaptureRef => Boolean): Boolean =
@@ -191,7 +191,10 @@ sealed abstract class CaptureSet extends Showable:
       existsElem(elems, _.subsumes(x))
       || !x.isMaxCapability
         && !x.derivesFrom(defn.Caps_CapSet)
-        && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+        && x.captureSetOfInfo.subCaptures(this)(using ctx,
+            vs match
+              case vs: FrozenVarState => vs
+              case _ => FrozenVarState()).isOK
 
     comparer match
       case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
@@ -207,7 +210,7 @@ sealed abstract class CaptureSet extends Showable:
    */
   def mightAccountFor(x: CaptureRef)(using Context): Boolean =
     reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
-      elems.exists(_.subsumes(x)(using ctx, FrozenState()))
+      elems.exists(_.subsumes(x)(using ctx, FrozenVarState()))
       || !x.isMaxCapability
         && {
           val elems = x.captureSetOfInfo.elems
@@ -228,8 +231,12 @@ sealed abstract class CaptureSet extends Showable:
    *                  be added when making this test. An attempt to add either
    *                  will result in failure.
    */
-  final def subCaptures(that: CaptureSet, frozen: Boolean)(using Context): CompareResult =
-    subCaptures(that)(using ctx, if frozen then FrozenState() else VarState())
+  final def subCaptures(that: CaptureSet, frozen: Frozen)(using Context): CompareResult =
+    val state = frozen match
+      case Frozen.None => VarState()
+      case Frozen.Vars => FrozenVarState()
+      case Frozen.All => FrozenAllState
+    subCaptures(that)(using ctx, state)
 
   /** The subcapturing test, using a given VarState */
   private def subCaptures(that: CaptureSet)(using Context, VarState): CompareResult =
@@ -246,16 +253,16 @@ sealed abstract class CaptureSet extends Showable:
    *  in a frozen state.
    */
   def =:= (that: CaptureSet)(using Context): Boolean =
-       this.subCaptures(that, frozen = true).isOK
-    && that.subCaptures(this, frozen = true).isOK
+       this.subCaptures(that, Frozen.All).isOK
+    && that.subCaptures(this, Frozen.All).isOK
 
   /** The smallest capture set (via <:<) that is a superset of both
    *  `this` and `that`
    */
   def ++ (that: CaptureSet)(using Context): CaptureSet =
-    if this.subCaptures(that, frozen = true).isOK then
+    if this.subCaptures(that, Frozen.All).isOK then
       if that.isAlwaysEmpty && this.keepAlways then this else that
-    else if that.subCaptures(this, frozen = true).isOK then this
+    else if that.subCaptures(this, Frozen.All).isOK then this
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
     else Union(this, that)
 
@@ -267,8 +274,8 @@ sealed abstract class CaptureSet extends Showable:
   /** The largest capture set (via <:<) that is a subset of both `this` and `that`
    */
   def **(that: CaptureSet)(using Context): CaptureSet =
-    if this.subCaptures(that, frozen = true).isOK then this
-    else if that.subCaptures(this, frozen = true).isOK then that
+    if this.subCaptures(that, Frozen.Vars).isOK then this
+    else if that.subCaptures(this, Frozen.Vars).isOK then that
     else if this.isConst && that.isConst then Const(elemIntersection(this, that))
     else Intersection(this, that)
 
@@ -395,6 +402,12 @@ object CaptureSet:
   type Vars = SimpleIdentitySet[Var]
   type Deps = SimpleIdentitySet[CaptureSet]
 
+  /** An enum indicating a Frozen degree for subCapturing tests */
+  enum Frozen:
+    case None // operations are performed in a regular VarState
+    case Vars // operations are performed in a FrozenVarState
+    case All  // operations are performed in FrozenAllState
+
   @sharable private var varId = 0
 
   /** If set to `true`, capture stack traces that tell us where sets are created */
@@ -538,7 +551,7 @@ object CaptureSet:
       else
         //if id == 34 then assert(!elem.isUniversalRootCapability)
         assert(elem.isTrackableRef, elem)
-        assert(!this.isInstanceOf[HiddenSet] || summon[VarState] == FrozenSepState, summon[VarState])
+        assert(!this.isInstanceOf[HiddenSet] || summon[VarState] == FrozenAllState, summon[VarState])
         elems += elem
         if elem.isRootCapability then
           rootAddedHandler()
@@ -1043,7 +1056,7 @@ object CaptureSet:
     def getElems(v: Var): Option[Refs] = elemsMap.get(v)
 
     /** Record elements, return whether this was allowed.
-     *  By default, recording is allowed but the special state FrozenState
+     *  By default, recording is allowed in regular both not in frozen states.
      *  overrides this.
      */
     def putElems(v: Var, elems: Refs): Boolean = { elemsMap(v) = elems; true }
@@ -1055,14 +1068,14 @@ object CaptureSet:
     def getDeps(v: Var): Option[Deps] = depsMap.get(v)
 
     /** Record dependent sets, return whether this was allowed.
-     *  By default, recording is allowed but the special state FrozenState
+     *  By default, recording is allowed in regular both not in frozen states.
      *  overrides this.
      */
     def putDeps(v: Var, deps: Deps): Boolean = { depsMap(v) = deps; true }
 
     /** Record hidden elements in elemsMap of hidden set `v`,
      *  return whether this was allowed. By default, recording is allowed
-     *  but the special state FrozenSepState overrides this.
+     *  but the special state FrozenAllState overrides this.
      */
     def putHidden(v: HiddenSet, elems: Refs): Boolean = { elemsMap(v) = elems; true }
 
@@ -1080,21 +1093,22 @@ object CaptureSet:
       else false
   end VarState
 
-  /** A special state that does not allow to record elements or dependent sets.
+  /** A class for states that do not allow to record elements or dependent sets.
    *  In effect this means that no new elements or dependent sets can be added
-   *  in this state (since the previous state cannot be recorded in a snapshot)
-   *  On the other hand, this state does allow by default Fresh.Cap to subsume arbitary
-   *  types, which are then recorded in its hidden set.
+   *  in these states (since the previous state cannot be recorded in a snapshot)
+   *  On the other hand, these states do allow by default Fresh.Cap instances to
+   *  subsume arbitary types, which are then recorded in their hidden sets.
    */
-  class FrozenState extends VarState:
+  class FrozenVarState extends VarState:
     override def putElems(v: Var, refs: Refs) = false
     override def putDeps(v: Var, deps: Deps) = false
 
   @sharable
-  /** A frozen state that allows a Fresh.Cap instncce to subsume a
-   *  reference `r` only if `r` is present in the hidden set of the instance.
+  /** A frozen state that allows a Fresh.Cap instancce to subsume a
+   *  reference `r` only if `r` is already present in the hidden set of the instance.
+   *  No new references can be added.
    */
-  object FrozenSepState extends FrozenState:
+  object FrozenAllState extends FrozenVarState:
     override def putHidden(v: HiddenSet, elems: Refs): Boolean = false
 
   @sharable

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

@@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
 import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
 import scala.collection.mutable
-import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
+import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult, Frozen}
 import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
@@ -320,7 +320,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** Assert subcapturing `cs1 <: cs2` (available for debugging, otherwise unused) */
     def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
-      assert(cs1.subCaptures(cs2, frozen = false).isOK, i"$cs1 is not a subset of $cs2")
+      assert(cs1.subCaptures(cs2, Frozen.None).isOK, i"$cs1 is not a subset of $cs2")
 
     /** If `res` is not CompareResult.OK, report an error */
     def checkOK(res: CompareResult, prefix: => String, pos: SrcPos, provenance: => String = "")(using Context): Unit =
@@ -334,15 +334,15 @@ class CheckCaptures extends Recheck, SymTransformer:
     /** Check subcapturing `{elem} <: cs`, report error on failure */
     def checkElem(elem: CaptureRef, cs: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context) =
       checkOK(
-          elem.singletonCaptureSet.subCaptures(cs, frozen = false),
+          elem.singletonCaptureSet.subCaptures(cs, Frozen.None),
           i"$elem cannot be referenced here; it is not",
           pos, provenance)
 
     /** Check subcapturing `cs1 <: cs2`, report error on failure */
     def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos,
         provenance: => String = "", cs1description: String = "")(using Context) =
       checkOK(
-          cs1.subCaptures(cs2, frozen = false),
+          cs1.subCaptures(cs2, Frozen.None),
           if cs1.elems.size == 1 then i"reference ${cs1.elems.toList.head}$cs1description is not"
           else i"references $cs1$cs1description are not all",
           pos, provenance)
@@ -1390,7 +1390,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val cs = actual.captureSet
           if covariant then cs ++ leaked
           else
-            if !leaked.subCaptures(cs, frozen = false).isOK then
+            if !leaked.subCaptures(cs, Frozen.None).isOK then
               report.error(
                 em"""$expected cannot be box-converted to ${actual.capturing(leaked)}
                     |since the additional capture set $leaked resulted from box conversion is not allowed in $actual""", pos)
@@ -1713,7 +1713,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                     val widened = ref.captureSetOfInfo
                     val added = widened.filter(isAllowed(_))
                     capt.println(i"heal $ref in $cs by widening to $added")
-                    if !added.subCaptures(cs, frozen = false).isOK then
+                    if !added.subCaptures(cs, Frozen.None).isOK then
                       val location = if meth.exists then i" of ${meth.showLocated}" else ""
                       val paramInfo =
                         if ref.paramName.info.kind.isInstanceOf[UniqueNameKind]

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

@@ -2889,10 +2889,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     end inverse
   end MapExistentials
 
+  protected def frozenDegree(frozen: Boolean) =
+    if frozen then CaptureSet.Frozen.Vars else CaptureSet.Frozen.None
+
   protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
     try
       if assocExistentials.isEmpty then
-        refs1.subCaptures(refs2, frozen)
+        refs1.subCaptures(refs2, frozenDegree(frozen))
       else
         val mapped = refs1.map(MapExistentials(assocExistentials))
         if mapped.elems.exists(Existential.isBadExistential)
@@ -2903,15 +2906,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       throw ex
 
   protected def subCapturesMapped(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
-    refs1.subCaptures(refs2, frozen)
+    refs1.subCaptures(refs2, frozenDegree(frozen))
 
   /** Is the boxing status of tp1 and tp2 the same, or alternatively, is
    *  the capture sets `refs1` of `tp1` a subcapture of the empty set?
    *  In the latter case, boxing status does not matter.
    */
   protected def sameBoxed(tp1: Type, tp2: Type, refs1: CaptureSet)(using Context): Boolean =
     (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
-    || refs1.subCaptures(CaptureSet.empty, frozenConstraint).isOK
+    || refs1.subCaptures(CaptureSet.empty, frozenDegree(frozenConstraint)).isOK
 
   // ----------- Diagnostics --------------------------------------------------
 

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

@@ -19,7 +19,7 @@ import typer.Inferencing.*
 import typer.IfBottom
 import reporting.TestingReporter
 import cc.{CapturingType, derivedCapturingType, CaptureSet, captureSet, isBoxed, isBoxedCapturing}
-import CaptureSet.{CompareResult, IdempotentCaptRefMap, IdentityCaptRefMap}
+import CaptureSet.{CompareResult, IdempotentCaptRefMap, IdentityCaptRefMap, Frozen}
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
@@ -161,7 +161,7 @@ object TypeOps:
         TypeComparer.lub(simplify(l, theMap), simplify(r, theMap), isSoft = tp.isSoft)
       case tp @ CapturingType(parent, refs) =>
         if !ctx.mode.is(Mode.Type)
-            && refs.subCaptures(parent.captureSet, frozen = true).isOK
+            && refs.subCaptures(parent.captureSet, Frozen.All).isOK
             && (tp.isBoxed || !parent.isBoxedCapturing)
               // fuse types with same boxed status and outer boxed with any type
         then

scala2-library-cc/src/scala/collection/IndexedSeqView.scala

@@ -136,7 +136,7 @@ object IndexedSeqView {
 
   @SerialVersionUID(3L)
   class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)
-    extends SeqView.Concat[A](prefix, caps.unsafe.unsafeAssumeSeparate(suffix)) with IndexedSeqView[A]
+    extends SeqView.Concat[A](prefix, suffix) with IndexedSeqView[A]
 
   @SerialVersionUID(3L)
   class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)

scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala

@@ -75,7 +75,7 @@ private[mutable] object CheckedIndexedSeqView {
 
   @SerialVersionUID(3L)
   class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int)
-    extends IndexedSeqView.Concat[A](prefix, caps.unsafe.unsafeAssumeSeparate(suffix)) with CheckedIndexedSeqView[A]
+    extends IndexedSeqView.Concat[A](prefix, suffix) with CheckedIndexedSeqView[A]
 
   @SerialVersionUID(3L)
   class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int)