More robust level handling

Author: odersky

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

@@ -14,6 +14,7 @@ import tpd.*
 import StdNames.nme
 import config.Feature
 import collection.mutable
+import CCState.*
 
 private val Captures: Key[CaptureSet] = Key()
 
@@ -64,11 +65,47 @@ class CCState:
    */
   var levelError: Option[CaptureSet.CompareResult.LevelError] = None
 
+  private var curLevel: Level = outermostLevel
+  private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
+
+object CCState:
+
+  opaque type Level = Int
+
+  val undefinedLevel: Level = -1
+
+  val outermostLevel: Level = 0
+
+  /** The level of the current environment. Levels start at 0 and increase for
+   *  each nested function or class. -1 means the level is undefined.
+   */
+  def currentLevel(using Context): Level = ccState.curLevel
+
+  inline def inNestedLevel[T](inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.curLevel
+    ccs.curLevel = ccs.curLevel.nextInner
+    try op finally ccs.curLevel = saved
+
+  inline def inNestedLevelUnless[T](inline p: Boolean)(inline op: T)(using Context): T =
+    val ccs = ccState
+    val saved = ccs.curLevel
+    if !p then ccs.curLevel = ccs.curLevel.nextInner
+    try op finally ccs.curLevel = saved
+
+  extension (x: Level)
+    def isDefined: Boolean = x >= 0
+    def <= (y: Level) = (x: Int) <= y
+    def nextInner: Level = if isDefined then x + 1 else x
+
+  extension (sym: Symbol)(using Context)
+    def ccLevel: Level = ccState.symLevel.getOrElse(sym, -1)
+    def recordLevel() = ccState.symLevel(sym) = currentLevel
 end CCState
 
 /** The currently valid CCState */
 def ccState(using Context) =
-  Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState
+  Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState1
 
 class NoCommonRoot(rs: Symbol*)(using Context) extends Exception(
   i"No common capture root nested in ${rs.mkString(" and ")}"
@@ -339,6 +376,12 @@ extension (tp: Type)
       case _ =>
         tp
 
+  def level(using Context): Level =
+    tp match
+    case tp: TermRef => tp.symbol.ccLevel
+    case tp: ThisType => tp.cls.ccLevel.nextInner
+    case _ => undefinedLevel
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =
@@ -423,9 +466,7 @@ extension (sym: Symbol)
     || sym.is(Method, butNot = Accessor)
 
   /** The owner of the current level. Qualifying owners are
-   *   - methods other than constructors and anonymous functions
-   *   - anonymous functions, provided they either define a local
-   *     root of type caps.Capability, or they are the rhs of a val definition.
+   *   - methods, other than accessors
    *   - classes, if they are not staticOwners
    *   - _root_
    */

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

@@ -16,6 +16,7 @@ import util.{SimpleIdentitySet, Property}
 import typer.ErrorReporting.Addenda
 import util.common.alwaysTrue
 import scala.collection.mutable
+import CCState.*
 
 /** A class for capture sets. Capture sets can be constants or variables.
  *  Capture sets support inclusion constraints <:< where <:< is subcapturing.
@@ -55,10 +56,14 @@ sealed abstract class CaptureSet extends Showable:
    */
   def isAlwaysEmpty: Boolean
 
-  /** An optional level limit, or NoSymbol if none exists. All elements of the set
-   *  must be in scopes visible from the level limit.
+  /** An optional level limit, or undefinedLevel if none exists. All elements of the set
+   *  must be at levels equal or smaller than the level of the set, if it is defined.
    */
-  def levelLimit: Symbol
+  def level: Level
+
+  /** An optional owner, or NoSymbol if none exists. Used for diagnstics
+   */
+  def owner: Symbol
 
   /** Is this capture set definitely non-empty? */
   final def isNotEmpty: Boolean = !elems.isEmpty
@@ -239,9 +244,7 @@ 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.levelLimit.maxNested(that.levelLimit, onConflict = (sym1, sym2) => sym1),
-        this.elems ++ that.elems)
+    else Var(initialElems = this.elems ++ that.elems)
       .addAsDependentTo(this).addAsDependentTo(that)
 
   /** The smallest superset (via <:<) of this capture set that also contains `ref`.
@@ -411,7 +414,9 @@ object CaptureSet:
 
     def withDescription(description: String): Const = Const(elems, description)
 
-    def levelLimit = NoSymbol
+    def level = undefinedLevel
+
+    def owner = NoSymbol
 
     override def toString = elems.toString
   end Const
@@ -431,7 +436,7 @@ object CaptureSet:
   end Fluid
 
   /** The subclass of captureset variables with given initial elements */
-  class Var(directOwner: Symbol, initialElems: Refs = emptySet)(using @constructorOnly ictx: Context) extends CaptureSet:
+  class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptySet, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
 
     /** A unique identification number for diagnostics */
     val id =
@@ -440,9 +445,6 @@ object CaptureSet:
 
     //assert(id != 40)
 
-    override val levelLimit =
-      if directOwner.exists then directOwner.levelOwner else NoSymbol
-
     /** A variable is solved if it is aproximated to a from-then-on constant set. */
     private var isSolved: Boolean = false
 
@@ -516,12 +518,10 @@ object CaptureSet:
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
       if elem.isRootCapability then !noUniversal
       else elem match
-        case elem: TermRef if levelLimit.exists =>
-          var sym = elem.symbol
-          if sym.isLevelOwner then sym = sym.owner
-          levelLimit.isContainedIn(sym.levelOwner)
-        case elem: ThisType if levelLimit.exists =>
-          levelLimit.isContainedIn(elem.cls.levelOwner)
+        case elem: TermRef if level.isDefined =>
+          elem.symbol.ccLevel <= level
+        case elem: ThisType if level.isDefined =>
+          elem.cls.ccLevel.nextInner <= level
         case ReachCapability(elem1) =>
           levelOK(elem1)
         case MaybeCapability(elem1) =>
@@ -599,8 +599,8 @@ object CaptureSet:
       val debugInfo =
         if !isConst && ctx.settings.YccDebug.value then ids else ""
       val limitInfo =
-        if ctx.settings.YprintLevel.value && levelLimit.exists
-        then i"<in $levelLimit>"
+        if ctx.settings.YprintLevel.value && level.isDefined
+        then i"<at level ${level.toString}>"
         else ""
       debugInfo ++ limitInfo
 
@@ -619,13 +619,6 @@ 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(directOwner: Symbol)(using Context) extends Var(directOwner):
-    override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context) = this
-
   /** 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)
   extends Var(owner, initialElems):
@@ -654,7 +647,7 @@ object CaptureSet:
    */
   class Mapped private[CaptureSet]
     (val source: Var, tm: TypeMap, variance: Int, initial: CaptureSet)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, initial.elems):
+  extends DerivedVar(source.owner, initial.elems):
     addAsDependentTo(initial)  // initial mappings could change by propagation
 
     private def mapIsIdempotent = tm.isInstanceOf[IdempotentCaptRefMap]
@@ -751,7 +744,7 @@ object CaptureSet:
    */
   final class BiMapped private[CaptureSet]
     (val source: Var, bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
-  extends DerivedVar(source.levelLimit, initialElems):
+  extends DerivedVar(source.owner, initialElems):
 
     override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
       if origin eq source then
@@ -785,7 +778,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.levelLimit, source.elems.filter(p)):
+  extends DerivedVar(source.owner, source.elems.filter(p)):
 
     override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
       if accountsFor(elem) then
@@ -815,7 +808,7 @@ object CaptureSet:
   extends Filtered(source, !other.accountsFor(_))
 
   class Intersected(cs1: CaptureSet, cs2: CaptureSet)(using Context)
-  extends Var(cs1.levelLimit.minNested(cs2.levelLimit), elemIntersection(cs1, cs2)):
+  extends Var(initialElems = elemIntersection(cs1, cs2)):
     addAsDependentTo(cs1)
     addAsDependentTo(cs2)
     deps += cs1
@@ -905,7 +898,7 @@ object CaptureSet:
             if ctx.settings.YccDebug.value then printer.toText(trace, ", ")
             else blocking.show
           case LevelError(cs: CaptureSet, elem: CaptureRef) =>
-            Str(i"($elem at wrong level for $cs in ${cs.levelLimit})")
+            Str(i"($elem at wrong level for $cs at level ${cs.level.toString})")
 
     /** The result is OK */
     def isOK: Boolean = this == OK
@@ -1148,6 +1141,6 @@ object CaptureSet:
           i"""
             |
             |Note that reference ${ref}$levelStr
-            |cannot be included in outer capture set $cs which is associated with ${cs.levelLimit}"""
+            |cannot be included in outer capture set $cs"""
 
 end CaptureSet

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

@@ -19,6 +19,7 @@ import transform.{Recheck, PreRecheck, CapturedVars}
 import Recheck.*
 import scala.collection.mutable
 import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
+import CCState.*
 import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.trace
@@ -191,7 +192,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     if Feature.ccEnabled then
       super.run
 
-  val ccState = new CCState
+  val ccState1 = new CCState // Dotty problem: Rename to ccState ==> Crash in ExplicitOuter
 
   class CaptureChecker(ictx: Context) extends Rechecker(ictx):
 
@@ -311,7 +312,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
         if sym.ownersIterator.exists(_.isTerm)
-        then CaptureSet.Var(sym.owner)
+        then CaptureSet.Var(sym.owner, level = sym.ccLevel)
         else CaptureSet.empty)
 
     /** For all nested environments up to `limit` or a closed environment perform `op`,
@@ -592,6 +593,9 @@ class CheckCaptures extends Recheck, SymTransformer:
               tree.srcPos)
       super.recheckTypeApply(tree, pt)
 
+    override def recheckBlock(tree: Block, pt: Type)(using Context): Type =
+      inNestedLevel(super.recheckBlock(tree, pt))
+
     override def recheckClosure(tree: Closure, pt: Type, forceDependent: Boolean)(using Context): Type =
       val cs = capturedVars(tree.meth.symbol)
       capt.println(i"typing closure $tree with cvs $cs")
@@ -695,13 +699,14 @@ class CheckCaptures extends Recheck, SymTransformer:
         val localSet = capturedVars(sym)
         if !localSet.isAlwaysEmpty then
           curEnv = Env(sym, EnvKind.Regular, localSet, curEnv)
-        try checkInferredResult(super.recheckDefDef(tree, sym), tree)
-        finally
-          if !sym.isAnonymousFunction then
-            // Anonymous functions propagate their type to the enclosing environment
-            // so it is not in general sound to interpolate their types.
-            interpolateVarsIn(tree.tpt)
-          curEnv = saved
+        inNestedLevel:
+          try checkInferredResult(super.recheckDefDef(tree, sym), tree)
+          finally
+            if !sym.isAnonymousFunction then
+              // Anonymous functions propagate their type to the enclosing environment
+              // so it is not in general sound to interpolate their types.
+              interpolateVarsIn(tree.tpt)
+            curEnv = saved
 
     /** If val or def definition with inferred (result) type is visible
      *  in other compilation units, check that the actual inferred type
@@ -771,7 +776,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           checkSubset(thisSet,
             CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
             selfType.srcPos, cs1description = " captured by this self type")
-        super.recheckClassDef(tree, impl, cls)
+        inNestedLevelUnless(cls.is(Module)):
+          super.recheckClassDef(tree, impl, cls)
       finally
         curEnv = saved
 
@@ -823,9 +829,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.owner), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner, level = currentLevel), curEnv)
         case _ if tree.hasAttachment(ClosureBodyValue) =>
-          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner), curEnv)
+          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner, level = currentLevel), curEnv)
         case _ =>
       val res =
         try
@@ -995,7 +1001,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           val saved = curEnv
           curEnv = Env(
             curEnv.owner, EnvKind.NestedInOwner,
-            CaptureSet.Var(curEnv.owner),
+            CaptureSet.Var(curEnv.owner, level = currentLevel),
             if boxed then null else curEnv)
           try
             val (eargs, eres) = expected.dealias.stripCapturing match