Refine rules for capture parameters and members #22000

noti0na1 · 2024-11-21T19:13:18Z

This PR refines rules for capture set variables (parameters and members).

Fix #21999, #22005, #22030

Add requirements for capture set variables

When a capture set is encoded as a type, the type must refer to CapSet and bounded by >: CapSet <: CapSet^.

An unbounded capture parameter would be C >: CapSet <: CapSet^, which can be desugared from C^.

def f[C^](io: IO^{C^}) = ???

// becomes

def f[C >: CapSet <: CapSet^](io: IO^{C^}) = ???

We may consider the similar desugaring for type member in the future:

class A:
  type C^

// becomes

class A:
  type C >: CapSet <: CapSet^

Then, constaints between capture variables become possible:

def test[X^, Y^, Z >: X <: Y](x: C^{X^}, y: C^{Y^}, z: C^{Z^}) = ???
// Z is still bounded by >: CapSet <: CapSet^

Update definitions in the library caps.scala, such that a type following the rule can be used inside a capture set.

// Rule out C^{(Nothing)^} during typer
def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ???

sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]

Add cases to handle `CapSet` in `subsumes`

*   X = CapSet^cx, exists rx in cx, rx subsumes y ==>  X subsumes y
*   Y = CapSet^cy, forall ry in cy, x subsumes ry ==>  x subsumes Y
*   X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y  ==> X subsumes y
*   Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
*   Contains[X, y]  ==>  X subsumes y

Fix some issues related to overriding

When deciding whether a class has a non-trivial self type, we look at the underlying type without capture set.

[test_scala2_library_tasty]

noti0na1 · 2024-11-22T13:45:47Z

TODO: fix override check for type members during CC

bracevac · 2024-11-26T15:57:03Z

tests/pos-custom-args/captures/cc-poly-varargs.scala

-
-
-
+  race[Either[T1, T2], Cap](left, right)


This should not be necessary. I'll look into normalization and subtyping of captures.

The subtyping Cap <:< CapSet^{Cap^} should work. We will fix this in a different PR.

tests/pos-custom-args/captures/cc-poly-varargs.scala

tests/neg/cc-poly-2.scala

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

Co-authored-by: Oliver Bračevac <[email protected]>

noti0na1 · 2024-11-29T14:35:48Z

@bracevac This PR should be ready to review. The one error in test_scala2_library_tasty is not related to this PR.

odersky

Otherwise LGTM

odersky · 2024-11-29T16:58:51Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -4057,8 +4057,11 @@ object Parsers {
              || sourceVersion.isAtLeast(`3.6`) && in.isColon =>
            makeTypeDef(typeAndCtxBounds(tname))
          case _ =>
-            syntaxErrorOrIncomplete(ExpectedTypeBoundOrEquals(in.token))
-            return EmptyTree // return to avoid setting the span to EmptyTree
+            if in.isIdent(nme.UPARROW) && Feature.ccEnabled then


This is not backed by a comment or a syntax description. Do we want to accept

type C^

now? I suggest we wait with introducing this. The syntax might change. And for now, we can just write the expansion. So I would propose we drop this change for the time being.

odersky · 2024-11-29T18:24:05Z

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

@@ -135,14 +142,26 @@ trait CaptureRef extends TypeProxy, ValueType:
              case _ => false
          || viaInfo(y.info)(subsumingRefs(this, _))
        case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
+        case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) =>
+          y.info match
+            case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)


Can this case happen? I thought the upper bound has to be of the form CapSet^cs? If it can happen, maybe add a comment explaining why.

The upper and lower bounds don't have to be in the form of CapSet^{...}. They can also be other capture set variables, which are bounded by CapSet, like def test[X^, Y^, Z >: X <: Y]. With this set up, both cases would happen during subsumes.

odersky · 2024-11-29T18:24:19Z

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

+        case x: TypeRef if assumedContainsOf(x).contains(y) => true
+        case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
+          x.info match
+            case TypeBounds(lo: CaptureRef, _) =>


Same as above; can this case happen?

odersky

Might need a rebase to make the tests pass.

noti0na1 · 2024-11-30T13:01:07Z

Currently blocked by error on main branch: #22058

noti0na1 requested a review from bracevac November 21, 2024 19:17

noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from 651b674 to c933560 Compare November 22, 2024 09:59

noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from d016cce to a8c624e Compare November 24, 2024 22:22

noti0na1 mentioned this pull request Nov 26, 2024

Type members are not checked for overriding during CC #22030

Open

noti0na1 changed the title ~~Make capture parameters and members bounded by CapSet by default~~ Refine rules for capture parameters and members Nov 26, 2024

bracevac reviewed Nov 26, 2024

View reviewed changes

This was linked to issues Nov 29, 2024

Wrong subcapture check result when capture parameter presents #22005

Open

Type members are not checked for overriding during CC #22030

Open

noti0na1 requested review from odersky and Linyxus November 29, 2024 14:29

noti0na1 and others added 11 commits November 29, 2024 15:31

Make capture parameters and members bounded by CapSet by default

4c8300e

Correct rules for CapSet; update definition for Contains; fix tests

1016e77

Refine subsumes rule; fix test

dc99105

Add constraint to capsOf

d531cb5

Update test

3c7e419

Apply suggestions from code review

9f665b5

Co-authored-by: Oliver Bračevac <[email protected]>

Fix test

25fdb50

Fix crash error

f440e6d

Fix overriding check

7aa534f

Update Stepper in the library

9b92726

Clean comments

5a901f4

noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from 008eb08 to 5a901f4 Compare November 29, 2024 14:34

noti0na1 assigned bracevac Nov 29, 2024

noti0na1 added the area:experimental:cc Capture checking related label Nov 29, 2024

bracevac approved these changes Nov 29, 2024

View reviewed changes

odersky requested changes Nov 29, 2024

View reviewed changes

noti0na1 added 2 commits November 30, 2024 01:42

Drop syntax sugar for capture set member

f8893e5

Update comment

8fc3df1

odersky approved these changes Nov 30, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refine rules for capture parameters and members #22000

Refine rules for capture parameters and members #22000

noti0na1 commented Nov 21, 2024 •

edited

Loading

noti0na1 commented Nov 22, 2024 •

edited

Loading

bracevac Nov 26, 2024

noti0na1 Nov 29, 2024

noti0na1 commented Nov 29, 2024

odersky left a comment

odersky Nov 29, 2024

noti0na1 Nov 30, 2024

odersky Nov 29, 2024

noti0na1 Nov 30, 2024

odersky Nov 29, 2024

odersky left a comment

noti0na1 commented Nov 30, 2024

Refine rules for capture parameters and members #22000

Are you sure you want to change the base?

Refine rules for capture parameters and members #22000

Conversation

noti0na1 commented Nov 21, 2024 • edited Loading

Add requirements for capture set variables

Add cases to handle CapSet in subsumes

Fix some issues related to overriding

noti0na1 commented Nov 22, 2024 • edited Loading

bracevac Nov 26, 2024

Choose a reason for hiding this comment

noti0na1 Nov 29, 2024

Choose a reason for hiding this comment

noti0na1 commented Nov 29, 2024

odersky left a comment

Choose a reason for hiding this comment

odersky Nov 29, 2024

Choose a reason for hiding this comment

noti0na1 Nov 30, 2024

Choose a reason for hiding this comment

odersky Nov 29, 2024

Choose a reason for hiding this comment

noti0na1 Nov 30, 2024

Choose a reason for hiding this comment

odersky Nov 29, 2024

Choose a reason for hiding this comment

odersky left a comment

Choose a reason for hiding this comment

noti0na1 commented Nov 30, 2024

noti0na1 commented Nov 21, 2024 •

edited

Loading

Add cases to handle `CapSet` in `subsumes`

noti0na1 commented Nov 22, 2024 •

edited

Loading