Rename caps.cap to caps.any

[odersky]

• Internally rename FreshCap to LocalCap

• Introduce fresh

  • New global definition: caps.fresh.
  • fresh is for ResultCaps in function types.
  • Disallow fresh outside result types of function types.

• Fix isTrackableRef: previously, a static term ref was trackable if its prefix was the ThisType
  of a package, but was not trackable if the prefix was a TermRef to the same package.
  Now both versions are trackable.

• Don't go to basetypes when comparing dependent functions at cc

• Improve printing of capabilities:

  • Don't elide a universal capture set in a TypeMismatch message if one of its capabilities is mentioned
    in an error note.
  • Don't elide capture sets containing fresh when printing
  • Don't use the verbose output for fresh if there are no open existentials
  • Systematically backquote all entities shown as capabilities

[SethTisue]

(fyi @nrinaudo, who iirc might have suggested the name change?)

[bracevac]

@bjornregnell

[odersky]

any was a result of a discussion with @bjornregnell. The first suggestion was anyCapability but then we felt it safe to abbreviate to just any. any can only used in capture sets such as C^{any}, so it's clear from the context that it is a capability.

[bjornregnell]

Yes, I think any is much less cryptic and unabiguous than cap and says what it is more directly. I observed in the talks about capabilities that the speakers always had to phrase an explanation of cap in terms of a "root" capability or similar that actually refers to any capability so I think this is a great improvement.

[nrinaudo]

Oh thank god, I had no recollection of suggesting this and was wondering if my mind was finally starting to go.

[nrinaudo]

Yes, I think any is much less cryptic and unabiguous than cap and says what it is more directly. I observed in the talks about capabilities that the speakers always had to phrase an explanation of cap in terms of a "root" capability or similar that actually refers to any capability so I think this is a great improvement.

This might not be the place for this question, feel free to let me know if it's not, but: how is that going to interact with there being multiple root capabilities? Are we going to have error messages like any^1 and any^2 refer to any capabilities, but not necessarily the same ?

[bjornregnell]

Oh thank god, I had no recollection of suggesting this and was wondering if my mind was finally starting to go.

I'm the guilty one :)

BTW: many thanks for your efforts in providing pedagogical and down-to-earth explanations of the practical usage of capabilities and capture checking! @nrinaudo

[nrinaudo]

BTW: many thanks for your efforts in providing pedagogical and down-to-earth explanations of the practical usage of capabilities and capture checking! @nrinaudo

Yeah well now I have to go and fix all of them to use any rather than cap, don't I? :)

You're quite welcome - it's mostly how I learn, by explaining things to others and exposing holes in my understanding that I need to fix.

[bjornregnell]

Yes, I think any is much less cryptic and unabiguous than cap and says what it is more directly. I observed in the talks about capabilities that the speakers always had to phrase an explanation of cap in terms of a "root" capability or similar that actually refers to any capability so I think this is a great improvement.

This might not be the place for this question, feel free to let me know if it's not, but: how is that going to interact with there being multiple root capabilities? Are we going to have error messages like any^1 and any^2 refer to any capabilities, but not necessarily the same ?

I guess, esp. for improving error messages etc there needs to be a way to talk about different subsets of any. Helping the user of capture checking to understand the implications of the checking rules via error messages is really important, but can also be challenging as the theory includes concepts that may seem esoteric to a beginner. Any suggestions on good feedback from the compiler in diagnostics, errors and warnings is helpful.

[odersky]

I guess, esp. for improving error messages etc there needs to be a way to talk about different subsets of any. Helping the user of capture checking to understand the implications of the checking rules via error messages is really important, but can also be challenging as the theory includes concepts that may seem esoteric to a beginner. Any suggestions on good feedback from the compiler in diagnostics, errors and warnings is helpful.

What we do now:

• If there are several any or fresh occurrences to different capabilities, they get subscripts.
• We have a "where" clause that explains what these capabilities are and where they come from.
• We avoid referring to the same capability in different ways. I.e. if we have A => B and a separate note that mentions the any to which => expands, we avoid A => B and print A ->{any} B instead.