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

@@ -17,6 +17,7 @@ import typer.ErrorReporting.Addenda
 import TypeComparer.linkOK
 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.
@@ -56,10 +57,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
@@ -242,9 +247,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`.
@@ -414,7 +417,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
@@ -434,7 +439,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 =
@@ -443,9 +448,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
 
@@ -519,12 +521,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) =>
@@ -602,8 +602,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
 
@@ -622,13 +622,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):
@@ -657,7 +650,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]
@@ -754,7 +747,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
@@ -788,7 +781,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
@@ -818,7 +811,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
@@ -908,7 +901,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
@@ -1151,6 +1144,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`,
@@ -585,6 +586,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")
@@ -688,13 +692,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
 
     override def recheckRHS(rhs: Tree, pt: Type)(using Context): Type =
       def avoidMap = new TypeOps.AvoidMap:
@@ -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
 
@@ -824,9 +830,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
@@ -990,7 +996,11 @@ class CheckCaptures extends Recheck, SymTransformer:
 
       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)
+        curEnv = Env(
+          curEnv.owner,
+          EnvKind.NestedInOwner,
+          CaptureSet.Var(curEnv.owner, level = currentLevel),
+          if boxed then null else curEnv)
         try op
         finally curEnv = saved
 

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

@@ -17,7 +17,7 @@ Handling existentials in CC:
 
 In adapt:
 
-  - If an EX is toplevel in expected type, replace with a fresh capture set variable
+  - If an EX is toplevel in expected type, replace with `cap`.
   - If an EX is toplevel in actual type, find a trackable replacement `x` as follows:
       + If actual type is a trackable ref, pick that
       + Otherwise, create a fresh skolem val symbol with currently enclosing
@@ -26,30 +26,31 @@ In adapt:
       + If the EX-bound variable appears only at toplevel, replace it with `x`
       + Otherwise, replace it with `x*`.
 
-In avoidance of a type T:
+Delayed packing:
 
-  - Replace all co-variant occurrences of locals variables in T (including locally
-    created EX-skolems) with single fresh EX-bound variable, which wraps T.
-  - Contravariant occurrences of local variables are approximated by the empty capture set,
-    as was the case before.
-  - Invariant occurrences of local variables produce errors, as was the case before.
-  - Check that no existentially quantified local variable appears under a box.
+ - When typing a `def` (including an anonymoys function), convert all covariant
+   toplevel `cap`s to a fresh existential variable wrapping the result type.
 
-The reason it is done this way is that it produces the smallest existential type
-wrt the existential type ordering shown below. For instance, consider the type
+Level checking and avoidance:
 
-      (A^{x}, B^{y})
+  - Environments, capture refs, and capture set variables carry levels
 
-where `x` and `y` are local. We widen to
+    + levels start at 0
+    + The level of a block or template statement sequence is one higher than the level of
+      its environment
+    + The level of a TermRef is the level of the environment where its symbol is defined.
+    + The level of a ThisType is the level of the statements of the class to which it beloongs.
+    + The level of a TermParamRef is currently -1 (i.e. TermParamRefs are not yet checked using this system)
+    + The level of a capture set variable is the level of the environment where it is created.
 
-      EX a.(A^{a}, B^{a})
+  - Variables also carry info whether they accept `cap` or not. Variables introduced under a box
+    don't, the others do.
 
-rather than
-
-      EX a.EX b.(A^{a}, A^{b})
-
-In the subtype ordering of existentials the first of these types is a subtype of
-the other, but not _vice versa_.
+  - Capture set variables do not accept elements of level higher than the variable's level
+  - We use avoidance to heal such cases: If the level-incorrect ref appears
+    + covariantly: widen to underlying capture set, reject if that is cap and the variable does not allow it
+    + contravariantly: narrow to {}
+    + invarianty: reject with error
 
 In cv-computation (markFree):