Skip to content

Commit

Permalink
Drop @unbox annotation
Browse files Browse the repository at this point in the history
  • Loading branch information
odersky committed Oct 14, 2024
1 parent 16f86f0 commit 1836fb3
Show file tree
Hide file tree
Showing 19 changed files with 42 additions and 59 deletions.
5 changes: 0 additions & 5 deletions library/src/scala/caps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -52,11 +52,6 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
*/
final class untrackedCaptures extends annotation.StaticAnnotation

/** This should go into annotations. For now it is here, so that we
* can experiment with it quickly between minor releases
*/
final class unbox extends annotation.StaticAnnotation

object unsafe:

extension [T](x: T)
Expand Down
3 changes: 1 addition & 2 deletions tests/neg-custom-args/captures/i15749a.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import caps.cap
import caps.unbox

class Unit
object u extends Unit
Expand All @@ -18,7 +17,7 @@ def test =

def force[A](thunk: Unit ->{cap} A): A = thunk(u)

def forceWrapper[A](@unbox mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
def forceWrapper[A](mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
// Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
// `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work
8 changes: 4 additions & 4 deletions tests/neg-custom-args/captures/i21614.check
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:9:33 ----------------------------------------
9 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:8:33 ----------------------------------------
8 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
| ^
| Found: (f : F^)
| Required: File^
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:12 ---------------------------------------
12 | files.map(new Logger(_)) // error, Q: can we improve the error message?
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:11:12 ---------------------------------------
11 | files.map(new Logger(_)) // error, Q: can we improve the error message?
| ^^^^^^^^^^^^^
| Found: Logger{val f: (_$1 : File^{files*})}^
| Required: Logger{val f: File^?}^?
Expand Down
5 changes: 2 additions & 3 deletions tests/neg-custom-args/captures/i21614.scala
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
import language.experimental.captureChecking
import caps.Capability
import caps.unbox

trait File extends Capability
class Logger(f: File^) extends Capability // <- will work if we remove the extends clause

def mkLoggers1[F <: File^](@unbox files: List[F]): List[Logger^] =
def mkLoggers1[F <: File^](files: List[F]): List[Logger^] =
files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?

def mkLoggers2(@unbox files: List[File^]): List[Logger^] =
def mkLoggers2(files: List[File^]): List[Logger^] =
files.map(new Logger(_)) // error, Q: can we improve the error message?
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/leak-problem-2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ import language.experimental.captureChecking

trait Source[+T]

def race[T](@caps.unbox sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
def race[T](sources: Seq[Source[T]^]): Source[T]^{sources*} = ???

def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{}
= race(Seq(src1, src2)) // error
Expand Down
36 changes: 18 additions & 18 deletions tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:22:11 --------------------------------------
22 | cur = (() => f.write()) :: Nil // error
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:21:11 --------------------------------------
21 | cur = (() => f.write()) :: Nil // error
| ^^^^^^^^^^^^^^^^^^^^^^^
| Found: List[box () ->{f} Unit]
| Required: List[box () ->{xs*} Unit]
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:33:7 ---------------------------------------
33 | (() => f.write()) :: Nil // error
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:32:7 ---------------------------------------
32 | (() => f.write()) :: Nil // error
| ^^^^^^^^^^^^^^^^^^^^^^^
| Found: List[box () ->{f} Unit]
| Required: box List[box () ->{xs*} Unit]^?
Expand All @@ -15,40 +15,40 @@
| cannot be included in outer capture set {xs*} of value cur
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/reaches.scala:38:31 -----------------------------------------------------------
38 | val next: () => Unit = cur.head // error
-- Error: tests/neg-custom-args/captures/reaches.scala:37:31 -----------------------------------------------------------
37 | val next: () => Unit = cur.head // error
| ^^^^^^^^
| The expression's type box () => Unit is not allowed to capture the root capability `cap`.
| This usually means that a capability persists longer than its allowed lifetime.
-- Error: tests/neg-custom-args/captures/reaches.scala:45:35 -----------------------------------------------------------
45 | val next: () => Unit = cur.get.head // error
-- Error: tests/neg-custom-args/captures/reaches.scala:44:35 -----------------------------------------------------------
44 | val next: () => Unit = cur.get.head // error
| ^^^^^^^^^^^^
| The expression's type box () => Unit is not allowed to capture the root capability `cap`.
| This usually means that a capability persists longer than its allowed lifetime.
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:2 ---------------------------------------
53 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:52:2 ---------------------------------------
52 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
| ^
| Found: box () => Unit
| Required: () => Unit
|
| Note that box () => Unit cannot be box-converted to () => Unit
| since at least one of their capture sets contains the root capability `cap`
54 | usingFile: f =>
55 | id(() => f.write())
53 | usingFile: f =>
54 | id(() => f.write())
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 --------------------------------------
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:61:27 --------------------------------------
61 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
| ^^^^^
| Found: File^{f}
| Required: File^{id*}
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/reaches.scala:61:31 -----------------------------------------------------------
61 | val leaked = usingFile[File^{id*}]: f => // error
-- Error: tests/neg-custom-args/captures/reaches.scala:60:31 -----------------------------------------------------------
60 | val leaked = usingFile[File^{id*}]: f => // error
| ^^^
| id* cannot be tracked since its capture set is empty
-- Error: tests/neg-custom-args/captures/reaches.scala:62:18 -----------------------------------------------------------
62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
-- Error: tests/neg-custom-args/captures/reaches.scala:61:18 -----------------------------------------------------------
61 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
| ^^^
| id* cannot be tracked since its capture set is empty
5 changes: 2 additions & 3 deletions tests/neg-custom-args/captures/reaches.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import caps.unbox
class File:
def write(): Unit = ???

Expand All @@ -11,7 +10,7 @@ class Ref[T](init: T):
def get: T = x
def set(y: T) = { x = y }

def runAll0(@unbox xs: List[Proc]): Unit =
def runAll0(xs: List[Proc]): Unit =
var cur: List[() ->{xs*} Unit] = xs
while cur.nonEmpty do
val next: () ->{xs*} Unit = cur.head
Expand All @@ -21,7 +20,7 @@ def runAll0(@unbox xs: List[Proc]): Unit =
usingFile: f =>
cur = (() => f.write()) :: Nil // error

def runAll1(@unbox xs: List[Proc]): Unit =
def runAll1(xs: List[Proc]): Unit =
val cur = Ref[List[() ->{xs*} Unit]](xs) // OK, by revised VAR
while cur.get.nonEmpty do
val next: () ->{xs*} Unit = cur.get.head
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/spread-problem.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ import language.experimental.captureChecking

trait Source[+T]

def race[T](@caps.unbox sources: (Source[T]^)*): Source[T]^{sources*} = ???
def race[T](sources: (Source[T]^)*): Source[T]^{sources*} = ???

def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} =
race(Seq(src1, src2)*) // error
Expand Down
5 changes: 2 additions & 3 deletions tests/pos-custom-args/captures/dep-reach.scala
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
import caps.unbox
object Test:
class C
type Proc = () => Unit

def f(c: C^, d: C^): () ->{c, d} Unit =
def foo(@unbox xs: Proc*): () ->{xs*} Unit =
def foo(xs: Proc*): () ->{xs*} Unit =
xs.head
val a: () ->{c} Unit = () => ()
val b: () ->{d} Unit = () => ()
Expand All @@ -13,7 +12,7 @@ object Test:

def g(c: C^, d: C^): () ->{c, d} Unit =

def foo(@unbox xs: Seq[() => Unit]): () ->{xs*} Unit =
def foo(xs: Seq[() => Unit]): () ->{xs*} Unit =
xs.head

val a: () ->{c} Unit = () => ()
Expand Down
3 changes: 1 addition & 2 deletions tests/pos-custom-args/captures/i20503.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import language.experimental.captureChecking
import caps.unbox

class List[+A]:
def head: A = ???
Expand All @@ -8,7 +7,7 @@ class List[+A]:
def foreach[U](f: A => U): Unit = ???
def nonEmpty: Boolean = ???

def runOps(@unbox ops: List[() => Unit]): Unit =
def runOps(ops: List[() => Unit]): Unit =
// See i20156, due to limitation in expressiveness of current system,
// we could map over the list of impure elements. OK with existentials.
ops.foreach(op => op())
Expand Down
3 changes: 1 addition & 2 deletions tests/pos-custom-args/captures/reaches.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import caps.unbox

class C
def f(xs: List[C^]) =
Expand All @@ -22,7 +21,7 @@ extension [A](x: A) def :: (xs: List[A]): List[A] = ???

object Nil extends List[Nothing]

def runAll(@unbox xs: List[Proc]): Unit =
def runAll(xs: List[Proc]): Unit =
var cur: List[() ->{xs*} Unit] = xs // OK, by revised VAR
while cur.nonEmpty do
val next: () ->{xs*} Unit = cur.head
Expand Down
3 changes: 1 addition & 2 deletions tests/pos/cc-poly-source-capability.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
import language.experimental.captureChecking
import annotation.experimental
import caps.{CapSet, Capability}
import caps.unbox

@experimental object Test:

Expand All @@ -18,7 +17,7 @@ import caps.unbox

def allListeners: Set[Listener^{X^}] = listeners

def test1(async1: Async, @unbox others: List[Async]) =
def test1(async1: Async, others: List[Async]) =
val src = Source[CapSet^{async1, others*}]
val lst1 = listener(async1)
val lsts = others.map(listener)
Expand Down
3 changes: 1 addition & 2 deletions tests/pos/cc-poly-source.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
import language.experimental.captureChecking
import annotation.experimental
import caps.{CapSet, Capability}
import caps.unbox

@experimental object Test:

Expand All @@ -25,7 +24,7 @@ import caps.unbox
val ls = src.allListeners
val _: Set[Listener^{lbl1, lbl2}] = ls

def test2(@unbox lbls: List[Label^]) =
def test2(lbls: List[Label^]) =
def makeListener(lbl: Label^): Listener^{lbl} = ???
val listeners = lbls.map(makeListener)
val src = Source[CapSet^{lbls*}]
Expand Down
3 changes: 1 addition & 2 deletions tests/pos/gears-probem-1.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import language.experimental.captureChecking
import caps.unbox

trait Future[+T]:
def await: T
Expand All @@ -17,7 +16,7 @@ class Result[+T, +E]:
case class Err[+E](e: E) extends Result[Nothing, E]
case class Ok[+T](x: T) extends Result[T, Nothing]

extension [T](@unbox fs: Seq[Future[T]^])
extension [T](fs: Seq[Future[T]^])
def awaitAll =
val collector//: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
= Collector(fs)
Expand Down
2 changes: 1 addition & 1 deletion tests/pos/i13541.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ object Z:
type Foo[B] = [A] =>> Bar[A, B]
trait Bar[A, B]

given fooUnit[A: F]: Foo[Unit][A] = ???
given fooUnit: [A: F] => Foo[Unit][A] = ???
//given bar[A: F]: Bar[A, Unit] = ???

def f[A: F](using Foo[Unit][A]): Nothing = ???
Expand Down
3 changes: 1 addition & 2 deletions tests/pos/i18699.scala
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
import language.experimental.captureChecking
import caps.unbox

trait Cap:
def use: Int = 42

def test2(@unbox cs: List[Cap^]): Unit =
def test2(cs: List[Cap^]): Unit =
val t0: Cap^{cs*} = cs.head // error
var t1: Cap^{cs*} = cs.head // error
4 changes: 2 additions & 2 deletions tests/pos/i20342.scala
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
class Repo[EC, E](using defaults: RepoDefaults[EC, E])
trait RepoDefaults[EC, E]
object RepoDefaults:
inline given genImmutableRepo[E: DbCodec]: RepoDefaults[E, E] = ???
inline given genRepo[EC: DbCodec, E: DbCodec]: RepoDefaults[EC, E] = ???
inline given genImmutableRepo: [E: DbCodec] => RepoDefaults[E, E] = ???
inline given genRepo: [EC: DbCodec, E: DbCodec] => RepoDefaults[EC, E] = ???

trait DbCodec[E]

Expand Down
3 changes: 1 addition & 2 deletions tests/pos/reach-capability.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
import language.experimental.captureChecking
import annotation.experimental
import caps.Capability
import caps.unbox

@experimental object Test2:

Expand All @@ -12,7 +11,7 @@ import caps.unbox

class Listener

def test2(@unbox lbls: List[Label]) =
def test2(lbls: List[Label]) =
def makeListener(lbl: Label): Listener^{lbl} = ???
val listeners = lbls.map(makeListener) // should work

3 changes: 1 addition & 2 deletions tests/pos/reach-problem.scala
Original file line number Diff line number Diff line change
@@ -1,11 +1,10 @@
import language.experimental.captureChecking
import caps.unbox

class Box[T](items: Seq[T^]):
def getOne: T^{items*} = ???

object Box:
def getOne[T](@unbox items: Seq[T^]): T^{items*} =
def getOne[T](items: Seq[T^]): T^{items*} =
val bx = Box(items)
bx.getOne
/*
Expand Down

0 comments on commit 1836fb3

Please sign in to comment.