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.

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

Two fixes to capture checking #17524

Merged
merged 2 commits into from
May 22, 2023
Merged

Two fixes to capture checking #17524

merged 2 commits into from
May 22, 2023

Conversation

Linyxus
Copy link
Contributor

@Linyxus Linyxus commented May 16, 2023

  • It changes isParamDependent to consider CaptureDependency as well, so that when applying a capture dependent function the capture sets in the types of the remaining parameters will be correctly substituted. For example:
def foo[X](x: Foo[X]^, op: () ->{x} Unit): Unit = ???
foo(a, useA)

After rechecking a in the argument list, the expected type of the second argument, useA, should become () -> {a} Unit. This example previously does not work.

  • It fixes Dependent function application can leak a scoped capability #17517. It fixes the healing of capture sets, which happens at the end of the capture checking phase, in which we traverse the capture checked tree and try to heal the ill-formed capture sets in type arguments. Here we say a capture set C in a type argument is ill-formed if it contains TermParamRef bound by other lambdas. For example:
def usingLogger[sealed T](f: OutputStream^)(op: Logger^{f} => T): T = ???
usingLogger[() ->?1 Unit](file)(l => () => l.log("test"))

l will be propagated to ?1 as a result of capture checking, which makes ?1 ill-formed and we should widen l to file. The problem is that we heal the capture sets one-after-another but the healing of a later capture set may propagate more TermParamRefs to a healed one. For example:

usingFile[() ->?2 Unit](  // should be error
  "foo",
  file => {
    usingLogger[() ->?1 Unit](file)(l => () => l.log("test"))
  }
)

After capture checking both ?1 and ?2 will be {l}. When traversing the tree we first heal ?2, wherein we widen l to file, but file is a TermRef here and we do nothing. Then, only later when we heal ?1, we also widen l to file but this will end up propagating a TermParamRef of file to ?2, which we should have widened as well. But ?2 is already healed and is not inspected again.

This PR solves this issue by installing a handler when healing the capture sets which will try to heal the new elements propagated later in the healing process.

Linyxus added 2 commits May 17, 2023 00:48
Capture set healing happens at the end of capture checking (in the `postCheck`
function), which checks the capture set in each type argument and widen the
ill-formed `TermParamRef`s by widening them. However, it is possible that a
capture set is healed first, and then get a `TermParamRef` propagated into it
later when we are healing another capture set. This lead to unsoundness.

This commit installs an handler on capture sets when healing them and will
inspect the newly added elements and heal these new elements as well.
@odersky odersky merged commit f2f1156 into scala:main May 22, 2023
@odersky odersky deleted the cc-dep-param branch May 22, 2023 16:38
@Kordyjan Kordyjan added this to the 3.3.1 milestone Aug 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Dependent function application can leak a scoped capability
3 participants