Change retains annotation from using term arguments to using type arguments #22909

noti0na1 · 2025-04-02T13:53:05Z

This PR updates the retains annotation to use type arguments instead of term arguments in order to streamline capture set representations and related type checking. Key changes include:

Adjusting the looking up for capture variables in capture sets, by creating dummy term symbols.
Removing term parameter for retains annotation and capsOf.
Modifying annotation construction in RetainingType, CaptureAnnotation, and associated AST desugarings.

For example,

def f[C^](x: A^): B @retains[x.type | C] // B^{x, C}

…uments

odersky

The refactoring of annotations looks all good.

I have doubts about the CaptureParam part, for several reasons. I think we should try to

drop the InCaptureSet mode
Re-use the ConstructorProxy flag (maybe call it Surrogate instead to make clear it serves multiple purposes now)
Set proxy types to NoType at PostTyper
Avoid all special treatments in transforms

odersky · 2025-05-27T09:23:52Z

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

@@ -380,6 +380,8 @@ object Flags {
  /** Tracked modifier for class parameter / a class with some tracked parameters */
  val (Tracked @ _, _, Dependent @ _) = newFlags(46, "tracked")

+  val (CaptureParam @ _, _, _) = newFlags(47, "capture-param")


We don't have many flags left, and a flag in this range would have to be pickled, which means a change in TastyFormat. I think we should just re-use the ConstructorProxy flag, which serves a very similar purpose, and is already thoroughly debugged.

odersky · 2025-05-27T09:26:38Z

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

@@ -748,7 +748,9 @@ object Types extends TypeUtils {
        case tp: ClassInfo => tp.appliedRef
        case _ => widenIfUnstable
      }
-      findMember(name, pre, required, excluded)
+      // The dummy term capture variable can only be found in a capture set.
+      val excluded1 = if ctx.mode.is(Mode.InCaptureSet) then excluded else excluded | CaptureParam


It's an interesting twist, but I am not sure we need the mode either. I believe it would complicate the spec if we had to say that a capability is present as a term name only when we are looking inside a set. Analogously, we'd say a constructor proxy is available as a term name only when we are resolving the function part of an application. We could do that as well, but we don't because it would complicate the spec. I think it's OK to just unconditionally look for capature parameter terms.

Eventually all dummy term symbols will be erased, and I don't want them been found as a regular value and left in the program. For example, in tests/neg-custom-args/captures/check-dummy-symbol.scala

odersky · 2025-05-27T09:27:15Z

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

@@ -196,7 +196,10 @@ class PostTyper extends MacroTransform with InfoTransformer { thisPhase =>
      val saved = inJavaAnnot
      inJavaAnnot = annot.symbol.is(JavaDefined)
      if (inJavaAnnot) checkValidJavaAnnotation(annot)
-      try transform(annot)
+      try
+        val annotCtx = if annot.hasAttachment(untpd.RetainsAnnot)


I wonder why this is necessary. We should not do any name resolution here?

PostTyper will check all singleton types are valid, and we want to treat singletons like f: => T specially in capture set.

ok I see now

odersky · 2025-05-27T09:28:30Z

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

@@ -89,7 +89,7 @@ class Getters extends MiniPhase with SymTransformer { thisPhase =>
      else d1 = d1.copySymDenotation(initFlags = d1.flags &~ Local)
    d1
  }
-  private val NoGetterNeededFlags = Method | Param | JavaDefined | JavaStatic
+  private val NoGetterNeededFlags = Method | Param | JavaDefined | JavaStatic | CaptureParam


Is this necessary? We should not even see capture parameters at this point. Maybe hide them in PostTyper as is done in #23269.

Agree, we should remove these special symbols right after typer, then maybe we don't all the special handling later.

bracevac · 2025-05-27T12:46:00Z

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

@@ -801,7 +801,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
      case CapturingType(_, refs) =>
        !refs.isAlwaysEmpty
      case RetainingType(parent, refs) =>
-        !refs.isEmpty
+        !refs.retainedElements.isEmpty


I'm wondering if we should massage the RetainingType extractor to directly expose refs as the retainedElements set? Isn't this what we want 99% of the time anyways?

RetainingType is designed to work only on type level, without additional processing and check. There is a place we only check what annotation it is and pass refs back directly, and there are places we don't want illegal capture reference exception, like checking well forming in typer and printing.

bracevac · 2025-05-27T12:51:09Z

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

@@ -1330,8 +1326,8 @@ class Definitions {
   */
  object ByNameFunction:
    def apply(tp: Type)(using Context): Type = tp match
-      case tp @ RetainingType(tp1, refs) if tp.annot.symbol == RetainsByNameAnnot =>
-        RetainingType(apply(tp1), refs)
+      case tp @ RetainingType(tp1, refSet) if tp.annot.symbol == RetainsByNameAnnot =>


Are RetainingTypes corresponding to what we in the papers on capture checking refer to as CapturingTypes? If yes, let's rename it (same rationale as refactoring CaptureRef to Capability).

I'm not sure I understand the comment. RetainingType is just a "CapturingType" living outside the cc phase.

The point is to find a better name. Just looking at it, the name tells me nothing. And if it's something that corresponds to the terminology in the calculus, then we should name it as such. Or at the very least, it should be a name that would tell us it's capture-checking related.

It's RetainingType since it's of the form T @retains U.

Same thing with @retains: is this truly the best name for what it stands for? Why not, e.g., T @captures U, T @capturing U, etc. ?

I don't mind if there is a better name. Since it's an internal temporary type holder not related to the core calculus, users wouldn't see it, and most of cc logic wouldn't see it neither, the name is just not important here. Using a special name also makes it easy to tell a type is newly coming to cc phase.

bracevac · 2025-05-27T12:59:47Z

tests/neg-custom-args/captures/capset-members-nohat.scala

@@ -2,7 +2,7 @@ import language.experimental.captureChecking
 import caps.*

 trait Abstract[X^]:
-  type C >: {X}
+  type C^ >: {X}


As the name of the file suggests, the point of this test is to check if we can omit the hat. I know we discussed that there are situations that cause trouble like C >: A <: B, but here (and also the other test cases) I don't quite see why it's strictly necessary to re-add the hat.

bracevac · 2025-05-27T13:03:21Z

tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala

@@ -8,6 +8,8 @@ import annotation.tailrec
 import caps.cap
 import caps.unsafe.unsafeAssumeSeparate

+import language.experimental.captureChecking


Maybe just uniformly add this import to all tests in the captures test folders? It's annoying to not have it during manual debugging.

bracevac

Some smaller comments. LGTM otherwise. I'll leave the final approval to Martin.

noti0na1 force-pushed the change-retains branch from 6009cce to b344155 Compare May 15, 2025 20:27

noti0na1 marked this pull request as ready for review May 15, 2025 20:28

noti0na1 self-assigned this May 15, 2025

noti0na1 requested a review from Copilot May 15, 2025 20:28

This comment was marked as resolved.

Sign in to view

noti0na1 force-pushed the change-retains branch from 51d6a8e to 7b3b063 Compare May 19, 2025 12:48

noti0na1 mentioned this pull request May 20, 2025

Pickling test crash on widened SkolemTypes inside annotation type arguments #23194

Closed

noti0na1 added 2 commits May 26, 2025 02:19

Change retains annotation from using term arguments to using type arg…

9d7fd0e

…uments

Update extractors

565e001

noti0na1 force-pushed the change-retains branch from 75f5c78 to 565e001 Compare May 26, 2025 00:22

Bring Mayby back

085df3d

noti0na1 requested a review from Copilot May 26, 2025 03:19

This comment was marked as resolved.

Sign in to view

noti0na1 added 2 commits May 26, 2025 13:11

Cleanup code

6893878

Add more comments

ff629f2

noti0na1 requested review from odersky and bracevac May 26, 2025 11:32

noti0na1 assigned odersky and unassigned noti0na1 May 26, 2025

odersky requested changes May 27, 2025

View reviewed changes

bracevac reviewed May 27, 2025

View reviewed changes

bracevac requested changes May 27, 2025

View reviewed changes

natsukagami mentioned this pull request May 28, 2025

Add @retainsArg to read-only and reach capabilities #23238

Open

Change retains annotation from using term arguments to using type arguments #22909

Are you sure you want to change the base?

Change retains annotation from using term arguments to using type arguments #22909

Uh oh!

Conversation

noti0na1 commented Apr 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

odersky left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

noti0na1 May 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

noti0na1 May 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bracevac left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

noti0na1 commented Apr 2, 2025 •

edited

Loading

noti0na1 May 27, 2025 •

edited

Loading

noti0na1 May 27, 2025 •

edited

Loading