@@ -388,6 +388,52 @@ class CheckCaptures extends Recheck, SymTransformer:
388388 |To allow this, the ${ref.symbol} should be declared with a @use annotation """ , pos)
389389 case _ =>
390390
391+ /** Avoid locally defined capability by charging the underlying type
392+ * (which may not be cap). This scheme applies only under the deferredReaches setting.
393+ */
394+ def avoidLocalCapability (c : CaptureRef , env : Env , lastEnv : Env | Null ): Unit =
395+ if c.isParamPath then
396+ c match
397+ case ReachCapability (_) | _ : TypeRef =>
398+ checkUseDeclared(c, env, lastEnv)
399+ case _ =>
400+ else
401+ val underlying = c match
402+ case ReachCapability (c1) =>
403+ CaptureSet .ofTypeDeeply(c1.widen)
404+ case _ =>
405+ CaptureSet .ofType(c.widen, followResult = false )
406+ capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
407+ underlying.disallowRootCapability: () =>
408+ report.error(em " Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set " , pos)
409+ recur(underlying, env, lastEnv)
410+
411+ /** Avoid locally defined capability if it is a reach capability or capture set
412+ * parameter. This is the default.
413+ */
414+ def avoidLocalReachCapability (c : CaptureRef , env : Env ): Unit = c match
415+ case ReachCapability (c1) =>
416+ if c1.isParamPath then
417+ checkUseDeclared(c, env, null )
418+ else
419+ // When a reach capabilty x* where `x` is not a parameter goes out
420+ // of scope, we need to continue with `x`'s underlying deep capture set.
421+ // It is an error if that set contains cap.
422+ // The same is not an issue for normal capabilities since in a local
423+ // definition `val x = e`, the capabilities of `e` have already been charged.
424+ // Note: It's not true that the underlying capture set of a reach capability
425+ // is always cap. Reach capabilities over paths depend on the prefix, which
426+ // might turn a cap into something else.
427+ // The path-use.scala neg test contains an example.
428+ val underlying = CaptureSet .ofTypeDeeply(c1.widen)
429+ capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
430+ underlying.disallowRootCapability: () =>
431+ report.error(em " Local reach capability $c leaks into capture scope of ${env.ownerString}" , pos)
432+ recur(underlying, env, null )
433+ case c : TypeRef if c.isParamPath =>
434+ checkUseDeclared(c, env, null )
435+ case _ =>
436+
391437 def recur (cs : CaptureSet , env : Env , lastEnv : Env | Null ): Unit =
392438 if env.isOpen && ! env.owner.isStaticOwner && ! cs.isAlwaysEmpty then
393439 // Only captured references that are visible from the environment
@@ -399,45 +445,9 @@ class CheckCaptures extends Recheck, SymTransformer:
399445 case ref =>
400446 false
401447 if ! isVisible then
402- // println(i"out of scope: $c")
403- if ccConfig.deferredReaches then // avoid all locally bound capabilities
404- if c.isParamPath then
405- c match
406- case ReachCapability (_) | _ : TypeRef =>
407- checkUseDeclared(c, env, lastEnv)
408- case _ =>
409- else
410- val underlying = c match
411- case ReachCapability (c1) =>
412- CaptureSet .ofTypeDeeply(c1.widen)
413- case _ =>
414- CaptureSet .ofType(c.widen, followResult = false )
415- capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
416- underlying.disallowRootCapability: () =>
417- report.error(em " Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set " , pos)
418- recur(underlying, env, lastEnv)
419- else c match // avoid only reach capabilities and capture sets
420- case ReachCapability (c1) =>
421- if c1.isParamPath then
422- checkUseDeclared(c, env, lastEnv)
423- else
424- // When a reach capabilty x* where `x` is not a parameter goes out
425- // of scope, we need to continue with `x`'s underlying deep capture set.
426- // It is an error if that set contains cap.
427- // The same is not an issue for normal capabilities since in a local
428- // definition `val x = e`, the capabilities of `e` have already been charged.
429- // Note: It's not true that the underlying capture set of a reach capability
430- // is always cap. Reach capabilities over paths depend on the prefix, which
431- // might turn a cap into something else.
432- // The path-use.scala neg test contains an example.
433- val underlying = CaptureSet .ofTypeDeeply(c1.widen)
434- capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
435- underlying.disallowRootCapability: () =>
436- report.error(em " Local reach capability $c leaks into capture scope of ${env.ownerString}" , pos)
437- recur(underlying, env, lastEnv)
438- case c : TypeRef if c.isParamPath =>
439- checkUseDeclared(c, env, lastEnv)
440- case _ =>
448+ if ccConfig.deferredReaches
449+ then avoidLocalCapability(c, env, lastEnv)
450+ else avoidLocalReachCapability(c, env)
441451 isVisible
442452 checkSubset(included, env.captured, pos, provenance(env))
443453 capt.println(i " Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}" )
0 commit comments