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

Type members are not checked for overriding during CC #22030

Closed
noti0na1 opened this issue Nov 26, 2024 · 2 comments · Fixed by #22000
Closed

Type members are not checked for overriding during CC #22030

noti0na1 opened this issue Nov 26, 2024 · 2 comments · Fixed by #22000
Milestone

Comments

@noti0na1
Copy link
Member

noti0na1 commented Nov 26, 2024

Compiler version

3.6.4-RC1-bin-20241125-0afabd6-NIGHTLY, the main branch

Minimized code

import language.experimental.modularity
import caps.*

class IO
class File

trait Abstract(tracked val io: IO^):
  type C >: CapSet <: CapSet^{io}
  def f(file: File^{C^}): Unit

class Concrete1(io: IO^) extends Abstract(io):
  type C = CapSet
  def f(file: File) = ()

class Concrete2(io1: IO^, io2: IO^) extends Abstract(io1):
  // Overriden member: type C >: CapSet <: CapSet^{io1}
  type C = CapSet^{io2} // should be error, since CapSet^{io2} !<:< CapSet^{io1}
  def f(file: File^{io2}) = ()

Output

Compiled without any error

Expectation

Should report error overriding type C in Concrete2

@noti0na1
Copy link
Member Author

noti0na1 commented Nov 26, 2024

However, if we encode the capture set into a type parameter, the same program can be checked correctly with #22000:

import language.experimental.modularity
import caps.*

class IO
class File

trait Abstract[X^]:
  type C >: CapSet <: X
  def f(file: File^{C^}): Unit

class Concrete1(io: IO^) extends Abstract[CapSet^{io}]:
  type C = CapSet
  def f(file: File) = ()

class Concrete2(io1: IO^, io2: IO^) extends Abstract[CapSet^{io1}]:
  type C = CapSet^{io2} // error
  def f(file: File^{io2}) = ()
-- [E164] Declaration Error: Stest.scala:1718:7 --------------------------------
1718 |  type C = CapSet^{io2} // error
     |       ^
     |error overriding type C in trait Abstract with bounds >: caps.CapSet <: caps.CapSet^{Concrete2.this.io1};
     |  type C, which equals caps.CapSet^{Concrete2.this.io2} has incompatible type
     |
     | longer explanation available when compiling with `-explain`
1 error found

@noti0na1
Copy link
Member Author

noti0na1 commented Nov 26, 2024

Maybe related to !compatTypes(memberTp(upwardsSelf), otherTp(upwardsSelf))) in checkAllOverrides during cc phase? The upwardsSelf gives wrong types.

@noti0na1 noti0na1 linked a pull request Nov 29, 2024 that will close this issue
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]
@WojciechMazur WojciechMazur added this to the 3.6.4 milestone Jan 16, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants