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 Subtyping and Normalization of Capture Sets #22103

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

Improve Subtyping and Normalization of Capture Sets #22103

bracevac opened this issue Dec 3, 2024 · 1 comment · Fixed by #22299 · May be fixed by #22288
Assignees
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
@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
bracevac added a commit to bracevac/scala3 that referenced this issue Jan 1, 2025
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.
bracevac added a commit to dotty-staging/dotty that referenced this issue Jan 19, 2025
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.
bracevac added a commit to dotty-staging/dotty that referenced this issue Jan 19, 2025
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.
bracevac added a commit that referenced this issue Jan 22, 2025
Fixes #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.

Supersedes #22183 and
#22289. This solution is overall
cleaner and does not require adding a new bit to the TypeComparer's
ApproxState.

TODOs/Issues/Questions:

- [x] Fix extension method in test
[cc-poly-varargs.scala](https://github.com/dotty-staging/dotty/blob/capture-subtyping-canon/tests/pos-custom-args/captures/cc-poly-varargs.scala).
Currently causes an infinite regress.
   - [x] Fix the aftermath
      * tests/neg-custom-args/captures/lazylists-exceptions.scala
      * tests/neg-custom-args/captures/exceptions.scala
      * tests/neg-custom-args/captures/real-try.scala
      * tests/run-custom-args/captures/colltest5
- [x] Some negative cases in test
[capture-vars-subtyping.scala](https://github.com/dotty-staging/dotty/blob/capture-subtyping-canon/tests/neg-custom-args/captures/capture-vars-subtyping.scala)
pass: `D <: E` fails, but its canonicalized form `CapSet^{D^} <:
CapSet^{E^}` now succeeds. Potential problem in the subcapturing
implementation.
- [x] ~Extend to intersection/unions `def f[C^, D^, E <: C | D, F <: C &
D](...) = ...` etc.~ Lacking good uses cases, not planned right now.
- [X] ~If we have `C^` declared in the current context, should there be
a difference between `C` vs. `C^` for subsequent mentions? We currently
do, but seems a bit too subtle for users.~ Will be addressed by a new
scheme for declaring capture variables using context bounds.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment