Change retains annotation from using term arguments to using type arguments

[noti0na1]

Fix #22842

This PR updates the retains annotation to use type arguments rather than term arguments, streamlining capture set representations and related type checking. It replaces usages of ConstructorProxy with PhantomSymbol, adjusts annotation construction in several compiler phases, and introduces dummy term capture parameters.

• Updated flag checks and use PhantomSymbol for dummy 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}

[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]

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]

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.

[noti0na1]

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

[noti0na1]

Last week you suggested that we avoid modifying the excluded set, and instead report an error if we encounter a dummy capture term outside the capture set. I did some experimentation, and I don't think this approach will work here.

Unlike constructor proxies, which can shadow outer symbols and produce an error at the use site, we expect term variables and capture variables with the same name to coexist at different levels—and to resolve to different references depending on whether the usage occurs inside or outside the capture set.

def f(C: AnyRef) = // defines a term C
  def g[C^] = // defines a type C and a dummy term C
    // when using C as a type, we should find C from g
    call[C](...)
    // when using C as a term outside capture set, we should find C from f
    call(C)
    // when using C as a term inside capture set, we should find the dummy C from g
    T^{C}

In the second case, with your proposal, we would find the dummy C from g, and we will report an error. But if we still want to find the C from f, we have to add special logic to find* functions, which I think is more complicated than an excluded set.

[odersky]

Whether we shadow or not is a design decision. But note that for constructor proxies there are also cases where we do not shadow:

def C = "hello"
object M:
  class C()
  val x = C

This expands to:

package <empty> {
  final lazy module val M: M = new M()
  final module class M() extends Object() { this: M.type =>
    class C() extends Object() {}
    val x: String = C
  }
  final lazy module val test$package: test$package = new test$package()
  final module class test$package() extends Object() {
    this: test$package.type =>
    def C: String = "hello"
  }
}

We pick the outer C in the definition of x, there's no shadowing. My point is, we should make the mechanisms and specs of constructor proxies and capture parameters as similar as possible. I don't think we need new flags and new clauses in low-level methods like findMember. We seem to already have the mechanisms to do what we want for constructor proxies, let's re-use them for capture parameters.

I had forgotten what the exact behavior of constructor proxies was before. I thought they would always shadow, but it seems it's more subtle than that. (In fact I think I recall now that they originally shadowed but that was revised for better backwards compatibility). But no matter, the point is, however constructor proxies work, capture parameters should work the same way.

[noti0na1]

I think I also misunderstood some rules of constructor proxies before... I'm trying using constructor proxy flag with a new case for capture set, and it seems to work now.

[noti0na1]

ConstructorProxy are renamed to PhantomSymbol now.

[odersky]

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

[noti0na1]

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

[noti0na1]

Since phantom symbols are not removed before erasure, we have to add this during Getters.

[bracevac]

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?

[noti0na1]

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]

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).

[noti0na1]

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

[bracevac]

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.

[odersky]

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

[bracevac]

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. ?

[noti0na1]

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]

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.

[noti0na1]

Due to some issues related to ordering of typing def and symbol creation, we decide to keep all the hats at the definition. We can fix the issue and refine the tests in a separate PR.

[bracevac]

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.