Backport "Separation checking for product types" to 3.7.0 #22964

WojciechMazur · 2025-04-10T12:44:44Z

Backports #22539 to the 3.7.0-RC2.

PR submitted by the release tooling.

When printing a type `C^` where `C` extends `Capability`, don't show the `^`. This is overridden under -Yprint-debug. [Cherry-picked 103ef96]

- Add Mutable trait and mut modifier. - Add dedicated tests `isMutableVar` and `isMutableVarOrAccessor` so that update methods can share the same flag `Mutable` with mutable vars. - Disallow update methods overriding normal methods - Disallow update methods which are not members of classes extending Mutable - Add design document from papers repo to docs/internals - Add readOnly capabilities - Implement raeadOnly access - Check that update methods are only called on references with exclusive capture sets. - Use cap.rd as default capture set of Capability subtypes - Make Mutable a Capability, this means Mutable class references get {cap.rd} as default capture set. - Use {cap} as captu [Cherry-picked 748f4a6]

….toCap If existentials are mapped to fresh, it matters where they are opened. Pure or not arguments don't have anything to do with that. [Cherry-picked e4cc265]

These are represented as Fresh.Cap(hidden) where hidden is the set of capabilities subsumed by a fresh. The underlying representation is as an annotated type `T @annotation.internal.freshCapability`. Require -source `3.7` for caps to be converted to Fresh.Cap Also: - Refacture and document CaputureSet - Make SimpleIdentitySets showable - Refactor VarState - Drop Frozen enum - Make VarState subclasses inner classes of companion object - Rename them - Give implicit parameter VarState of subCapture method a default value - Fix printing of capturesets containing cap and some other capability - Revise handing of @uncheckedAnnotation [Cherry-picked ad11819][modified]

Check separation from source 3.7 on. We currently only check applications, other areas of separation checking are still to be implemented. [Cherry-picked 4c8a50f]

Check that a capability that gets hidden in the (result-)type of some definition is not used afterwards in the same or a nested scope. [Cherry-picked b0c9b3d]

[Cherry-picked 70074c4]

When checking whether two items overlap we should always check their deep capture sets. Buried aliases should count as well. [Cherry-picked 190aaca]

This is necessary since capability sets are IdentitySets. [Cherry-picked 67d42bd]

[Cherry-picked b1da91a]

[Cherry-picked 131f070]

TODO: - check that only @consume parameters flow to @consume parameters [Cherry-picked 3adf4b0]

[Cherry-picked ee23239]

[Cherry-picked a4df033]

Downgrade to -source 3.6 to turn it off. [Cherry-picked 52dc9b4]

[Cherry-picked 824dd83]

[Cherry-picked 7b0b80b]

Allow them only in @consume methods [Cherry-picked 66fc880]

Also: Fixes to computations of overlapWith and -- on Refs that take account of pathss, where shorter paths cover deeper ones. [Cherry-picked 821e17a]

[Cherry-picked 3ed82a3]

[Cherry-picked 2d37938]

[Cherry-picked d661678]

[Cherry-picked 9710872]

This partially reverts commit 7b3d3f4. It looks like this fixes the problems we had with CI timeouts as well. [Cherry-picked 367f66c]

[Cherry-picked 51050f9]

[Cherry-picked f0e0117]

[Cherry-picked 8d15e88]

[Cherry-picked 5132d55]

[Cherry-picked 21a5399]

[Cherry-picked 91eef32]

[Cherry-picked f3ef42b]

Not allowing whitespace clashes with the rules for leading infix operators. For instance, the following does not work, since `->` is not recognized as a leading infix operator. ```scala A ->{x} B ``` Also: Print existential capture set id under -uniqids [Cherry-picked 4c53fd1]

[Cherry-picked 641dffa]

Also, implement infrastructure to add a note to a type mismatch when a failure to subsume occurs. [Cherry-picked 58baf53]

Allows some simplifications in the zoo of classification methods. [Cherry-picked 33ef293]

Allows some simplifications in the zoo of classification methods. [Cherry-picked 12047d8]

[Cherry-picked 399b220]

[Cherry-picked 6093dab]

[Cherry-picked f7484ce]

Exceptions are bracketed in `withCapAsRoot` calls. [Cherry-picked d27f2bb]

TODO: Check that the new error in box-adapt-contra makes sense TODO: error messages need to be improved [Cherry-picked ec8d119]

[Cherry-picked 731c9aa]

1. Strip readonly modifier before checking o=for overlaps 2. Don't reset consume to empty before entering defs [Cherry-picked d89138a]

I believe the timeout was simply that we have to many pos tests, so theior compilation takes more than the limit of 20 minutes. Testing this hypothesis by moving pos-custumargs/captures tests into a separate top-level test posCC [Cherry-picked a6f1ab2]

Deduct explicit refs of actual as opposed to formal argument type. [Cherry-picked d2e276c]

Move extension methods to SepChecks object, drop unused ones. [Cherry-picked f547582]

- Make it peak-based instead of footprint-based - Don't flag rd/rd conflicts between consumed and re-used [Cherry-picked ee60b21]

[Cherry-picked c790007]

[Cherry-picked 9a49c52]

[Cherry-picked d781b3e]

Avoid globally visible vars in CCState. Make sure notes don't leak from one test to another. [Cherry-picked dc0dd7f]

[Cherry-picked fbe37b8]

[Cherry-picked ac84d13]

Intersections used the heuristic mightAccountFor instead of the precise accountsFor. Thsi can lead to a loss of precision and (if unchecked afterwards) also soundness. The fix caused some tests to fail, which involved tracked parameters. We now deal with tracked parameters in the same way as parameters that carry a @refineOverride annotation. [Cherry-picked 23cb1f3]

[Cherry-picked 48a52a2]

WojciechMazur · 2025-04-10T13:13:38Z

This backport was required by multiple conflicts occurring while backporting relatively small #22849

However, based on the size of changes (in this and 2 other PR) we'd prefer to not backport it at the last moment

64 files changed, 3866 insertions(+), 1500 deletions(-)  // excluding tests
232 files changed, 6362 insertions(+), 2010 deletions(-) // including

@natsukagami @odersky Do you think it would be possible to create an alternative variant for 3.7.0 including only required stabilisation changes without a large refactor? Preferably only having required changes from #22849 and #22956
It feels a bit risky to introduce such big change in such late moment

odersky · 2025-04-10T14:19:20Z

I agree, this PR should not be backported, the change set is too large. We intentionally waited until after the 3.7 cutoff to merge it. So yes, we need to extract just #22849 and #22956.

natsukagami · 2025-04-10T15:04:34Z

I'll extract the two PRs by tonight.

EDIT see #22967

odersky and others added 30 commits April 10, 2025 14:43

Elide capabilities implied by Capability subtypes when printing

e29c8d9

When printing a type `C^` where `C` extends `Capability`, don't show the `^`. This is overridden under -Yprint-debug. [Cherry-picked 103ef96]

Drop special handling of functions with pure arguments in Existential…

8e37a5c

….toCap If existentials are mapped to fresh, it matters where they are opened. Pure or not arguments don't have anything to do with that. [Cherry-picked e4cc265]

Separation checking for applications

d218cc4

Check separation from source 3.7 on. We currently only check applications, other areas of separation checking are still to be implemented. [Cherry-picked 4c8a50f]

Separation checking for blocks

8939a08

Check that a capability that gets hidden in the (result-)type of some definition is not used afterwards in the same or a nested scope. [Cherry-picked b0c9b3d]

Address review comments

7a714d2

[Cherry-picked 70074c4]

Use deep capturesets for separation checking.

6b2c624

When checking whether two items overlap we should always check their deep capture sets. Buried aliases should count as well. [Cherry-picked 190aaca]

Cache derived reach, readOnly, and maybe capabilities

ec0bafd

This is necessary since capability sets are IdentitySets. [Cherry-picked 67d42bd]

Avoid forming intersections of capture sets on refined type lookup

e265377

[Cherry-picked b1da91a]

Check separation of different parts of a declared type.

485a534

[Cherry-picked 131f070]

Check that hidden parameters are annotated @consume

b106107

TODO: - check that only @consume parameters flow to @consume parameters [Cherry-picked 3adf4b0]

Check that only @consume parameters flow to @consume parameters

83c864c

[Cherry-picked ee23239]

Check that SharedCapabilities don't capture cap.

b83d97a

[Cherry-picked a4df033]

Turn separation checking on by default

654415c

Downgrade to -source 3.6 to turn it off. [Cherry-picked 52dc9b4]

Make sure fresh results of methods only hide local refs

ac1ba8a

[Cherry-picked 824dd83]

Make sure parameters are not used again after they are consumed

246c27e

[Cherry-picked 7b0b80b]

Check accesses to non-local this in hidden sets

00c94c3

Allow them only in @consume methods [Cherry-picked 66fc880]

Check that @consumed prefix capabilities are not re-used

2d2271a

Also: Fixes to computations of overlapWith and -- on Refs that take account of pathss, where shorter paths cover deeper ones. [Cherry-picked 821e17a]

Allow SharableCapablity anywhere on a path

0b67cf8

[Cherry-picked 3ed82a3]

Polishings

0b3187e

[Cherry-picked 2d37938]

Polish and document separation checker.

ce1477f

[Cherry-picked d661678]

Address review comments

04be85a

[Cherry-picked 9710872]

Fix handling paths extending SharedCapabiolity

fb00530

This partially reverts commit 7b3d3f4. It looks like this fixes the problems we had with CI timeouts as well. [Cherry-picked 367f66c]

Streamline deepCaptureSet

e3b8034

[Cherry-picked 51050f9]

Avoid edge case where non-sensical info was printed for selections

9918cf5

[Cherry-picked f0e0117]

Make printFresh a -Y option

bf10f66

[Cherry-picked 8d15e88]

Charge deep capture set for arguments to @consume parameters

5c636ae

[Cherry-picked 5132d55]

Don't flag local fresh capabilities as errors in markFree

938afc5

[Cherry-picked 21a5399]

Tweak error message in SepCheck

852a710

[Cherry-picked 91eef32]

hamzaremmal and others added 25 commits April 10, 2025 14:44

chore: double the heap size and the stack size

3fe1c8c

[Cherry-picked f3ef42b]

Make CanThrow a SharedCapability

ab3c8e9

[Cherry-picked 641dffa]

Let existential variables only subsume shared capabilities

e472bc9

Also, implement infrastructure to add a note to a type mismatch when a failure to subsume occurs. [Cherry-picked 58baf53]

Classify existential variables as root capabilities

e09162c

Allows some simplifications in the zoo of classification methods. [Cherry-picked 33ef293]

Classify existential variables as root capabilities

5256587

Allows some simplifications in the zoo of classification methods. [Cherry-picked 12047d8]

Merge Existential and Fresh into root module

aeb5b28

[Cherry-picked 399b220]

Drop Caps_Exists handling and deprecate caps.Exists

9cfc405

[Cherry-picked 6093dab]

Small tweaks

e0b3711

[Cherry-picked f7484ce]

Make cap not subsume anything by default.

2d3016f

Exceptions are bracketed in `withCapAsRoot` calls. [Cherry-picked d27f2bb]

Turn off withCapAsRoot exception for box adaptation

a527629

TODO: Check that the new error in box-adapt-contra makes sense TODO: error messages need to be improved [Cherry-picked ec8d119]

Test case showing that second soundness hole is filled

4d097ac

[Cherry-picked 731c9aa]

Tighten consume checks

b7c6b35

1. Strip readonly modifier before checking o=for overlaps 2. Don't reset consume to empty before entering defs [Cherry-picked d89138a]

Split posCC from pos tests

c37499e

I believe the timeout was simply that we have to many pos tests, so theior compilation takes more than the limit of 20 minutes. Testing this hypothesis by moving pos-custumargs/captures tests into a separate top-level test posCC [Cherry-picked a6f1ab2]

Fine-tune pruning for consume checks of arguments

6e6dfb8

Deduct explicit refs of actual as opposed to formal argument type. [Cherry-picked d2e276c]

Refactor

462bb0e

Move extension methods to SepChecks object, drop unused ones. [Cherry-picked f547582]

Fix compute overlap logic for consumes

22c70e1

- Make it peak-based instead of footprint-based - Don't flag rd/rd conflicts between consumed and re-used [Cherry-picked ee60b21]

Remove unused files and document root.scala

b4fe06f

[Cherry-picked c790007]

Add mut modifier to Parser doc comment

31a539a

[Cherry-picked 9a49c52]

Rename -Ycc-print-fresh to -Ycc-verbose

c53b88a

[Cherry-picked d781b3e]

Refactor addenda generation

990d286

Avoid globally visible vars in CCState. Make sure notes don't leak from one test to another. [Cherry-picked dc0dd7f]

More refactoring, avoid globally accessible variable

312b330

[Cherry-picked fbe37b8]

Fix typo in error message

98d1ab0

[Cherry-picked ac84d13]

Fix MimaFilters

cffd1a2

[Cherry-picked 48a52a2]

WojciechMazur closed this Apr 11, 2025

WojciechMazur deleted the backport-release-3.7.0-22539 branch April 11, 2025 14:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Backport "Separation checking for product types" to 3.7.0 #22964

Backport "Separation checking for product types" to 3.7.0 #22964

WojciechMazur commented Apr 10, 2025

WojciechMazur commented Apr 10, 2025

odersky commented Apr 10, 2025 •

edited

Loading

natsukagami commented Apr 10, 2025 •

edited

Loading

Backport "Separation checking for product types" to 3.7.0 #22964

Backport "Separation checking for product types" to 3.7.0 #22964

Conversation

WojciechMazur commented Apr 10, 2025

WojciechMazur commented Apr 10, 2025

odersky commented Apr 10, 2025 • edited Loading

natsukagami commented Apr 10, 2025 • edited Loading

odersky commented Apr 10, 2025 •

edited

Loading

natsukagami commented Apr 10, 2025 •

edited

Loading