Skip to content

Ignore capture sets in certain cases of subtyping #22183

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

Closed
wants to merge 2 commits into from
Closed

Ignore capture sets in certain cases of subtyping #22183

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7d8b439
Ignore capture sets in certain cases of subtyping
bracevac Dec 10, 2024
7f1d765
Tests for capture variable subtyping
bracevac Dec 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 47 additions & 0 deletions tests/neg-custom-args/captures/capture-vars-subtyping.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
import language.experimental.captureChecking
import caps.*

def test[C^] =
val a: C = ???
val b: CapSet^{C^} = a
val c: C = b
val d: CapSet^{C^, c} = a

// TODO: make "CapSet-ness" of type variables somehow contagious?
// Then we don't have to spell out the bounds explicitly...
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should support that. Say we have def foo[C^, D <: C, E >: C], then we should automatically constraint both D and E to be capture set variables, i.e., D is implicitly lower-bounded by CapSet, and E is implicitly upper-bounded by CapSet^

def testTrans[C^, D >: CapSet <: C, E >: CapSet <: D, F >: C <: CapSet^] =
val d1: D = ???
val d2: CapSet^{D^} = d1
val d3: D = d2
val e1: E = ???
val e2: CapSet^{E^} = e1
val e3: E = e2
val d4: D = e1
val c1: C = d1
val c2: C = e1
val f1: F = c1
val d_e_f1: CapSet^{D^,E^,F^} = d1
val d_e_f2: CapSet^{D^,E^,F^} = e1
val d_e_f3: CapSet^{D^,E^,F^} = f1
val f2: F = d_e_f1
val c3: C = d_e_f1 // error
Copy link
Contributor Author

@bracevac bracevac Dec 22, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line and the three following lines are all not flagged as errors, but they should be. Investigating.

val c4: C = f1 // error
val e4: E = f1 // error
val e5: E = d1 // error


trait A[+T]

trait B[-C]

def testCong[C^, D^] =
val a: A[C] = ???
val b: A[CapSet^{C^}] = a
val c: A[CapSet^{D^}] = a // error
val d: A[CapSet^{C^,D^}] = a
val e: A[C] = d // error
val f: B[C] = ???
val g: B[CapSet^{C^}] = f
val h: B[C] = g
val i: B[CapSet^{C^,D^}] = h // error
val j: B[C] = i
Loading