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

Improve Subtyping and Normalization of Capture Sets #22103

Open
bracevac opened this issue Dec 3, 2024 · 1 comment · May be fixed by #22299 or #22288
Open

Improve Subtyping and Normalization of Capture Sets #22103

bracevac opened this issue Dec 3, 2024 · 1 comment · May be fixed by #22299 or #22288
Assignees
@bracevac
Labels
area:experimental:cc Capture checking related itype:bug

Comments

@bracevac
Copy link
Contributor

bracevac commented Dec 3, 2024

Compiler version

Latest nightly

Minimized code

As noted in PR #22000, some expected subtyping
relations are still not supported.

import language.experimental.captureChecking

abstract class Source[+T, Cap^]:
  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{this, f} = ???

def race[T, Cap^](sources: Source[T, Cap]^{Cap^}*): Source[T, Cap]^{Cap^} = ???

def either[T1, T2, Cap^](
    src1: Source[T1, Cap]^{Cap^},
    src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
  val left = src1.transformValuesWith(Left(_))
  val right = src2.transformValuesWith(Right(_))
  race(left, right) // <- rejected
  //race[Either[T1, T2], Cap](left, right) // <- accepted

Expectation

The last line should not require explicit type arguments. This appears to be caused
by not being able to conclude Cap <: CapSet^{Cap^}, but both sides
are morally equivalent.
@bracevac bracevac added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Dec 3, 2024
@bracevac bracevac self-assigned this Dec 3, 2024
@bracevac bracevac added area:experimental:cc Capture checking related and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Dec 3, 2024
@bracevac bracevac mentioned this issue Dec 10, 2024
Closed
@Linyxus
Copy link
Contributor

Linyxus commented Jan 1, 2025

A (possible) minimisation:

import language.experimental.captureChecking
import caps.*

trait F[Cap^]
def expect[C^](x: F[C]): x.type = x

def test[C^](x: F[C]): Unit =
  val t1 = expect[CapSet^{C^}](x)

Linyxus added a commit to dotty-staging/dotty that referenced this issue Jan 1, 2025
@Linyxus
Add test cases for scala#22103
32e550b
@Linyxus Linyxus linked a pull request Jan 1, 2025 that will close this issue
Draft
bracevac added a commit to bracevac/scala3 that referenced this issue Jan 1, 2025
@bracevac
Canonicalize capture variable subtype comparisons
079d4f5 
Fixes scala#22103

Subtype problems where at least one side is a type variable
representing a capture variable are canonicalized to
capturing type comparisons on the special `CapSet` for the
universe capture sets. For example, `C <: CapSet^{C^}`
becomes `CapSet^{C^} <: CapSet^{C^}`, and `A <: B` becomes
`CapSet^{A^} <: CapSet^{B^}` if both `A` and `B` are capture
variables.
This was referenced Jan 1, 2025
Closed
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bracevac bracevac

Labels
area:experimental:cc Capture checking related itype:bug
Projects
None yet
Milestone
No milestone
2 participants
@bracevac @Linyxus