Skip to content

Commit 3be18f5

Browse files
committed
add box adaptation test cases
1 parent 577b3a5 commit 3be18f5

File tree

6 files changed

+136
-0
lines changed

6 files changed

+136
-0
lines changed
Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
trait Cap
2+
3+
def main(io: {*} Cap, fs: {*} Cap): Unit = {
4+
val test1: {} Unit -> Unit = _ => { // error
5+
type Op = [T] -> ({io} T -> Unit) -> Unit
6+
val f: ({io} Cap) -> Unit = ???
7+
val op: Op = ???
8+
op[{io} Cap](f)
9+
// expected type of f: {io} (box {io} Cap) -> Unit
10+
// actual type: ({io} Cap) -> Unit
11+
// adapting f to the expected type will also
12+
// charge the environment with {io}
13+
}
14+
15+
val test2: {} Unit -> Unit = _ => {
16+
type Box[X] = X
17+
type Op0[X] = Box[X] -> Unit
18+
type Op1[X] = Unit -> Box[X]
19+
val f: Unit -> ({io} Cap) -> Unit = ???
20+
val test: {} Op1[{io} Op0[{io} Cap]] = f
21+
// expected: {} Unit -> box {io} (box {io} Cap) -> Unit
22+
// actual: Unit -> ({io} Cap) -> Unit
23+
//
24+
// although adapting `({io} Cap) -> Unit` to
25+
// `box {io} (box {io} Cap) -> Unit` will leak the
26+
// captured variables {io}, but since it is inside a box,
27+
// we will charge neither the outer type nor the environment
28+
}
29+
30+
val test3 = {
31+
type Box[X] = X
32+
type Id[X] = Box[X] -> Unit
33+
type Op[X] = Unit -> Box[X]
34+
val f: Unit -> ({io} Cap) -> Unit = ???
35+
val g: Op[{fs} Id[{io} Cap]] = f // error
36+
val h: {} Op[{io} Id[{io} Cap]] = f
37+
}
38+
}
Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
trait Cap { def use(): Int }
2+
3+
def test1(): Unit = {
4+
type Id[X] = [T] -> (op: X => T) -> T
5+
6+
val x: Id[{*} Cap] = ???
7+
x(cap => cap.use()) // error
8+
}
9+
10+
def test2(io: {*} Cap): Unit = {
11+
type Id[X] = [T] -> (op: X -> T) -> T
12+
13+
val x: Id[{io} Cap] = ???
14+
x(cap => cap.use()) // error
15+
}
16+
17+
def test3(io: {*} Cap): Unit = {
18+
type Id[X] = [T] -> (op: {io} X -> T) -> T
19+
20+
val x: Id[{io} Cap] = ???
21+
x(cap => cap.use()) // ok
22+
}
23+
24+
def test4(io: {*} Cap, fs: {*} Cap): Unit = {
25+
type Id[X] = [T] -> (op: {io} X -> T) -> T
26+
27+
val x: Id[{io, fs} Cap] = ???
28+
x(cap => cap.use()) // error
29+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
trait Cap
2+
3+
def test1(io: {*} Cap) = {
4+
type Op[X] = [T] -> Unit -> X
5+
val f: Op[{io} Cap] = ???
6+
val x: [T] -> Unit -> ({io} Cap) = f // error
7+
}
8+
9+
def test2(io: {*} Cap) = {
10+
type Op[X] = [T] -> Unit -> {io} X
11+
val f: Op[{io} Cap] = ???
12+
val x: Unit -> ({io} Cap) = f[Unit] // error
13+
val x1: {io} Unit -> ({io} Cap) = f[Unit] // ok
14+
}
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
trait Cap { def use(): Int }
2+
3+
def test1(io: {*} Cap): Unit = {
4+
type Id[X] = [T] -> (op: {io} X -> T) -> T
5+
6+
val x: Id[{io} Cap] = ???
7+
val f: ({*} Cap) -> Unit = ???
8+
x(f) // ok
9+
// actual: {*} Cap -> Unit
10+
// expected: {io} box {io} Cap -> Unit
11+
}
12+
13+
def test2(io: {*} Cap): Unit = {
14+
type Id[X] = [T] -> (op: {*} X -> T) -> T
15+
16+
val x: Id[{*} Cap] = ???
17+
val f: ({io} Cap) -> Unit = ???
18+
x(f) // error
19+
}
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
trait Cap { def use(): Int }
2+
3+
def test1(io: {*} Cap): Unit = {
4+
type Id[X] = [T] -> (op: {io} X -> T) -> T
5+
6+
val x: Id[{io} Cap] = ???
7+
x(cap => cap.use()) // ok
8+
}
9+
10+
def test2(io: {*} Cap): Unit = {
11+
type Id[X] = [T] -> (op: {io} (x: X) -> T) -> T
12+
13+
val x: Id[{io} Cap] = ???
14+
x(cap => cap.use())
15+
// should work when the expected type is a dependent function
16+
}
17+
18+
def test3(io: {*} Cap): Unit = {
19+
type Id[X] = [T] -> (op: {} (x: X) -> T) -> T
20+
21+
val x: Id[{io} Cap] = ???
22+
x(cap => cap.use()) // error
23+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
trait Cap { def use(): Int }
2+
3+
def test1(io: {*} Cap): Unit = {
4+
type Op[X] = [T] -> X -> Unit
5+
val f: [T] -> ({io} Cap) -> Unit = ???
6+
val op: Op[{io} Cap] = f // error
7+
}
8+
9+
def test2(io: {*} Cap): Unit = {
10+
type Lazy[X] = [T] -> Unit -> X
11+
val f: Lazy[{io} Cap] = ???
12+
val test: [T] -> Unit -> ({io} Cap) = f // error
13+
}

0 commit comments

Comments
 (0)