Changes to Fresh and Separation Checking

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

@@ -12,7 +12,7 @@ import CCState.*
 import Periods.{NoRunId, RunWidth}
 import compiletime.uninitialized
 import StdNames.nme
-import CaptureSet.VarState
+import CaptureSet.{Refs, emptyRefs, VarState}
 import Annotations.Annotation
 import Flags.*
 import config.Printers.capt
@@ -147,7 +147,7 @@ object Capabilities:
    *  @param origin  an indication where and why the FreshCap was created, used
    *                 for diagnostics
    */
-  case class FreshCap private (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability:
+  case class FreshCap (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability:
     val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
       // fails initialization check without the @unchecked
 
@@ -547,6 +547,23 @@ object Capabilities:
           captureSetValid = currentId
         computed
 
+    /** The elements hidden by this capability, if this is a FreshCap
+     *  or a derived version of one. Read-only status and restrictions
+     *  are transferred from the capability to its hidden set.
+     */
+    def hiddenSet(using Context): Refs = computeHiddenSet(identity)
+
+    /** Compute result based on hidden set of this capability.
+     *  Restrictions and read-only status transfer from the capability to its
+     *  hidden set.
+     *  @param  f   a function that gets applied to all detected hidden sets
+     */
+    def computeHiddenSet(f: Refs => Refs)(using Context): Refs = this match
+      case self: FreshCap => f(self.hiddenSet.elems)
+      case Restricted(elem1, cls) => elem1.computeHiddenSet(f).map(_.restrict(cls))
+      case ReadOnly(elem1) => elem1.computeHiddenSet(f).map(_.readOnly)
+      case _ => emptyRefs
+
     /** The transitive classifiers of this capability. */
     def transClassifiers(using Context): Classifiers =
       def toClassifiers(cls: ClassSymbol): Classifiers =
@@ -753,25 +770,44 @@ object Capabilities:
      *   x covers x
      *   x covers y  ==>  x covers y.f
      *   x covers y  ==>  x* covers y*, x? covers y?
+     *   x covers y  ==>  <fresh hiding x> covers y
+     *   x covers y  ==>  x.only[C] covers y, x covers y.only[C]
+     *
      *   TODO what other clauses from subsumes do we need to port here?
+     *   The last clause is a conservative over-approximation: basically, we can't achieve
+     *   separation by having different classifiers for now. It would be good to
+     *   have a test that would expect such separation, then we can try to refine
+     *   the clause to make the test pass.
      */
     final def covers(y: Capability)(using Context): Boolean =
-      (this eq y)
-      || y.match
-          case y @ TermRef(ypre: Capability, _) =>
-            this.covers(ypre)
-          case Reach(y1) =>
-            this match
-              case Reach(x1) => x1.covers(y1)
-              case _ => false
-          case Maybe(y1) =>
-            this match
-              case Maybe(x1) => x1.covers(y1)
-              case _ => false
-          case y: FreshCap =>
-            y.hiddenSet.superCaps.exists(this.covers(_))
-          case _ =>
-            false
+      val seen: util.EqHashSet[FreshCap] = new util.EqHashSet
+
+      def recur(x: Capability, y: Capability): Boolean =
+        (x eq y)
+        || y.match
+            case y @ TermRef(ypre: Capability, _) =>
+              recur(x, ypre)
+            case Reach(y1) =>
+              x match
+                case Reach(x1) => recur(x1, y1)
+                case _ => false
+            case Maybe(y1) =>
+              x match
+                case Maybe(x1) => recur(x1, y1)
+                case _ => false
+            case Restricted(y1, _) =>
+              recur(x, y1)
+            case _ =>
+              false
+        || x.match
+            case x: FreshCap if !seen.contains(x) =>
+              seen.add(x)
+              x.hiddenSet.exists(recur(_, y))
+            case Restricted(x1, _) => recur(x1, y)
+            case _ => false
+
+      recur(this, y)
+    end covers
 
     def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] =
       CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)

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

@@ -151,21 +151,37 @@ extension (tp: Type)
     case tp: ObjectCapability => tp.captureSetOfInfo
     case _ => CaptureSet.ofType(tp, followResult = false)
 
-  /** The deep capture set of a type. This is by default the union of all
+  /** Compute a captureset by traversing parts of this type. This is by default the union of all
    *  covariant capture sets embedded in the widened type, as computed by
    *  `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
    *  a singleton capability `x` or a reach capability `x*`, the deep capture
    *  set can be narrowed to`{x*}`.
+   *  @param includeTypevars  if true, return a new FreshCap for every type parameter
+   *                          or abstract type with an Any upper bound. Types with
+   *                          defined upper bound are always mapped to the dcs of their bound
+   *  @param includeBoxed     if true, include capture sets found in boxed parts of this type
    */
-  def deepCaptureSet(includeTypevars: Boolean)(using Context): CaptureSet =
-    val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars)
+  def computeDeepCaptureSet(includeTypevars: Boolean, includeBoxed: Boolean = true)(using Context): CaptureSet =
+    val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars, includeBoxed)
     if dcs.isAlwaysEmpty then tp.captureSet
     else tp match
       case tp: ObjectCapability if tp.isTrackableRef => tp.reach.singletonCaptureSet
       case _ => tp.captureSet ++ dcs
 
+  /** The deep capture set of a type. This is by default the union of all
+   *  covariant capture sets embedded in the widened type, as computed by
+   *  `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
+   *  a singleton capability `x` or a reach capability `x*`, the deep capture
+   *  set can be narrowed to`{x*}`.
+   */
   def deepCaptureSet(using Context): CaptureSet =
-    deepCaptureSet(includeTypevars = false)
+    computeDeepCaptureSet(includeTypevars = false)
+
+  /** The span capture set of a type. This is analogous to deepCaptureSet but ignoring
+   *  capture sets in boxed parts.
+   */
+  def spanCaptureSet(using Context): CaptureSet =
+    computeDeepCaptureSet(includeTypevars = false, includeBoxed = false)
 
   /** A type capturing `ref` */
   def capturing(ref: Capability)(using Context): Type =
@@ -362,7 +378,7 @@ extension (tp: Type)
    */
   def derivesFromCapTraitDeeply(cls: ClassSymbol)(using Context): Boolean =
     val accumulate = new DeepTypeAccumulator[Boolean]:
-      def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet) =
+      def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet, boxed: Boolean) =
         this(acc, parent)
         && (parent.derivesFromCapTrait(cls)
             || refs.isConst && refs.elems.forall(_.derivesFromCapTrait(cls)))
@@ -734,15 +750,15 @@ object ContainsParam:
 abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
   val seen = util.HashSet[Symbol]()
 
-  protected def capturingCase(acc: T, parent: Type, refs: CaptureSet): T
+  protected def capturingCase(acc: T, parent: Type, refs: CaptureSet, boxed: Boolean): T
 
   protected def abstractTypeCase(acc: T, t: TypeRef, upperBound: Type): T
 
   def apply(acc: T, t: Type) =
     if variance < 0 then acc
     else t.dealias match
       case t @ CapturingType(parent, cs) =>
-        capturingCase(acc, parent, cs)
+        capturingCase(acc, parent, cs, t.isBoxed)
       case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) =>
         seen += t.symbol
         abstractTypeCase(acc, t, t.info.bounds.hi)

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

@@ -777,7 +777,7 @@ object CaptureSet:
           assert(elem.subsumes(elem1),
             i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this")
 
-    protected def includeElem(elem: Capability)(using Context): Unit =
+    protected def includeElem(elem: Capability)(using Context, VarState): Unit =
       if !elems.contains(elem) then
         if debugVars && id == debugTarget then
           println(i"###INCLUDE $elem in $this")
@@ -803,7 +803,10 @@ object CaptureSet:
         // id == 108 then assert(false, i"trying to add $elem to $this")
         assert(elem.isWellformed, elem)
         assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
-        includeElem(elem)
+        try includeElem(elem)
+        catch case ex: AssertionError =>
+          println(i"error for incl $elem in $this, ${summon[VarState].toString}")
+          throw ex
         if isBadRoot(elem) then
           rootAddedHandler()
         val normElem = if isMaybeSet then elem else elem.stripMaybe
@@ -947,12 +950,64 @@ object CaptureSet:
     override def toString = s"Var$id$elems"
   end Var
 
-  /** Variables that represent refinements of class parameters can have the universal
-   *  capture set, since they represent only what is the result of the constructor.
-   *  Test case: Without that tweak, logger.scala would not compile.
-   */
-  class RefiningVar(owner: Symbol)(using Context) extends Var(owner):
-    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this
+  /** Variables created in types of inferred type trees */
+  class ProperVar(override val owner: Symbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true, isRefining: Boolean)(using /*@constructorOnly*/ ictx: Context)
+  extends Var(owner, initialElems, nestedOK):
+
+    /** Make sure that capset variables in types of vals and result types of
+     *  non-anonymous functions contain only a single FreshCap, and furthermore
+     *  that that FreshCap has as origin InDecl(owner), where owner is the val
+     *  or def for which the type is defined.
+     *  Note: This currently does not apply to classified or read-only fresh caps.
+     */
+    override def includeElem(elem: Capability)(using ctx: Context, vs: VarState): Unit = elem match
+      case elem: FreshCap
+      if !nestedOK
+          && !elems.contains(elem)
+          && !owner.isAnonymousFunction
+          && ccConfig.newScheme =>
+        def fail = i"attempting to add $elem to $this"
+        def hideIn(fc: FreshCap): Unit =
+          assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail)
+          if !isRefining then
+            // If a variable is added by addCaptureRefinements in a synthetic
+            // refinement of a class type, don't do level checking. The problem is
+            // that the variable might be matched against a type that does not have
+            // a refinement, in which case FreshCaps of the class definition would
+            // leak out in the corresponding places. This will fail level checking.
+            // The disallowBadRoots override below has a similar reason.
+            // TODO: We should instead mark the variable as impossible to instantiate
+            // and drop the refinement later in the inferred type.
+            // Test case is drop-refinement.scala.
+            assert(fc.acceptsLevelOf(elem),
+              i"level failure, cannot add $elem with ${elem.levelOwner} to $owner / $getClass / $fail")
+          fc.hiddenSet.add(elem)
+        val isSubsumed = (false /: elems): (isSubsumed, prev) =>
+          prev match
+            case prev: FreshCap =>
+              hideIn(prev)
+              true
+            case _ => isSubsumed
+        if !isSubsumed then
+          if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then
+            val fc = new FreshCap(owner, Origin.InDecl(owner))
+            assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail)
+            hideIn(fc)
+            super.includeElem(fc)
+          else
+            super.includeElem(elem)
+      case _ =>
+        super.includeElem(elem)
+
+    /** Variables that represent refinements of class parameters can have the universal
+     *  capture set, since they represent only what is the result of the constructor.
+     *  Test case: Without that tweak, logger.scala would not compile.
+     */
+    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) =
+      if isRefining then this
+      else super.disallowBadRoots(upto)(handler)
+
+  end ProperVar
 
   /** A variable that is derived from some other variable via a map or filter. */
   abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
@@ -1163,6 +1218,9 @@ object CaptureSet:
    */
   class HiddenSet(initialOwner: Symbol, val owningCap: FreshCap)(using @constructorOnly ictx: Context)
   extends Var(initialOwner):
+
+    // Updated by anchorCaps in CheckCaptures, but owner can be changed only
+    // if it was NoSymbol before.
     var givenOwner: Symbol = initialOwner
 
     override def owner = givenOwner
@@ -1171,62 +1229,9 @@ object CaptureSet:
 
     description = i"of elements subsumed by a fresh cap in $initialOwner"
 
-    private def aliasRef: FreshCap | Null =
-      if myElems.size == 1 then
-        myElems.nth(0) match
-          case alias: FreshCap if deps.contains(alias.hiddenSet) => alias
-          case _ => null
-      else null
-
-    private def aliasSet: HiddenSet =
-      if myElems.size == 1 then
-        myElems.nth(0) match
-          case alias: FreshCap if deps.contains(alias.hiddenSet) => alias.hiddenSet
-          case _ => this
-      else this
-
-    def superCaps: List[FreshCap] =
-      deps.toList.map(_.asInstanceOf[HiddenSet].owningCap)
-
-    override def elems: Refs =
-      val al = aliasSet
-      if al eq this then super.elems else al.elems
-
-    override def elems_=(refs: Refs) =
-      val al = aliasSet
-      if al eq this then super.elems_=(refs) else al.elems_=(refs)
-
-    /** Add element to hidden set. Also add it to all supersets (as indicated by
-     *  deps of this set). Follow aliases on both hidden set and added element
-     *  before adding. If the added element is also a Fresh instance with
-     *  hidden set H which is a superset of this set, then make this set an
-     *  alias of H.
-     */
+    /** Add element to hidden set. */
     def add(elem: Capability)(using ctx: Context, vs: VarState): Unit =
-      val alias = aliasSet
-      if alias ne this then alias.add(elem)
-      else
-        def addToElems() =
-          assert(!isConst)
-          includeElem(elem)
-          deps.foreach: dep =>
-            assert(dep != this)
-            vs.addHidden(dep.asInstanceOf[HiddenSet], elem)
-        elem match
-          case elem: FreshCap =>
-            if this ne elem.hiddenSet then
-              val alias = elem.hiddenSet.aliasRef
-              if alias != null then
-                add(alias)
-              else if deps.contains(elem.hiddenSet) then // make this an alias of elem
-                capt.println(i"Alias $this to ${elem.hiddenSet}")
-                elems = SimpleIdentitySet(elem)
-                deps = SimpleIdentitySet(elem.hiddenSet)
-              else
-                addToElems()
-                elem.hiddenSet.includeDep(this)
-          case _ =>
-            addToElems()
+      includeElem(elem)
 
     /** Apply function `f` to `elems` while setting `elems` to empty for the
      *  duration. This is used to escape infinite recursions if two Freshs
@@ -1553,7 +1558,7 @@ object CaptureSet:
   /** The capture set of the type underlying the capability `c` */
   def ofInfo(c: Capability)(using Context): CaptureSet = c match
     case Reach(c1) =>
-      c1.widen.deepCaptureSet(includeTypevars = true)
+      c1.widen.computeDeepCaptureSet(includeTypevars = true)
         .showing(i"Deep capture set of $c: ${c1.widen} = ${result}", capt)
     case Restricted(c1, cls) =>
       if cls == defn.NothingClass then CaptureSet.empty
@@ -1615,13 +1620,17 @@ object CaptureSet:
   /** The deep capture set of a type is the union of all covariant occurrences of
    *  capture sets. Nested existential sets are approximated with `cap`.
    */
-  def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false)(using Context): CaptureSet =
+  def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false, includeBoxed: Boolean = true)(using Context): CaptureSet =
     val collect = new DeepTypeAccumulator[CaptureSet]:
-      def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet) =
-        this(acc, parent) ++ refs
+
+      def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet, boxed: Boolean) =
+        if includeBoxed || !boxed then this(acc, parent) ++ refs
+        else this(acc, parent)
+
       def abstractTypeCase(acc: CaptureSet, t: TypeRef, upperBound: Type) =
         if includeTypevars && upperBound.isExactlyAny then fresh(Origin.DeepCS(t))
         else this(acc, upperBound)
+
     collect(CaptureSet.empty, tp)
 
   type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[Capability]]

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

@@ -1376,7 +1376,10 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where local capture roots are instantiated to root variables.
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
-      testAdapted(actual, expected, tree, addenda)(err.typeMismatch)
+      try testAdapted(actual, expected, tree, addenda)(err.typeMismatch)
+      catch case ex: AssertionError =>
+        println(i"error while checking $tree: $actual against $expected")
+        throw ex
 
     @annotation.tailrec
     private def findImpureUpperBound(tp: Type)(using Context): Type = tp match