@@ -98,10 +98,14 @@ extension (tree: Tree)
9898 tree.putAttachment(Captures , refs)
9999 refs
100100
101- /** The arguments of a @retains or @retainsByName annotation */
101+ /** The arguments of a @retains, @retainsCap or @retainsByName annotation */
102102 def retainedElems (using Context ): List [Tree ] = tree match
103- case Apply (_, Typed (SeqLiteral (elems, _), _) :: Nil ) => elems
104- case _ => Nil
103+ case Apply (_, Typed (SeqLiteral (elems, _), _) :: Nil ) =>
104+ elems
105+ case _ =>
106+ if tree.symbol.maybeOwner == defn.RetainsCapAnnot
107+ then ref(defn.captureRoot.termRef) :: Nil
108+ else Nil
105109
106110extension (tp : Type )
107111
@@ -207,7 +211,7 @@ extension (tp: Type)
207211 def dropAllRetains (using Context ): Type = // TODO we should drop retains from inferred types before unpickling
208212 val tm = new TypeMap :
209213 def apply (t : Type ) = t match
210- case AnnotatedType (parent, annot) if annot.symbol == defn. RetainsAnnot =>
214+ case AnnotatedType (parent, annot) if annot.symbol.isRetains =>
211215 apply(parent)
212216 case _ =>
213217 mapOver(t)
@@ -220,9 +224,31 @@ extension (tp: Type)
220224 * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
221225 * are unrelated.
222226 */
223- def reach (using Context ): CaptureRef =
224- assert(tp.isTrackableRef)
225- AnnotatedType (tp, Annotation (defn.ReachCapabilityAnnot , util.Spans .NoSpan ))
227+ def reach (using Context ): CaptureRef = tp match
228+ case tp : CaptureRef if tp.isTrackableRef =>
229+ if tp.isReach then tp else ReachCapability (tp)
230+
231+ /** If `x` is a capture ref, its maybe capability `x?`, represented internally
232+ * as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
233+ * not be part of a capture set. We have `{} <: {x?} <: {x}`. Maybe capabilities
234+ * cannot be propagated between sets. If `a <: b` and `a` acquires `x?` then
235+ * `x` is propagated to `b` as a conservative approximation.
236+ *
237+ * Maybe capabilities should only arise for capture sets that appear in invariant
238+ * position in their surrounding type. They are similar to TypeBunds types, but
239+ * restricted to capture sets. For instance,
240+ *
241+ * Array[C^{x?}]
242+ *
243+ * should be morally equivalent to
244+ *
245+ * Array[_ >: C^{} <: C^{x}]
246+ *
247+ * but it has fewer issues with type inference.
248+ */
249+ def maybe (using Context ): CaptureRef = tp match
250+ case tp : CaptureRef if tp.isTrackableRef =>
251+ if tp.isMaybe then tp else MaybeCapability (tp)
226252
227253 /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
228254 * universal capture set, replace all these occurrences by `{ref*}`. This implements
@@ -326,6 +352,14 @@ extension (cls: ClassSymbol)
326352
327353extension (sym : Symbol )
328354
355+ /** This symbol is one of `retains` or `retainsCap` */
356+ def isRetains (using Context ): Boolean =
357+ sym == defn.RetainsAnnot || sym == defn.RetainsCapAnnot
358+
359+ /** This symbol is one of `retains`, `retainsCap`, or`retainsByName` */
360+ def isRetainsLike (using Context ): Boolean =
361+ isRetains || sym == defn.RetainsByNameAnnot
362+
329363 /** A class is pure if:
330364 * - one its base types has an explicitly declared self type with an empty capture set
331365 * - or it is a value class
@@ -419,12 +453,21 @@ object ReachCapabilityApply:
419453 case Apply (reach, arg :: Nil ) if reach.symbol == defn.Caps_reachCapability => Some (arg)
420454 case _ => None
421455
456+ class AnnotatedCapability (annot : Context ?=> ClassSymbol ):
457+ def apply (tp : Type )(using Context ) =
458+ AnnotatedType (tp, Annotation (annot, util.Spans .NoSpan ))
459+ def unapply (tree : AnnotatedType )(using Context ): Option [SingletonCaptureRef ] = tree match
460+ case AnnotatedType (parent : SingletonCaptureRef , ann) if ann.symbol == annot => Some (parent)
461+ case _ => None
462+
422463/** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
423464 * the reach capability `ref*` as a type.
424465 */
425- object ReachCapability :
426- def unapply (tree : AnnotatedType )(using Context ): Option [SingletonCaptureRef ] = tree match
427- case AnnotatedType (parent : SingletonCaptureRef , ann)
428- if ann.symbol == defn.ReachCapabilityAnnot => Some (parent)
429- case _ => None
466+ object ReachCapability extends AnnotatedCapability (defn.ReachCapabilityAnnot )
467+
468+ /** An extractor for `ref @maybeCapability`, which is used to express
469+ * the maybe capability `ref?` as a type.
470+ */
471+ object MaybeCapability extends AnnotatedCapability (defn.MaybeCapabilityAnnot )
472+
430473
0 commit comments