Moe robust level handling

Author: odersky

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

@@ -64,11 +64,29 @@ class CCState:
    */
   var levelError: Option[CaptureSet.CompareResult.LevelError] = None
 
+  private var myLevel: Int = 0
+
+  inline def inNestedLevel[T](inline op: T): T =
+    myLevel += 1
+    try op finally myLevel -=1
+
+  /** 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 = myLevel
+
+  private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
+
+  def level(sym: Symbol): Int = symLevel.getOrElse(sym, -1)
+
+  def recordLevel(sym: Symbol): Unit =
+    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 +357,13 @@ extension (tp: Type)
       case _ =>
         tp
 
+  def level(using Context): Int = tp match
+    case tp: TermRef => ccState.level(tp.symbol)
+    case tp: ThisType =>
+      val clsLevel = ccState.level(tp.cls)
+      if clsLevel == -1 then -1 else clsLevel + 1
+    case _ => -1
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =

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

@@ -434,7 +434,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(directOwner: Symbol, initialElems: Refs = emptySet, level: Int = -1, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
 
     /** A unique identification number for diagnostics */
     val id =
@@ -520,7 +520,12 @@ object CaptureSet:
       if elem.isRootCapability then !noUniversal
       else elem match
         case elem: TermRef if levelLimit.exists =>
-          levelLimit.isContainedIn(elem.symbol.levelOwner)
+          var sym = elem.symbol
+          val now = level == -1 || ccState.level(sym) <= level
+          val was = levelLimit.isContainedIn(elem.symbol.levelOwner)
+          if was != now then
+            println(i"Diff levelOK $sym at ${ccState.level(sym)} for $this at $level in ${directOwner}, now $now")
+          now
         case elem: ThisType if levelLimit.exists =>
           levelLimit.isContainedIn(elem.cls.levelOwner)
         case ReachCapability(elem1) =>

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

@@ -191,7 +191,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 +311,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 = ccState.level(sym))
         else CaptureSet.empty)
 
     /** For all nested environments up to `limit` or a closed environment perform `op`,
@@ -585,6 +585,9 @@ class CheckCaptures extends Recheck, SymTransformer:
               tree.srcPos)
       super.recheckTypeApply(tree, pt)
 
+    override def recheckBlock(tree: Block, pt: Type)(using Context): Type =
+      ccState.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 +691,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
+        ccState.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:
@@ -824,9 +828,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 = ccState.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 = ccState.currentLevel), curEnv)
         case _ =>
       val res =
         try
@@ -990,7 +994,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 = ccState.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):
 

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

@@ -410,14 +410,17 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if isExcluded(meth) then
             return
 
-          inContext(ctx.withOwner(meth)):
-            paramss.foreach(traverse)
-            transformResultType(tpt, meth)
-            traverse(tree.rhs)
-            //println(i"TYPE of ${tree.symbol.showLocated} = ${tpt.knownType}")
+          ccState.recordLevel(meth)
+          ccState.inNestedLevel:
+            inContext(ctx.withOwner(meth)):
+              paramss.foreach(traverse)
+              transformResultType(tpt, meth)
+              traverse(tree.rhs)
+              //println(i"TYPE of ${tree.symbol.showLocated} = ${tpt.knownType}")
 
         case tree @ ValDef(_, tpt: TypeTree, _) =>
           val sym = tree.symbol
+          ccState.recordLevel(sym)
           val defCtx = if sym.isOneOf(TermParamOrAccessor) then ctx else ctx.withOwner(sym)
           inContext(defCtx):
             transformResultType(tpt, sym)
@@ -434,13 +437,17 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 transformTT(arg, boxed = true, exact = false) // type arguments in type applications are boxed
 
         case tree: TypeDef if tree.symbol.isClass =>
+          ccState.recordLevel(tree.symbol)
           inContext(ctx.withOwner(tree.symbol)):
             traverseChildren(tree)
 
         case tree @ SeqLiteral(elems, tpt: TypeTree) =>
           traverse(elems)
           tpt.rememberType(box(transformInferredType(tpt.tpe)))
 
+        case tree: Block =>
+          ccState.inNestedLevel(traverseChildren(tree))
+
         case _ =>
           traverseChildren(tree)
       postProcess(tree)
@@ -556,7 +563,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 // Infer the self type for the rest, which is all classes without explicit
                 // self types (to which we also add nested module classes), provided they are
                 // neither pure, nor are publicily extensible with an unconstrained self type.
-                CapturingType(cinfo.selfType, CaptureSet.Var(cls))
+                CapturingType(cinfo.selfType, CaptureSet.Var(cls, level = ccState.currentLevel))
             val ps1 = inContext(ctx.withOwner(cls)):
               ps.mapConserve(transformExplicitType(_))
             if (selfInfo1 ne selfInfo) || (ps1 ne ps) then
@@ -680,11 +687,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
   /** Add a capture set variable to `tp` if necessary, or maybe pull out
    *  an embedded capture set variable from a part of `tp`.
    */
-  def addVar(tp: Type, owner: Symbol)(using Context): Type =
+  private def addVar(tp: Type, owner: Symbol)(using Context): Type =
     decorate(tp,
       addedSet = _.dealias.match
-        case CapturingType(_, refs) => CaptureSet.Var(owner, refs.elems)
-        case _ => CaptureSet.Var(owner))
+        case CapturingType(_, refs) => CaptureSet.Var(owner, refs.elems, level = ccState.currentLevel)
+        case _ => CaptureSet.Var(owner, level = ccState.currentLevel))
 
   def setupUnit(tree: Tree, recheckDef: DefRecheck)(using Context): Unit =
     setupTraverser(recheckDef).traverse(tree)(using ctx.withPhase(thisPhase))

compiler/src/dotty/tools/dotc/transform/Recheck.scala

@@ -266,7 +266,7 @@ abstract class Recheck extends Phase, SymTransformer:
 
     def recheckClassDef(tree: TypeDef, impl: Template, sym: ClassSymbol)(using Context): Type =
       recheck(impl.constr)
-      impl.parentsOrDerived.foreach(recheck(_))
+      impl.parents.foreach(recheck(_))
       recheck(impl.self)
       recheckStats(impl.body)
       sym.typeRef