Handle levels in constraint solving

 - Define a notion of ccNestingLevel, which corresponds to the nesting level
   of so called "level owners" relative to each other.
 - The outermost level owner is _root_.
 - Other level owners are classes that are not staticOwners
   and methods that are not constructors.
 - The ccNestingLevel of any symbol is the ccNestingLevel of its closest enclosing
   level owner, or -1 for NoSymbol.
 - Capture set variables are created with a level owner.
 - Capture set variables cannot include elements with higher ccNestingLevels
   than the variable's owner.
 - If level-incorrect elements are attempted to be added to a capture set variable,
   they are instead widened to the underlying capture set.

Author: odersky

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

@@ -253,6 +253,41 @@ extension (sym: Symbol)
     && sym != defn.Caps_unsafeBox
     && sym != defn.Caps_unsafeUnbox
 
+  /** The owner of the current level. Qualifying owners are
+   *   - methods other than constructors
+   *   - classes, if they are not staticOwners
+   *   - _root_
+   */
+  def levelOwner(using Context): Symbol =
+    if sym.isStaticOwner then defn.RootClass
+    else if sym.isClass || sym.is(Method) && !sym.isConstructor then sym
+    else sym.owner.levelOwner
+
+  /** The nesting level of `sym` for the purposes of `cc`,
+   *  -1 for NoSymbol
+   */
+  def ccNestingLevel(using Context): Int =
+    if sym.exists then
+      val lowner = sym.levelOwner
+      val cache = ctx.property(CheckCaptures.NestingLevels).get
+      cache.getOrElseUpdate(lowner,
+        if lowner.isRoot then 0 else lowner.owner.ccNestingLevel + 1)
+    else -1
+
+  /** Optionally, the nesting level of `sym` for the purposes of `cc`, provided
+   *  a capture checker is running.
+   */
+  def ccNestingLevelOpt(using Context): Option[Int] =
+    if ctx.property(CheckCaptures.NestingLevels).isDefined then
+      Some(ccNestingLevel)
+    else None
+
+  def maxNested(other: Symbol)(using Context): Symbol =
+    if sym.ccNestingLevel < other.ccNestingLevel then other else sym
+
+  def minNested(other: Symbol)(using Context): Symbol =
+    if sym.ccNestingLevel > other.ccNestingLevel then other else sym
+
 extension (tp: AnnotatedType)
   /** Is this a boxed capturing type? */
   def isBoxed(using Context): Boolean = tp.annot match

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

@@ -12,7 +12,7 @@ import annotation.internal.sharable
 import reporting.trace
 import printing.{Showable, Printer}
 import printing.Texts.*
-import util.{SimpleIdentitySet, Property}
+import util.{SimpleIdentitySet, Property, optional}, optional.{break, ?}
 import util.common.alwaysTrue
 import scala.collection.mutable
 import config.Config.ccAllowUnsoundMaps
@@ -55,6 +55,11 @@ sealed abstract class CaptureSet extends Showable:
    */
   def isAlwaysEmpty: Boolean
 
+  /** The level owner in which the set is defined. Sets can only take
+   *  elements with nesting level up to the cc-nestinglevel of owner.
+   */
+  def owner: Symbol
+
   /** Is this capture set definitely non-empty? */
   final def isNotEmpty: Boolean = !elems.isEmpty
 
@@ -123,10 +128,14 @@ sealed abstract class CaptureSet extends Showable:
    *                 as frozen.
    */
   def accountsFor(x: CaptureRef)(using Context): Boolean =
-    reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true) {
-      elems.exists(_.subsumes(x))
-      || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
-    }
+    if comparer.isInstanceOf[ExplainingTypeComparer] then // !!! DEBUG
+      reporting.trace.force(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
+        elems.exists(_.subsumes(x))
+        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+    else
+      reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
+        elems.exists(_.subsumes(x))
+        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
 
   /** A more optimistic version of accountsFor, which does not take variable supersets
    *  of the `x` reference into account. A set might account for `x` if it accounts
@@ -191,7 +200,8 @@ sealed abstract class CaptureSet extends Showable:
     if this.subCaptures(that, frozen = true).isOK then that
     else if that.subCaptures(this, frozen = true).isOK then this
     else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
-    else Var(this.elems ++ that.elems).addAsDependentTo(this).addAsDependentTo(that)
+    else Var(this.owner.maxNested(that.owner), this.elems ++ that.elems)
+      .addAsDependentTo(this).addAsDependentTo(that)
 
   /** The smallest superset (via <:<) of this capture set that also contains `ref`.
    */
@@ -276,7 +286,9 @@ sealed abstract class CaptureSet extends Showable:
     if isUniversal then handler()
     this
 
-  /** Invoke handler on the elements to check wellformedness of the capture set */
+  /** Invoke handler on the elements to ensure wellformedness of the capture set.
+   *  The handler might add additional elements to the capture set.
+   */
   def ensureWellformed(handler: List[CaptureRef] => Context ?=> Unit)(using Context): this.type =
     handler(elems.toList)
     this
@@ -353,6 +365,8 @@ object CaptureSet:
 
     def withDescription(description: String): Const = Const(elems, description)
 
+    def owner = NoSymbol
+
     override def toString = elems.toString
   end Const
 
@@ -371,16 +385,23 @@ object CaptureSet:
   end Fluid
 
   /** The subclass of captureset variables with given initial elements */
-  class Var(initialElems: Refs = emptySet) extends CaptureSet:
+  class Var(directOwner: Symbol, initialElems: Refs = emptySet)(using @constructorOnly ictx: Context) extends CaptureSet:
 
     /** A unique identification number for diagnostics */
     val id =
       varId += 1
       varId
 
+    override val owner = directOwner.levelOwner
+
     /** A variable is solved if it is aproximated to a from-then-on constant set. */
     private var isSolved: Boolean = false
 
+    private var ownLevelCache = -1
+    private def ownLevel(using Context) =
+      if ownLevelCache == -1 then ownLevelCache = owner.ccNestingLevel
+      ownLevelCache
+
     /** The elements currently known to be in the set */
     var elems: Refs = initialElems
 
@@ -425,16 +446,30 @@ object CaptureSet:
       deps = state.deps(this)
 
     def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
-      if !isConst && recordElemsState() then
+      if isConst || !recordElemsState() then
+        CompareResult.fail(this) // fail if variable is solved or given VarState is frozen
+      else if levelsOK(newElems) then
         elems ++= newElems
         if isUniversal then rootAddedHandler()
         newElemAddedHandler(newElems.toList)
         // assert(id != 5 || elems.size != 3, this)
         (CompareResult.OK /: deps) { (r, dep) =>
           r.andAlso(dep.tryInclude(newElems, this))
         }
-      else // fail if variable is solved or given VarState is frozen
-        CompareResult.fail(this)
+      else widenCaptures(newElems) match
+        case Some(newElems1) => tryInclude(newElems1, origin)
+        case None => CompareResult.fail(this)
+
+    private def levelsOK(elems: Refs)(using Context): Boolean =
+      !elems.exists(_.ccNestingLevel > ownLevel)
+
+    private def widenCaptures(elems: Refs)(using Context): Option[Refs] =
+      optional:
+        (SimpleIdentitySet[CaptureRef]() /: elems): (acc, elem) =>
+          if elem.ccNestingLevel <= ownLevel then acc + elem
+          else if elem.isRootCapability then break()
+          else acc ++ widenCaptures(elem.captureSetOfInfo.elems).?
+      .showing(i"widen catures ${elems.toList} for $this at $owner = $result", capt)
 
     def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult =
       if (cs eq this) || cs.isUniversal || isConst then
@@ -519,8 +554,8 @@ object CaptureSet:
   end Var
 
   /** A variable that is derived from some other variable via a map or filter. */
-  abstract class DerivedVar(initialElems: Refs)(using @constructorOnly ctx: Context)
-  extends Var(initialElems):
+  abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
+  extends Var(owner, initialElems):
 
     // For debugging: A trace where a set was created. Note that logically it would make more
     // sense to place this variable in Mapped, but that runs afoul of the initializatuon checker.
@@ -546,7 +581,7 @@ object CaptureSet:
    */
   class Mapped private[CaptureSet]
     (val source: Var, tm: TypeMap, variance: Int, initial: CaptureSet)(using @constructorOnly ctx: Context)
-  extends DerivedVar(initial.elems):
+  extends DerivedVar(source.owner, initial.elems):
     addAsDependentTo(initial)  // initial mappings could change by propagation
 
     private def mapIsIdempotent = tm.isInstanceOf[IdempotentCaptRefMap]
@@ -612,7 +647,7 @@ object CaptureSet:
    */
   final class BiMapped private[CaptureSet]
     (val source: Var, bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
-  extends DerivedVar(initialElems):
+  extends DerivedVar(source.owner, initialElems):
 
     override def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
       if origin eq source then
@@ -642,7 +677,7 @@ object CaptureSet:
   /** A variable with elements given at any time as { x <- source.elems | p(x) } */
   class Filtered private[CaptureSet]
     (val source: Var, p: Context ?=> CaptureRef => Boolean)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.elems.filter(p)):
+  extends DerivedVar(source.owner, source.elems.filter(p)):
 
     override def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
       val filtered = newElems.filter(p)
@@ -673,7 +708,7 @@ object CaptureSet:
   extends Filtered(source, !other.accountsFor(_))
 
   class Intersected(cs1: CaptureSet, cs2: CaptureSet)(using Context)
-  extends Var(elemIntersection(cs1, cs2)):
+  extends Var(cs1.owner.minNested(cs2.owner), elemIntersection(cs1, cs2)):
     addAsDependentTo(cs1)
     addAsDependentTo(cs2)
     deps += cs1

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

@@ -189,6 +189,9 @@ object CheckCaptures:
   /** Attachment key for bodies of closures, provided they are values */
   val ClosureBodyValue = Property.Key[Unit]
 
+  /** Attachment key for the nesting level cache */
+  val NestingLevels = Property.Key[mutable.HashMap[Symbol, Int]]
+
 class CheckCaptures extends Recheck, SymTransformer:
   thisPhase =>
 
@@ -263,7 +266,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         report.error(em"$header included in allowed capture set ${res.blocking}", pos)
 
     /** The current environment */
-    private var curEnv: Env = Env(NoSymbol, EnvKind.Regular, CaptureSet.empty, null)
+    private var curEnv: Env = inContext(ictx):
+      Env(defn.RootClass, EnvKind.Regular, CaptureSet.empty, null)
 
     private val myCapturedVars: util.EqHashMap[Symbol, CaptureSet] = EqHashMap()
 
@@ -272,7 +276,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     def capturedVars(sym: Symbol)(using Context) =
       myCapturedVars.getOrElseUpdate(sym,
-        if sym.ownersIterator.exists(_.isTerm) then CaptureSet.Var()
+        if sym.ownersIterator.exists(_.isTerm) then
+          CaptureSet.Var(if sym.isConstructor then sym.owner.owner else sym.owner)
         else CaptureSet.empty)
 
     /** For all nested environments up to `limit` or a closed environment perform `op`,
@@ -655,9 +660,9 @@ class CheckCaptures extends Recheck, SymTransformer:
       val saved = curEnv
       tree match
         case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
-          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner), curEnv)
         case _ if tree.hasAttachment(ClosureBodyValue) =>
-          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner), curEnv)
         case _ =>
       val res =
         try super.recheck(tree, pt)
@@ -674,13 +679,10 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  of simulated boxing and unboxing.
      */
     override def recheckFinish(tpe: Type, tree: Tree, pt: Type)(using Context): Type =
-      val typeToCheck = tree match
-        case _: Ident | _: Select | _: Apply | _: TypeApply if tree.symbol.unboxesResult =>
-          tpe
-        case _: Try =>
-          tpe
-        case _ =>
-          NoType
+      def needsUniversalCheck = tree match
+        case _: RefTree | _: Apply | _: TypeApply => tree.symbol.unboxesResult
+        case _: Try => true
+        case _ => false
       def checkNotUniversal(tp: Type): Unit = tp.widenDealias match
         case wtp @ CapturingType(parent, refs) =>
           refs.disallowRootCapability { () =>
@@ -691,8 +693,10 @@ class CheckCaptures extends Recheck, SymTransformer:
           }
           checkNotUniversal(parent)
         case _ =>
-      if !allowUniversalInBoxed then checkNotUniversal(typeToCheck)
+      if !allowUniversalInBoxed && needsUniversalCheck then
+        checkNotUniversal(tpe)
       super.recheckFinish(tpe, tree, pt)
+    end recheckFinish
 
   // ------------------ Adaptation -------------------------------------
   //
@@ -782,6 +786,12 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     def adaptBoxed(actual: Type, expected: Type, pos: SrcPos, alwaysConst: Boolean = false)(using Context): Type =
 
+      inline def inNestedEnv[T](boxed: Boolean)(op: => T): T =
+        val saved = curEnv
+        curEnv = Env(curEnv.owner, EnvKind.NestedInOwner, CaptureSet.Var(curEnv.owner), if boxed then null else curEnv)
+        try op
+        finally curEnv = saved
+
       /** Adapt function type `actual`, which is `aargs -> ares` (possibly with dependencies)
        *  to `expected` type.
        *  It returns the adapted type along with a capture set consisting of the references
@@ -791,10 +801,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       def adaptFun(actual: Type, aargs: List[Type], ares: Type, expected: Type,
           covariant: Boolean, boxed: Boolean,
           reconstruct: (List[Type], Type) => Type): (Type, CaptureSet) =
-        val saved = curEnv
-        curEnv = Env(curEnv.owner, EnvKind.NestedInOwner, CaptureSet.Var(), if boxed then null else curEnv)
-
-        try
+        inNestedEnv(boxed):
           val (eargs, eres) = expected.dealias.stripCapturing match
             case defn.FunctionOf(eargs, eres, _) => (eargs, eres)
             case expected: MethodType => (expected.paramInfos, expected.resType)
@@ -808,8 +815,6 @@ class CheckCaptures extends Recheck, SymTransformer:
             else reconstruct(aargs1, ares1)
 
           (resTp, curEnv.captured)
-        finally
-          curEnv = saved
 
       /** Adapt type function type `actual` to the expected type.
        *  @see [[adaptFun]]
@@ -818,10 +823,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           actual: Type, ares: Type, expected: Type,
           covariant: Boolean, boxed: Boolean,
           reconstruct: Type => Type): (Type, CaptureSet) =
-        val saved = curEnv
-        curEnv = Env(curEnv.owner, EnvKind.NestedInOwner, CaptureSet.Var(), if boxed then null else curEnv)
-
-        try
+        inNestedEnv(boxed):
           val eres = expected.dealias.stripCapturing match
             case RefinedType(_, _, rinfo: PolyType) => rinfo.resType
             case expected: PolyType => expected.resType
@@ -834,8 +836,6 @@ class CheckCaptures extends Recheck, SymTransformer:
             else reconstruct(ares1)
 
           (resTp, curEnv.captured)
-        finally
-          curEnv = saved
       end adaptTypeFun
 
       def adaptInfo(actual: Type, expected: Type, covariant: Boolean): String =
@@ -977,16 +977,16 @@ class CheckCaptures extends Recheck, SymTransformer:
         traverseChildren(t)
 
     override def checkUnit(unit: CompilationUnit)(using Context): Unit =
-      Setup(preRecheckPhase, thisPhase, recheckDef)(ctx.compilationUnit.tpdTree)
-      //println(i"SETUP:\n${Recheck.addRecheckedTypes.transform(ctx.compilationUnit.tpdTree)}")
-      withCaptureSetsExplained {
-        super.checkUnit(unit)
-        checkOverrides.traverse(unit.tpdTree)
-        checkSelfTypes(unit.tpdTree)
-        postCheck(unit.tpdTree)
-        if ctx.settings.YccDebug.value then
-          show(unit.tpdTree) // this does not print tree, but makes its variables visible for dependency printing
-      }
+      inContext(ctx.withProperty(NestingLevels, Some(new mutable.HashMap[Symbol, Int]))):
+        Setup(preRecheckPhase, thisPhase, this)(ctx.compilationUnit.tpdTree)
+        //println(i"SETUP:\n${Recheck.addRecheckedTypes.transform(ctx.compilationUnit.tpdTree)}")
+        withCaptureSetsExplained:
+          super.checkUnit(unit)
+          checkOverrides.traverse(unit.tpdTree)
+          checkSelfTypes(unit.tpdTree)
+          postCheck(unit.tpdTree)
+          if ctx.settings.YccDebug.value then
+            show(unit.tpdTree) // this does not print tree, but makes its variables visible for dependency printing
 
     /** Check that self types of subclasses conform to self types of super classes.
      *  (See comment below how this is achieved). The check assumes that classes
@@ -1139,6 +1139,8 @@ class CheckCaptures extends Recheck, SymTransformer:
               ||                                // non-local symbols cannot have inferred types since external capture types are not inferred
                 isLocal                         // local symbols still need explicit types if
                 && !sym.owner.is(Trait)         // they are defined in a trait, since we do OverridingPairs checking before capture inference
+              ||
+                sym.allOverriddenSymbols.nonEmpty
             def isNotPureThis(ref: CaptureRef) = ref match {
               case ref: ThisType => !ref.cls.isPureClass
               case _ => true