Add reach capabilities

This adds reach capabilities x* as described in the proposal.

Author: odersky

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

@@ -166,7 +166,7 @@ extension (tp: Type)
   def forceBoxStatus(boxed: Boolean)(using Context): Type = tp.widenDealias match
     case tp @ CapturingType(parent, refs) if tp.isBoxed != boxed =>
       val refs1 = tp match
-        case ref: CaptureRef if ref.isTracked => ref.singletonCaptureSet
+        case ref: CaptureRef if ref.isTracked || ref.isReach => ref.singletonCaptureSet
         case _ => refs
       CapturingType(parent, refs1, boxed)
     case _ =>
@@ -222,6 +222,52 @@ extension (tp: Type)
           mapOver(t)
     tm(tp)
 
+  /** If `x` is a capture ref, its reach capability `x*`, represented internally
+   *  as `x.$reach`. `x*` stands for all capabilities reachable through `x`".
+   *  We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
+   *  is the union of all capture sets that appear in covariant position in the
+   *  type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
+   *  are unrelated.
+   */
+  def reach(using Context): TermRef =
+    assert(tp.isTrackableRef)
+    TermRef(tp, nme.CC_REACH, defn.Any_ccReach)
+
+  /** If `ref` is a trackable capture ref, replace all covariant occurrences of a
+   *  universal capture set in `tp` by `{ref*}`. This implements the new aspect of
+   *  the (Var) rule, which can now be stated as follows:
+   *
+   *     x: T in E
+   *     -----------
+   *     E |- x: T'
+   *
+   *  where T' is T with (1) the toplevel capture set replaced by `{x}` and
+   *  (2) all covariant occurrences of cap replaced by `x*`. (1) is standard,
+   *  whereas (2) is new.
+   *
+   *  Why is this sound? Covariant occurrences of cap must represent capabilities
+   *  that are reachable from `x`, so they are included in the meaning of `{x*}`.
+   *  At the same time, encapsulation is still maintained since no covariant
+   *  occurrences of cap are allowed in instance types of type variables.
+   */
+  def withReachCaptures(ref: Type)(using Context): Type =
+    val narrowCaps = new TypeMap:
+      def apply(t: Type) = t.dealias match
+        case t1 @ CapturingType(p, cs) if cs.isUniversal && variance > 0 =>
+          t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
+        case _ => t match
+          case t @ CapturingType(p, cs) =>
+            t.derivedCapturingType(apply(p), cs) // don't map capture set variables
+          case t =>
+            mapOver(t)
+    ref match
+      case ref: CaptureRef if ref.isTrackableRef =>
+        val tp1 = narrowCaps(tp)
+        if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
+        tp1
+      case _ =>
+        tp
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =

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

@@ -156,17 +156,24 @@ sealed abstract class CaptureSet extends Showable:
 
   extension (x: CaptureRef)(using Context)
 
-    /* x subsumes y if one of the following is true:
-    *   - x is the same as y,
-    *   - x is a this reference and y refers to a field of x
-    *   - x is a super root of y
+    /** x subsumes x
+    *   this subsumes this.f
+    *   x subsumes y  ==>  x* subsumes y
+    *   x subsumes y  ==>  x* subsumes y*
     */
-    private def subsumes(y: CaptureRef) =
+    private def subsumes(y: CaptureRef): Boolean =
       (x eq y)
       || x.isSuperRootOf(y)
       || y.match
-          case y: TermRef => y.prefix eq x
+          case y: TermRef => !y.isReach && (y.prefix eq x)
           case _ => false
+      || x.match
+          case x: TermRef if x.isReach =>
+            y.match
+              case y: TermRef if y.isReach => x.reachPrefix.subsumes(y.reachPrefix)
+              case _ => x.reachPrefix.subsumes(y)
+          case _ =>
+            false
 
     /** x <:< cap,   cap[x] <:< cap
      *  cap[y] <:< cap[x] if y encloses x
@@ -530,7 +537,8 @@ object CaptureSet:
       if elem.isUniversalRootCapability then !noUniversal
       else elem match
         case elem: TermRef =>
-          if levelLimit.exists then
+          if elem.isReach then levelOK(elem.reachPrefix)
+          else if levelLimit.exists then
             var sym = elem.symbol
             if sym.isLevelOwner then sym = sym.owner
             levelLimit.isContainedIn(sym.levelOwner)
@@ -1037,6 +1045,8 @@ object CaptureSet:
   /** The capture set of the type underlying CaptureRef */
   def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
     case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
+    case ref: TermRef if ref.isReach => deepCaptureSet(ref.prefix.widen)
+      .showing(i"Deep capture set of $ref: ${ref.prefix.widen} = $result", capt)
     case _ => ofType(ref.underlying, followResult = true)
 
   /** Capture set of a type */
@@ -1078,6 +1088,16 @@ object CaptureSet:
     recur(tp)
       .showing(i"capture set of $tp = $result", captDebug)
 
+  private def deepCaptureSet(tp: Type)(using Context): CaptureSet =
+    val collect = new TypeAccumulator[CaptureSet]:
+      def apply(cs: CaptureSet, t: Type) = t.dealias match
+        case t @ CapturingType(p, cs1) =>
+          val cs2 = apply(cs, p)
+          if variance > 0 then cs2 ++ cs1 else cs2
+        case _ =>
+          foldOver(cs, t)
+    collect(CaptureSet.empty, tp)
+
   private val ShownVars: Property.Key[mutable.Set[Var]] = Property.Key()
 
   /** Perform `op`. Under -Ycc-debug, collect and print info about all variables reachable

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

@@ -1152,7 +1152,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                   // given `a: T^C`, improve `T^C` to `T^{a}`
               case _ =>
           case _ =>
-        val adapted = adapt(actualw, expected, covariant = true)
+        val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
         if adapted ne actualw then
           capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
           adapted

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

@@ -333,15 +333,17 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
     def apply(t: Type): Type = t match
       case t: NamedType =>
-        val sym = t.symbol
-        def outer(froms: List[List[Symbol]], tos: List[LambdaType]): Type =
-          def inner(from: List[Symbol], to: List[ParamRef]): Type =
-            if from.isEmpty then outer(froms.tail, tos.tail)
-            else if sym eq from.head then to.head
-            else inner(from.tail, to.tail)
-          if tos.isEmpty then t
-          else inner(froms.head, tos.head.paramRefs)
-        outer(from, to)
+        if t.prefix == NoPrefix then
+          val sym = t.symbol
+          def outer(froms: List[List[Symbol]], tos: List[LambdaType]): Type =
+            def inner(from: List[Symbol], to: List[ParamRef]): Type =
+              if from.isEmpty then outer(froms.tail, tos.tail)
+              else if sym eq from.head then to.head
+              else inner(from.tail, to.tail)
+            if tos.isEmpty then t
+            else inner(froms.head, tos.head.paramRefs)
+          outer(from, to)
+        else t.derivedSelect(apply(t.prefix))
       case _ =>
         mapOver(t)
 

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -304,6 +304,15 @@ class Definitions {
     @tu lazy val Any_typeCast: TermSymbol     = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOfPM, _.paramRefs(0), Final | SyntheticArtifact | StableRealizable)
       // generated by pattern matcher and explicit nulls, eliminated by erasure
 
+    @tu lazy val Any_ccReach =
+      newPermanentSymbol(AnyClass, nme.CC_REACH, Final | SyntheticArtifact | StableRealizable,
+          info = new LazyType:
+            def complete(denot: SymDenotation)(using Context): Unit =
+              denot.info = Caps_Cap.typeRef
+        ).entered
+      // The internal representation of a reach capability `x*` is `x.$reach`.
+      // See doc comment in CaptureOps.reach for more info on reach capabilities
+
     /** def getClass[A >: this.type](): Class[? <: A] */
     @tu lazy val Any_getClass: TermSymbol =
         enterPolyMethod(
@@ -313,7 +322,8 @@ class Definitions {
           bounds = TypeBounds.lower(AnyClass.thisType))
 
     def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
-      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast)
+      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest,
+      Any_typeCast, Any_ccReach)
 
   @tu lazy val ObjectClass: ClassSymbol = {
     val cls = requiredClass("java.lang.Object")

compiler/src/dotty/tools/dotc/core/StdNames.scala

@@ -120,6 +120,7 @@ object StdNames {
     val BITMAP_TRANSIENT: N           = s"${BITMAP_PREFIX}trans$$"    // initialization bitmap for transient lazy vals
     val BITMAP_CHECKINIT: N           = s"${BITMAP_PREFIX}init$$"      // initialization bitmap for checkinit values
     val BITMAP_CHECKINIT_TRANSIENT: N = s"${BITMAP_PREFIX}inittrans$$" // initialization bitmap for transient checkinit values
+    val CC_REACH: N                   = "$reach"
     val DEFAULT_GETTER: N             = str.DEFAULT_GETTER
     val DEFAULT_GETTER_INIT: N        = "$lessinit$greater"
     val DO_WHILE_PREFIX: N            = "doWhile$"

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -991,11 +991,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
 
         def tp1widened =
           val tp1w = tp1.underlying.widenExpr
-          tp1 match
-            case tp1: CaptureRef if isCaptureCheckingOrSetup && tp1.isTracked =>
-              CapturingType(tp1w.stripCapturing, tp1.singletonCaptureSet)
-            case _ =>
-              tp1w
+          if isCaptureCheckingOrSetup then
+            tp1
+              .match
+                case tp1: CaptureRef if tp1.isTracked =>
+                  CapturingType(tp1w.stripCapturing, tp1.singletonCaptureSet)
+                case _ =>
+                  tp1w
+              .withReachCaptures(tp1)
+          else tp1w
 
         comparePaths || isSubType(tp1widened, tp2, approx.addLow)
       case tp1: RefinedType =>

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -2174,6 +2174,9 @@ object Types {
     final def isTracked(using Context): Boolean =
       isTrackableRef && (isRootCapability || !captureSetOfInfo.isAlwaysEmpty)
 
+    /** Is this a reach reference of the form `x*`? */
+    def isReach(using Context): Boolean = false // overridden in TermRef
+
     /** Is this reference the generic root capability `cap` ? */
     def isUniversalRootCapability(using Context): Boolean = false
 
@@ -2918,8 +2921,14 @@ object Types {
       ((prefix eq NoPrefix)
       || symbol.is(ParamAccessor) && (prefix eq symbol.owner.thisType)
       || isRootCapability
+      || isReach
       ) && !symbol.isOneOf(UnstableValueFlags)
 
+    override def isReach(using Context): Boolean =
+      name == nme.CC_REACH && symbol == defn.Any_ccReach
+
+    def reachPrefix: CaptureRef = prefix.asInstanceOf[CaptureRef]
+
     override def isUniversalRootCapability(using Context): Boolean =
       name == nme.CAPTURE_ROOT && symbol == defn.captureRoot
 
@@ -2930,7 +2939,9 @@ object Types {
       if name == nme.LOCAL_CAPTURE_ROOT then normOwner else NoSymbol
 
     override def normalizedRef(using Context): CaptureRef =
-      if isTrackableRef then symbol.termRef else this
+      if isReach then TermRef(reachPrefix.normalizedRef, name, denot)
+      else if isTrackableRef then symbol.termRef
+      else this
   }
 
   abstract case class TypeRef(override val prefix: Type,

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -1476,6 +1476,7 @@ object Parsers {
       if in.token == THIS then simpleRef()
       else termIdent() match
         case id @ Ident(nme.CAPTURE_ROOT) =>
+          // TODO drop
           if in.token == LBRACKET then
             val ref = atSpan(id.span.start)(captureRootIn)
             val qual =
@@ -1486,7 +1487,11 @@ object Parsers {
           else
             atSpan(id.span.start)(captureRoot)
         case id =>
-          id
+          if isIdent(nme.raw.STAR) then
+            in.nextToken()
+            atSpan(startOffset(id)):
+              Select(id, nme.CC_REACH)
+          else id
 
     /**  CaptureSet ::=  `{` CaptureRef {`,` CaptureRef} `}`    -- under captureChecking
      */

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -168,7 +168,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
       toText(ref)
 
   private def toTextRetainedElems[T <: Untyped](refs: List[Tree[T]]): Text =
-    "{" ~ Text(refs.map(ref => toTextRetainedElem(ref))) ~ "}"
+    "{" ~ Text(refs.map(ref => toTextRetainedElem(ref)), ", ") ~ "}"
 
   /** Print capturing type, overridden in RefinedPrinter to account for
    *  capturing function types.
@@ -393,7 +393,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp: TermRef =>
         if tp.symbol.name == nme.LOCAL_CAPTURE_ROOT then  // TODO: Move to toTextCaptureRef
           Str(s"cap[${nameString(tp.localRootOwner)}]")
-        else toTextPrefixOf(tp) ~ selectionString(tp)
+        else if tp.isReach then
+          toTextRef(tp.reachPrefix) ~ "*"
+        else
+          toTextPrefixOf(tp) ~ selectionString(tp)
       case tp: ThisType =>
         nameString(tp.cls) + ".this"
       case SuperType(thistpe: SingletonType, _) =>

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

@@ -328,7 +328,9 @@ abstract class Recheck extends Phase, SymTransformer:
           assert(false, i"unexpected type of ${tree.fun}: $tp")
 
     def recheckTypeApply(tree: TypeApply, pt: Type)(using Context): Type =
-      recheck(tree.fun).widen match
+      val funtpe = recheck(tree.fun)
+      tree.fun.rememberType(funtpe) // remember type to support later bounds checks
+      funtpe.widen match
         case fntpe: PolyType =>
           assert(fntpe.paramInfos.hasSameLengthAs(tree.args))
           val argTypes = tree.args.map(recheck(_))

docs/_docs/internals/cc/alternatives-to-sealed.md

@@ -25,11 +25,14 @@ A capture checking variant
 - Why is this sound? Covariant occurrences of cap must represent capabilities that are reachable from `x`, so they are included in the meaning of `{x*}`. At the same time, encapsulation is still maintained since no covariant occurrences of cap are allowed in instance types of
 type variables.
 
-Examples:
+## Examples:
 
+Assume
 ```scala
+type Proc = () => Unit
+
 class Ref[T](init: T):
-  private var x: T
+  private var x: T = init
   def get: T = x
   def set(y: T) = { x = y }
 ```
@@ -50,7 +53,7 @@ def runAll(xs: List[Proc]): Unit =
 Same with refs:
 ```scala
 def runAll(xs: List[Proc]): Unit =
-  val cur = Ref[List[Proc]](xs: List[() ->{xs*} Unit]) // error, illegal type for type argument to Ref
+  val cur = Ref[List[Proc]](xs) // error, illegal type for type argument to Ref
   while cur.get.nonEmpty do
     val next: () => Unit = cur.get.head
     next()
@@ -161,7 +164,7 @@ Work items:
       and asSeenFrom work out of the box.
     - subcapturing: `x <:< x* <: dcs(x)`.
     - Narrowing code: in `adaptBoxed` where `x.type` gets widened to `T^{x}`, also
-      do the covariant `cap` to `x*` replacement.
+      do the covariant `cap` to `x*` replacement. Similarly in `fourthTry` of `TypeComparer`.
  - Drop local roots
  - Make all type paraneters sealed
 

tests/neg-custom-args/captures/lazyref.check

@@ -8,21 +8,21 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:21:35 --------------------------------------
 21 |  val ref2c: LazyRef[Int]^{cap2} = ref2 // error
    |                                   ^^^^
-   |                                   Found:    (ref2 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1})
+   |                                   Found:    LazyRef[Int]{val elem: () ->{ref2*} Int}^{ref2}
    |                                   Required: LazyRef[Int]^{cap2}
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:23:35 --------------------------------------
 23 |  val ref3c: LazyRef[Int]^{ref1} = ref3 // error
    |                                   ^^^^
-   |                                   Found:    (ref3 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1})
+   |                                   Found:    LazyRef[Int]{val elem: () ->{ref3*} Int}^{ref3}
    |                                   Required: LazyRef[Int]^{ref1}
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:25:35 --------------------------------------
 25 |  val ref4c: LazyRef[Int]^{cap1} = ref4 // error
    |                                   ^^^^
-   |                                   Found:    (ref4 : LazyRef[Int]{val elem: () => Int}^{cap2, cap1})
+   |                                   Found:    LazyRef[Int]{val elem: () ->{ref4*} Int}^{ref4}
    |                                   Required: LazyRef[Int]^{cap1}
    |
    | longer explanation available when compiling with `-explain`