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

Wrong subcapture check result when capture parameter presents #22005

Closed
noti0na1 opened this issue Nov 22, 2024 · 1 comment · Fixed by #22000
Closed

Wrong subcapture check result when capture parameter presents #22005

noti0na1 opened this issue Nov 22, 2024 · 1 comment · Fixed by #22000
Labels
area:experimental:cc Capture checking related itype:bug

Comments

@noti0na1
Copy link
Member

Compiler version

Current version
3.6.4-RC1-bin-SNAPSHOT-nonbootstrapped-git-c933560

Minimized code

import language.experimental.captureChecking
import caps.*

class IO
class File(io: IO^)
class Handler[C^]:
  def f(file: File^): File^{C^} = file // should be error!
  def g(file: File^{C^}): File^ = file // ok

def test(io1: IO^, io2: IO^, h: Handler[CapSet^{io2}]) =
  val f1: File^{io1} = ???
  val f2: File^{io2} = h.f(f1) // problem!

Output

Compiled

Expectation

Should reject f
@noti0na1 noti0na1 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 and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Nov 22, 2024
@noti0na1
Copy link
Member Author

cc @odersky @Linyxus @bracevac

@noti0na1 noti0na1 added area:experimental:cc Capture checking related and removed cc-experiment Intended to be merged with cc-experiment branch on origin labels Nov 22, 2024
noti0na1 added a commit to dotty-staging/dotty that referenced this issue Nov 22, 2024
@noti0na1
Fixing scala#22005
ba08501
@noti0na1 noti0na1 mentioned this issue Nov 22, 2024
Merged
@noti0na1 noti0na1 linked a pull request Nov 29, 2024 that will close this issue
Refine rules for capture parameters and members #22000
Merged
noti0na1 added a commit that referenced this issue Dec 1, 2024
@noti0na1
Refine rules for capture parameters and members (#22000)
6bf4483 
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
Assignees
No one assigned
Labels
area:experimental:cc Capture checking related itype:bug
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Refine rules for capture parameters and members dotty-staging/dotty
1 participant
@noti0na1