Skip to content

Commit 6d9dbf6

Browse files
oderskyodersky
committed
Tighten subsumption checking of Fresh instances
Fresh instances cannot subsume TermParamRefs since that would be a level violation.
1 parent d8a8084 commit 6d9dbf6

16 files changed

+85
-16
lines changed

‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,11 @@ trait CaptureRef extends TypeProxy, ValueType:
256256
|| this.match
257257
case root.Fresh(hidden) =>
258258
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
259-
|| !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
259+
|| !y.stripReadOnly.isCap
260+
&& !yIsExistential
261+
&& !y.isInstanceOf[TermParamRef]
262+
&& canAddHidden
263+
&& vs.addHidden(hidden, y)
260264
case x @ root.Result(binder) =>
261265
val result = y match
262266
case y @ root.Result(_) => vs.unify(x, y)

‎tests/neg-custom-args/captures/capt-test.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ def handle[E <: Exception, R <: Top](op: (CT[E] @retains(caps.cap)) => R)(handl
2020
catch case ex: E => handler(ex)
2121

2222
def test: Unit =
23-
val b = handle[Exception, () => Nothing] { // error
23+
val b = handle[Exception, () => Nothing] { // error // error
2424
(x: CanThrow[Exception]) => () => raise(new Exception)(using x)
2525
} {
2626
(ex: Exception) => ???

‎tests/neg-custom-args/captures/i15049.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,4 @@ class Foo:
77
def Test: Unit =
88
val f = new Foo
99
f.withSession(s => s).request // error
10-
f.withSession[Session^](t => t) // error
10+
f.withSession[Session^](t => t) // error // error

‎tests/neg-custom-args/captures/i16226.check

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:13:4 ----------------------------------------
2+
13 | (ref1, f1) => map[A, B](ref1, f1) // error
3+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
| Found: (ref1: LazyRef[box A^?]{val elem: () ->{cap, fresh} A^?}^{io}, f1: (x$0: A^?) => B^?) ->?
5+
| LazyRef[box B^?]{val elem: () ->{localcap} B^?}^{f1, ref1}
6+
| Required: (ref1: LazyRef[A]^{io}, f1: A => B) ->{fresh} LazyRef[B]^{fresh}
7+
|
8+
| longer explanation available when compiling with `-explain`
9+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ----------------------------------------
10+
15 | (ref1, f1) => map[A, B](ref1, f1) // error
11+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12+
| Found: (ref1: LazyRef[box A^?]{val elem: () ->{cap, fresh} A^?}^{io}, f1: (x$0: A^?) => B^?) ->?
13+
| LazyRef[box B^?]{val elem: () ->{localcap} B^?}^{f1, ref1}
14+
| Required: (ref: LazyRef[A]^{io}, f: A => B) ->{fresh} LazyRef[B]^{localcap}
15+
|
16+
| Note that the existential capture root in LazyRef[B]^
17+
| cannot subsume the capability f1.type since that capability is not a SharedCapability
18+
|
19+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/i16226.scala

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
class Cap extends caps.Capability
2+
3+
class LazyRef[T](val elem: () => T):
4+
val get: () ->{elem} T = elem
5+
def map[U](f: T => U): LazyRef[U]^{f, this} =
6+
new LazyRef(() => f(elem()))
7+
8+
def map[A, B](ref: LazyRef[A]^, f: A => B): LazyRef[B]^{f, ref} =
9+
new LazyRef(() => f(ref.elem()))
10+
11+
def main(io: Cap) = {
12+
def mapc[A, B]: (LazyRef[A]^{io}, A => B) => LazyRef[B]^ =
13+
(ref1, f1) => map[A, B](ref1, f1) // error
14+
def mapd[A, B]: (ref: LazyRef[A]^{io}, f: A => B) => LazyRef[B]^ =
15+
(ref1, f1) => map[A, B](ref1, f1) // error
16+
}

‎tests/neg-custom-args/captures/i21401.check

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,17 @@
44
| Type variable T of object Boxed cannot be instantiated to box IO^ since
55
| that type captures the root capability `cap`.
66
-- Error: tests/neg-custom-args/captures/i21401.scala:15:18 ------------------------------------------------------------
7-
15 | val a = usingIO[IO^](x => x) // error
7+
15 | val a = usingIO[IO^](x => x) // error // error
88
| ^^^
99
| Type variable R of method usingIO cannot be instantiated to box IO^ since
1010
| that type captures the root capability `cap`.
11+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:15:23 ---------------------------------------
12+
15 | val a = usingIO[IO^](x => x) // error // error
13+
| ^^^^^^
14+
| Found: (x: IO^) ->? box IO^{x}
15+
| Required: (x: IO^) ->{fresh} box IO^{fresh}
16+
|
17+
| longer explanation available when compiling with `-explain`
1118
-- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
1219
16 | val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
1320
| ^^^

‎tests/neg-custom-args/captures/i21401.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ def mkRes(x: IO^): Res =
1212
val op1: Boxed[IO^] -> R = op
1313
op1(Boxed[IO^](x)) // error
1414
def test2() =
15-
val a = usingIO[IO^](x => x) // error
15+
val a = usingIO[IO^](x => x) // error // error
1616
val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
1717
val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
1818
val y: IO^{x*} = x.unbox // was error

‎tests/neg-custom-args/captures/reaches.check

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,13 @@
4444
| ^
4545
| Type variable A of constructor Id cannot be instantiated to box () => Unit since
4646
| that type captures the root capability `cap`.
47+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:59:27 --------------------------------------
48+
59 | val id: File^ -> File^ = x => x // error
49+
| ^^^^^^
50+
| Found: (x: File^) ->? File^{x}
51+
| Required: (x: File^) -> File^{fresh}
52+
|
53+
| longer explanation available when compiling with `-explain`
4754
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:38 --------------------------------------
4855
62 | val leaked = usingFile[File^{id*}]: f => // error // error
4956
| ^

‎tests/neg-custom-args/captures/reaches.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ def test =
5656
id(() => f.write()) // was error
5757

5858
def attack2 =
59-
val id: File^ -> File^ = x => x
59+
val id: File^ -> File^ = x => x // error
6060
// val id: File^ -> File^{fresh}
6161

6262
val leaked = usingFile[File^{id*}]: f => // error // error

‎tests/neg-custom-args/captures/refine-reach-shallow.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import language.experimental.captureChecking
22
trait IO
33
def test1(): Unit =
4-
val f: IO^ => IO^ = x => x
4+
val f: IO^ => IO^ = x => x // error
55
val g: IO^ => IO^{f*} = f // error
66
def test2(): Unit =
77
val f: [R] -> (IO^ => R) -> R = ???

‎tests/neg-custom-args/captures/scoped-caps.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ def test(io: Object^): Unit =
99
val _: (x: A^) -> B^ = g // error
1010
val _: A^ -> B^ = f // error
1111
val _: A^ -> B^ = g
12-
val _: A^ -> B^ = x => g(x) // should be error, since g is pure, g(x): B^{x} , which does not match B^{fresh}
12+
val _: A^ -> B^ = x => g(x) // error, since g is pure, g(x): B^{x} , which does not match B^{fresh}
1313
val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
1414

1515
val h: S -> B^ = ???
@@ -20,9 +20,9 @@ def test(io: Object^): Unit =
2020
val _: (x: S) -> B^ = j
2121
val _: (x: S) -> B^ = x => j(x)
2222
val _: S -> B^ = j // error
23-
val _: S -> B^ = x => j(x) // should be error
23+
val _: S -> B^ = x => j(x) // error
2424

2525
val g2: A^ => B^ = ???
26-
val _: A^ => B^ = x => g2(x) // should be error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
26+
val _: A^ => B^ = x => g2(x) // error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
2727
val g3: A^ => B^ = ???
2828
val _: A^{io} => B^ = x => g3(x) // ok, now g3(x): B^{g3, x}, which is widened to B^{g3, io}

‎tests/neg-custom-args/captures/try.check

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,17 @@
11
-- Error: tests/neg-custom-args/captures/try.scala:23:28 ---------------------------------------------------------------
2-
23 | val a = handle[Exception, CanThrow[Exception]] { // error
2+
23 | val a = handle[Exception, CanThrow[Exception]] { // error // error
33
| ^^^^^^^^^^^^^^^^^^^
44
| Type variable R of method handle cannot be instantiated to box CT[Exception]^ since
55
| that type captures the root capability `cap`.
6+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:23:49 ------------------------------------------
7+
23 | val a = handle[Exception, CanThrow[Exception]] { // error // error
8+
| ^
9+
| Found: (x: CT[Exception]^) ->? box CT[Exception]^{x}
10+
| Required: (x: CT[Exception]^) ->{fresh} box CT[Exception]^{fresh}
11+
24 | (x: CanThrow[Exception]) => x
12+
25 | }{
13+
|
14+
| longer explanation available when compiling with `-explain`
615
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:29:43 ------------------------------------------
716
29 | val b = handle[Exception, () -> Nothing] { // error
817
| ^

‎tests/neg-custom-args/captures/try.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ def handle[E <: Exception, R <: Top](op: CT[E]^ => R)(handler: E => R): R =
2020
catch case ex: E => handler(ex)
2121

2222
def test =
23-
val a = handle[Exception, CanThrow[Exception]] { // error
23+
val a = handle[Exception, CanThrow[Exception]] { // error // error
2424
(x: CanThrow[Exception]) => x
2525
}{
2626
(ex: Exception) => ???

‎tests/neg-custom-args/captures/widen-reach.check

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,13 @@
33
| ^^^^^^^^
44
| Type variable T of trait Foo cannot be instantiated to IO^ since
55
| that type captures the root capability `cap`.
6+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:9:24 -----------------------------------
7+
9 | val foo: IO^ -> IO^ = x => x // error // error
8+
| ^^^^^^
9+
| Found: (x: IO^) ->? IO^{x}
10+
| Required: (x: IO^) -> IO^{fresh}
11+
|
12+
| longer explanation available when compiling with `-explain`
613
-- Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 -------------------------------------------------------
714
13 | val y2: IO^ -> IO^ = y1.foo // error
815
| ^^^^^^
@@ -14,7 +21,7 @@
1421
| Local reach capability x* leaks into capture scope of method test.
1522
| To allow this, the parameter x should be declared with a @use annotation
1623
-- [E164] Declaration Error: tests/neg-custom-args/captures/widen-reach.scala:9:6 --------------------------------------
17-
9 | val foo: IO^ -> IO^ = x => x // error
24+
9 | val foo: IO^ -> IO^ = x => x // error // error
1825
| ^
1926
| error overriding value foo in trait Foo of type IO^ -> box IO^;
2027
| value foo of type IO^ -> IO^ has incompatible type

‎tests/neg-custom-args/captures/widen-reach.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ trait Foo[+T]:
66
val foo: IO^ -> T
77

88
trait Bar extends Foo[IO^]: // error
9-
val foo: IO^ -> IO^ = x => x // error
9+
val foo: IO^ -> IO^ = x => x // error // error
1010

1111
def test(x: Foo[IO^]): Unit =
1212
val y1: Foo[IO^{x*}] = x

‎tests/pos-custom-args/captures/i16226.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
class Cap extends caps.Capability
1+
class Cap extends caps.SharedCapability
22

33
class LazyRef[T](val elem: () => T):
44
val get: () ->{elem} T = elem
@@ -9,6 +9,6 @@ def map[A, B](ref: LazyRef[A]^, f: A => B): LazyRef[B]^{f, ref} =
99
new LazyRef(() => f(ref.elem()))
1010

1111
def main(io: Cap) = {
12-
def mapd[A, B]: (LazyRef[A]^{io}, A => B) => LazyRef[B]^ =
12+
def mapd[A, B]: (ref: LazyRef[A]^{io}, f: A ->{io} B) => LazyRef[B]^ =
1313
(ref1, f1) => map[A, B](ref1, f1)
1414
}

0 commit comments

Comments
 (0)