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