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

Improve Captureset Subtyping and Intervals #21999

Closed
bracevac opened this issue Nov 21, 2024 · 1 comment · Fixed by #22000
Closed

Improve Captureset Subtyping and Intervals #21999

bracevac opened this issue Nov 21, 2024 · 1 comment · Fixed by #22000
Labels
area:experimental:cc Capture checking related cc-experiment Intended to be merged with cc-experiment branch on origin itype:bug

Comments

@bracevac
Copy link
Contributor

bracevac commented Nov 21, 2024

From discussions in PR #21875

Compiler version

Latest NIGHTLY

Minimized code

import language.experimental.captureChecking
import caps.*

trait Abstract[X >: Nothing]: // Concrete2 and 3 fail with this lower bound, but work with X >: CapSet^{}
    type C >: X <: CapSet^
    def boom(): Unit^{C^}

class Concrete extends Abstract[CapSet^{}]:
    type C = CapSet^{}
    def boom() = () // ok

class Concrete2 extends Abstract[CapSet^{}]:
    type C = CapSet^{} & CapSet^{}
    def boom() = () // error

class Concrete3 extends Abstract[CapSet^{}]:
    type C = CapSet^{} | CapSet^{}
    def boom() = () // error

Output

-- Error: local/i21868.scala:14:14 ---------------------------------------------
14 |    def boom() = () // error
   |              ^
   |          Illegal capture reference: (caps.CapSet^{}) & (caps.CapSet^{})
-- Error: local/i21868.scala:18:14 ---------------------------------------------
18 |    def boom() = () // error
   |              ^
   |          Illegal capture reference: (caps.CapSet^{}) | (caps.CapSet^{})

Expectation

  • I would expect those to work even if the lower bound of X in trait Abstract[X] is set to Nothing.
  • Can we make union and intersection on CapSet commute with capture set union and intersection, i.e., CapSet^c1 | CapSet^c2 <:> CapSet^(c1 | c2) and CapSet^c1 & CapSet^c2 <:> CapSet^(c1 & c2)? Probably, that involves improving normalizeCaptures in Setup.
  • Can we let the syntax C^ for declaring a type variable automatically desugar to the interval CapSet^{} <: C <: CapSet^?
    • Is this always airtight, or will it cause trouble?
@bracevac bracevac added itype:bug cc-experiment Intended to be merged with cc-experiment branch on origin stat:needs triage Every issue needs to have an "area" and "itype" label area:experimental:cc Capture checking related labels Nov 21, 2024
@bracevac
Copy link
Contributor Author

cc @noti0na1 @Linyxus

@bracevac bracevac removed the stat:needs triage Every issue needs to have an "area" and "itype" label label Nov 21, 2024
noti0na1 added a commit that referenced this issue Dec 1, 2024
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^`.

```scala
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:

```scala
class A:
  type C^

// becomes

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

Then, constaints between capture variables become possible:

```scala
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.

```scala
// 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]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:experimental:cc Capture checking related cc-experiment Intended to be merged with cc-experiment branch on origin itype:bug
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant