Skip to content

Cache ResultCaps #23198

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

Merged
merged 10 commits into from
May 21, 2025
Merged

Cache ResultCaps #23198

merged 10 commits into from
May 21, 2025

Conversation

odersky
Copy link
Contributor

@odersky odersky commented May 20, 2025

This fixes problems encountered for #15923 where we got infinite recursions
caused by infinite streams of new ResultCap instances that were added to capture sets.
The analysis of the problem showed that there is a cycle of dependencies involving
both forwards and backwards propagations of ResultCap instances between
BiMapped capture sets linked by SubstBindingMaps. Each propagation would
create a new derived ResultCap instance.

We could try to solve the problem by having SubstBindingMaps remember their mappings
and have their inverses work backwards. But that could still produce an infinite stream
if there was a cycle of SubstBindingMaps of length > 2. So we fix the problem at the
root by allowing only one derived ResultCap instance per original ResultCap / binder pair.

Fixes #15923

Based on #23184. Only last commit is new.

@odersky odersky requested a review from Linyxus May 20, 2025 09:40
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!

however, the soundness issue I mentioned does compile on the branch too:

import language.experimental.captureChecking
trait Cap
case class Id[X](x: X)
def mkId[X](x: X): Id[X] = Id(x)
def withCap[X](op: (lcap: Cap^) => () => X): X = ???
def bar() =
  val f = (lcap: Cap^) => () => mkId(lcap)
  val leak = withCap(f)
  val leaked = leak.x

Seems to be related to capture sets for inferred types.

@Linyxus
Copy link
Contributor

Linyxus commented May 20, 2025

The tree after cc:

    def bar(): Unit =
      {
        val f: (x$0: Cap^) ->{} () ->{} Id[box Cap^{x$0}]^{} = (lcap: Cap^) => () => mkId[box Cap^{lcap}](lcap)
        val leak: Id[box Cap^{}]^{} = withCap[box Id[box Cap^?]^?](f)
        val leaked: Cap^{} = leak.x
        ()
      }

note that f has the type (x$0: Cap^) -> () -> Id[box Cap^{x$0}] but when passing f to withCap the capture set in the inferred type argument seems to be empty (box Id[box Cap^?]).

@Linyxus Linyxus assigned odersky and unassigned Linyxus May 20, 2025
@odersky
Copy link
Contributor Author

odersky commented May 20, 2025

The tree after cc:

    def bar(): Unit =
      {
        val f: (x$0: Cap^) ->{} () ->{} Id[box Cap^{x$0}]^{} = (lcap: Cap^) => () => mkId[box Cap^{lcap}](lcap)
        val leak: Id[box Cap^{}]^{} = withCap[box Id[box Cap^?]^?](f)
        val leaked: Cap^{} = leak.x
        ()
      }

note that f has the type (x$0: Cap^) -> () -> Id[box Cap^{x$0}] but when passing f to withCap the capture set in the inferred type argument seems to be empty (box Id[box Cap^?]).

Two observations:

  • An error is issued if X is declared covariant in Id.
  • If we drop the inner () => in withCap and f we get the same behavior - error for +X, no error for X.

odersky added 10 commits May 21, 2025 13:49
Note i15923 does not signal a leak anymore. I moved it and some variants to pending.
Note: There seems to be something more fundamentally wrong with this test: We get an
infinite recursion for variant i15923b.
There was some accidental type confusion which made every capture root type end up
with cap as pathRoot and caps as pathOwner.
Split out Capability from Type. For now we keep most of the overall structure. E.g. capability handling code is
in file CaptureRef.scala. We will change this afterwards in separate refactorings.
Fixes scala#23170

This was disabled before. We also had to slightly extend fresh/cap collapsing
to make override checks go through under the new scheme.
This fixes problems encountered in scala#15923 where we got infinite recursions
caused by infinite streams of new ResultCap instances that were added to capture sets.
The analysis of the problem showed that there is a cycle of dependencies involving
both forwards and backwards propagations of ResultCap instances between
BiMapped capture sets linked by SubstBindingMaps. Each propagation would
create a new derived ResultCap instance.

We could try to solve the problem by having SubstBindingMaps remember their mappings
and have their inverses work backwards. But that could still produce an infinite stream
if there was a cycle of SubstBindingMaps of length > 2. So we fix the problem at the
root by allowing only one derived ResultCap instance per original ResultCap / binder pair.

Fixes scala#15923
A dependent function is represented as a refinement type with a normal applied
function type as parent. When capture checking two dependent function types, the
parents should be ignored. But there was a case where this did not happen:
If the left hand side is a sinletontype with a capturing type over a dependent function
type, and the original method type comparisons fail, then the parent type of the
left hand type was tried as a fallback. This commit adds a test that prevents
the fallback.
@odersky odersky assigned Linyxus and unassigned odersky May 21, 2025
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.

look great to me !

@Linyxus Linyxus enabled auto-merge May 21, 2025 14:11
@Linyxus Linyxus merged commit b078f6d into scala:main May 21, 2025
28 checks passed
@Linyxus Linyxus deleted the fix-15923 branch May 21, 2025 14:42
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.

Leaking capability in Scott-encoded wrapper
2 participants