-
Notifications
You must be signed in to change notification settings - Fork 24
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
Tests for capture checking #67
Comments
The following minimization gives the correct error, even if the error message could certainly be imrpoved: import scala.util.boundary, boundary.{Label, break}
class Async
class Future[+T]:
this: Future[T]^ =>
def await(using Async^): T = ???
object Future:
def apply[T](op: Async^ ?=> T)(using Async): Future[T]^{op} = ???
abstract class Result[+T, +E]
case class Ok[+T](value: T) extends Result[T, Nothing]
case class Err[+E](value: E) extends Result[Nothing, E]
object Result:
extension [T, E](r: Result[T, E])
/** `_.ok` propagates Err to current Label */
def ok(using Label[Err[E]]^): T = r match
case r: Ok[_] => r.value
case err => break(err.asInstanceOf[Err[E]])
def apply[T, E](body: Label[Err[E]]^ ?=> T): Result[T, E] =
boundary:
val result = body
Ok(result)
end Result
def test[T, E](using Async) =
val good1: List[Future[Result[T, E]]] => Future[Result[List[T], E]] = frs =>
Future:
Result:
frs.map(_.await.ok)
val good2: Result[Future[T], E] => Future[Result[T, E]] = rf =>
Future:
Result:
rf.ok.await // OK, Future argument has type Result[T]
def fail3(fr: Future[Result[T, E]]^) =
Result:
Future:
fr.await.ok // error, escaping label from Result We get:
But it does give a weirder error message if the
In this case we get:
And it compiles without errors if |
I think the false positives came because import annotation.capability
object boundary:
@capability final class Label[-T]
/** Abort current computation and instead return `value` as the value of
* the enclosing `boundary` call that created `label`.
*/
def break[T](value: T)(using label: Label[T]): Nothing = ???
def apply[T](body: Label[T] ?=> T): T = ???
end boundary
import boundary.{Label, break}
class Async
class Future[+T]:
this: Future[T]^ =>
def await(using Async^): T = ???
object Future:
def apply[T](op: Async^ ?=> T)(using Async): Future[T]^{op} = ???
abstract class Result[+T, +E]
case class Ok[+T](value: T) extends Result[T, Nothing]
case class Err[+E](value: E) extends Result[Nothing, E]
object Result:
extension [T, E](r: Result[T, E])
/** `_.ok` propagates Err to current Label */
def ok(using Label[Err[E]]): T = r match
case r: Ok[_] => r.value
case err => break(err.asInstanceOf[Err[E]])
transparent inline def apply[T, E](inline body: Label[Err[E]] ?=> T): Result[T, E] =
boundary:
val result = body
Ok(result)
end Result
def test[T, E](using Async) =
val good1: List[Future[Result[T, E]]] => Future[Result[List[T], E]] = frs =>
Future:
Result:
frs.map(_.await.ok)
val good2: Result[Future[T], E] => Future[Result[T, E]] = rf =>
Future:
Result:
rf.ok.await // OK, Future argument has type Result[T]
def fail3(fr: Future[Result[T, E]]^) =
Result:
Future:
fr.await.ok // error, escaping label from Result And that gives the expected error:
I am still not sure why the experiment with actual Gears code inferred Result[Any, Any]. |
I wrote down the relevant parts here. This is code not using any Gears implementation, and should still compile import language.experimental.captureChecking
import scala.annotation.capability
@capability trait Async
object Async:
def blocking[T](body: Async ?=> T): T = ???
object boundary:
@capability final class Label[-T]
/** Abort current computation and instead return `value` as the value of
* the enclosing `boundary` call that created `label`.
*/
def break[T](value: T)(using label: Label[T]): Nothing = ???
def apply[T](body: Label[T] ?=> T): T = ???
end boundary
enum Result[+T, +E]:
case Ok[+T](value: T) extends Result[T, Nothing]
case Err[+E](error: E) extends Result[Nothing, E]
object Result:
import boundary.Label
def apply[T, E](body: Label[Result[T, E]] ?=> T): Result[T, E] =
boundary(Ok(body))
extension [U, E](r: Result[U, E]^)(using Label[Err[E]])
def ok: U = r match
case Err(value) => boundary.break[Err[E]](Err(value))
case Ok(value) => value
class Future[+T]():
def await(using Async): T = ???
// def awaitResult(using Async): scala.util.Try[T] = ???
object Future:
def apply[T](body: Async ?=> T)(using spawn: Async): Future[T]^{body} = ???
def main() =
import Result.*
Async.blocking: async ?=>
def fail3[T, E](fr: Future[Result[T, E]]^) =
Result: label ?=>
val f: Future[T]^{async, fr, label} = Future: fut ?=>
fr.await.ok(using label) // error, escaping label from Result
f
|
It seems that changing object Result:
def apply[T, E](body: Label[Result[T, E]] ?=> T): Result[T, E] = to object Result:
def apply[T, E](body: Label[Err[E]] ?=> T): Result[T, E] = will make the compiler emit the error you had. We do need to have a |
In #20244 I have a minimization along these lines. But I don't get the error you see, for me it's still a "local reference leaks into outer capture set" message. |
Does compiling the minimization at #67 (comment) give you the "local reference leaks" error? I'm getting no compiler errors using |
That minimization also compiles for me without errors and a Result[Any, Any] label. I chased it down to the following difference: If we write def fail3[T, E](fr: Future[Result[T, E]]^) =
Result: label ?=>
val f = Future: fut ?=>
fr.await.ok // error, escaping label from Result
f
Result: label ?=> But if we drop the def fail3[T, E](fr: Future[Result[T, E]]^) =
Result:
val f = Future: fut ?=>
fr.await.ok // error, escaping label from Result
f
-- Error: effect-swaps-2.scala:46:6 --------------------------------------------
46 | Result: // contextual$2 ?=>
| ^^^^^^
|local reference contextual$2 from (using contextual$2:
| boundary.Label[
| Result[box Future[box T^?]^{fr, contextual$2, contextual$2}, box E^?]]^
|): box Future[box T^?]^{fr, contextual$2, contextual$2} leaks into outer capture set of type parameter T of method apply in object Result
1 error found I |
And it turns out that difference is already present after typer. With explicit label, it infers |
When we get capture checked Gears it would be good that the following works as expected:
On the other hand, the following case should fail:
This fails because it is expanded to
and the
Future
block has typeFuture[T]^{async, lbl}
.A transform having that type can be constructed but would be useless since we take a future of a value:
The difference between
good2
andfail3
is that Result is strict and Future is not.The text was updated successfully, but these errors were encountered: