Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refine rules for capture parameters and members #22000

Merged
merged 13 commits into from
Dec 1, 2024
Merged

Refine rules for capture parameters and members #22000

merged 13 commits into from
Dec 1, 2024

Conversation

noti0na1
Copy link
Member

@noti0na1 noti0na1 commented Nov 21, 2024 •
edited
Loading

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 noti0na1 requested a review from bracevac November 21, 2024 19:17
@noti0na1 noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from 651b674 to c933560 Compare November 22, 2024 09:59
@noti0na1
Copy link
Member Author

noti0na1 commented Nov 22, 2024 •
edited
Loading

TODO: fix override check for type members during CC

@noti0na1 noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from d016cce to a8c624e Compare November 24, 2024 22:22
@noti0na1 noti0na1 mentioned this pull request Nov 26, 2024
Closed
@noti0na1 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
bracevac reviewed Nov 26, 2024
View reviewed changes
tests/pos-custom-args/captures/cc-poly-varargs.scala



race[Either[T1, T2], Cap](left, right)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

tests/pos-custom-args/captures/cc-poly-varargs.scala Outdated Show resolved Hide resolved
tests/pos-custom-args/captures/cc-poly-varargs.scala Outdated Show resolved Hide resolved
tests/neg/cc-poly-2.scala Outdated Show resolved Hide resolved
compiler/src/dotty/tools/dotc/cc/CaptureRef.scala Show resolved Hide resolved
This was linked to issues Nov 29, 2024
Wrong subcapture check result when capture parameter presents #22005
Closed
Type members are not checked for overriding during CC #22030
Closed
@noti0na1 noti0na1 requested review from odersky and Linyxus November 29, 2024 14:29
@noti0na1 noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from 008eb08 to 5a901f4 Compare November 29, 2024 14:34
@noti0na1
Copy link
Member Author

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

@noti0na1 noti0na1 added the area:experimental:cc Capture checking related label Nov 29, 2024
odersky
odersky requested changes Nov 29, 2024
View reviewed changes
Copy link
Contributor

@odersky odersky left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise LGTM

compiler/src/dotty/tools/dotc/parsing/Parsers.scala Outdated
@@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure

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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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, _) =>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same as above; can this case happen?

odersky
odersky approved these changes Nov 30, 2024
View reviewed changes
Copy link
Contributor

@odersky odersky left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might need a rebase to make the tests pass.

@noti0na1
Copy link
Member Author

Currently blocked by error on main branch: #22058

Linyxus
Linyxus approved these changes Nov 30, 2024
View reviewed changes
Copy link
Contributor

@Linyxus Linyxus left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@noti0na1 noti0na1 force-pushed the make-cap-params-bounded-by-capset branch from 8fc3df1 to 6866bd1 Compare December 1, 2024 19:25
@noti0na1 noti0na1 merged commit 6bf4483 into scala:main Dec 1, 2024
29 checks passed
@noti0na1 noti0na1 deleted the make-cap-params-bounded-by-capset branch December 1, 2024 20:57
@bracevac bracevac mentioned this pull request Dec 3, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Linyxus Linyxus Linyxus approved these changes

@bracevac bracevac bracevac approved these changes

@odersky odersky odersky approved these changes

Assignees

@bracevac bracevac

Labels
area:experimental:cc Capture checking related
Projects
None yet
Milestone
No milestone
4 participants
@noti0na1 @odersky @bracevac @Linyxus