Existential Capabilities #20566
Merged
Existential Capabilities #20566
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
scalac is crashing on opaque types aliasing a capability type import language.experimental.captureChecking
trait A extends caps.Capability
object O:
opaque type B = AStack trace
|
|
Strange compiler error on this code import language.experimental.captureChecking
trait Suspend:
type Suspension
def resume(s: Suspension): Unit
trait Async(val support: Suspend) extends caps.Capability
class CancelSuspension(ac: Async, suspension: ac.support.Suspension):
ac.support.resume(suspension)gives -- [E007] Type Mismatch Error: Test.scala:11:20 --------------------------------
11 | ac.support.resume(suspension)
| ^^^^^^^^^^
|Found: ((CancelSuspension.this.ac : Async^)^{CancelSuspension.this.suspension*})#
| support.Suspension
|Required: CancelSuspension.this.ac.support.Suspension
|
| longer explanation available when compiling with `-explain`
1 error foundThe error doesn't come up if |
odersky
changed the title
|
Reach capabilities being widened into //> using scala 3.5.1-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
class Box[T](items: Seq[T^]):
def getOne: T^{items*} = ???
object Box:
def getOne[T](items: Seq[T^]): T^{items*} =
Box(items).getOnegives -- Error: /tmp/tmp.yIHCJZJOce/test.scala:9:15 ----------------------------------
9 | Box(items).getOne
| ^^^^^^^^^^^^^^^^^
|The expression's type (box T^?)^ is not allowed to capture the root capability `cap`.
|This usually means that a capability persists longer than its allowed lifetime.
1 error found |
|
@natsukagami Last problem should be fixed now. |
odersky
force-pushed
the
cc-ex-2
branch
4 times, most recently
from
0e57d54
to
60b0486
Compare
|
Similar to the above, simplified from //> using scala 3.5.1-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Future[+T]:
def await: T
trait Channel[T]:
def read(): Either[Nothing, T]
class Collector[T](val futures: Seq[Future[T]^]):
val results: Channel[Future[T]^{futures*}] = ???
end Collector
extension [T](fs: Seq[Future[T]^])
def awaitAll =
val collector = Collector(fs)
// val ch = collector.results // also errors
val fut: Future[T]^{fs*} = collector.results.read().right.get // found ...^{caps.cap} |
|
@natsukagami I noted that the last example typechecks if the type of collector is given explicitly: val collector: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
= Collector(fs) |
|
An unsound snippet that should not have compiled: import language.experimental.captureChecking
// Some capabilities that should be used locally
trait Async:
// some method
def read(): Unit
def usingAsync[X](op: Async^ => X): X = ???
case class Box[+T](get: T)
def useBoxedAsync(x: Box[Async^]): Unit = x.get.read()
def test(): Unit =
val f: Box[Async^] => Unit = useBoxedAsync
def boom(x: Async^): () ->{f} Unit =
() => f(Box(x))
val leaked = usingAsync[() ->{f} Unit](boom)
leaked() // scope violationFunctions like |
|
@Linyxus I need some more explanations why this is unsound. The typeckecked example is here: @SourceFile("leak-problem.scala") final module class leak-problem$package()
extends Object() {
private[this] type $this = leak-problem$package.type
private def writeReplace(): AnyRef =
new scala.runtime.ModuleSerializationProxy(
classOf[leak-problem$package.type])
def usingAsync[X](op: Async^ => X): X = ???
def useBoxedAsync(x: Box[box Async^]): Unit = x.Async.read()
def test(): Unit =
{
val f: Box[box Async^] => Unit =
{
def $anonfun(x: Box[box Async^]^?): Unit = useBoxedAsync(x)
closure($anonfun)
}
def boom(x: Async^): () ->{f} Unit =
{
def $anonfun(): Unit =
{
f.apply(Box.apply[box Async^{x}](x))
}
closure($anonfun)
}
val leaked: () ->{f} Unit =
usingAsync[box () ->{f} Unit](
{
def $anonfun(x: Async^): () ->{f} Unit = boom(x)
closure($anonfun)
}
)
leaked.apply()
}
}There's not a single reach capability in that program. |
|
The reach capability appears in the expression I have a modified version of this snippet which better shows the problem: import language.experimental.captureChecking
// Some capabilities that should be used locally
trait Async:
// some method
def read(): Unit
def usingAsync[X](op: Async^ => X): X = ???
case class Box[+T](get: T)
def useBoxedAsync(x: Box[Async^]): Unit =
val t0 = x
val t1 = x.get
t1.read()
def test(): Unit =
val f: Box[Async^] => Unit = useBoxedAsync
def boom(x: Async^): () ->{f} Unit =
() => f(Box(x))
val leaked = usingAsync[() ->{f} Unit](boom)
leaked() // scope violationThe tree after cc: def useBoxedAsync(x: Box[box Async^]): Unit =
{
val t0: Box[box Async^{x*}]^? = x
val t1: Async^{x*} = x.Async
t1.read()
} |
odersky
force-pushed
the
cc-ex-2
branch
2 times, most recently
from
d06a5e6
to
8a504aa
Compare
|
Some weird interaction between caps, opaque types and inlines... //> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Async extends caps.Capability:
def group: Int
object Async:
inline def current(using async: Async): async.type = async
opaque type Spawn <: Async = Async
def blocking[T](f: Spawn ?=> T): T = ???
def main() =
Async.blocking:
val a = Async.current.groupgives Making |
|
@natsukagami Should be fixed by latest commit |
//> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Source[+T]
def race[T](@caps.unboxed sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} = race(Seq(src1, src2))this compiles and returns a |
|
@natsukagami Should be fixed by latest commits |
|
Seems to not work with spread parameters //> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Source[+T]
def race[T](@caps.unbox sources: (Source[T]^)*): Source[T]^{sources*} = ???
def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} =
// race(Seq(src1, src2)*) // this fails
race(src1, src2) // this compiles |
The condition on capturing types did not make sense. In a type T^{} with an empty capture set
`T` can still be a type variable that's instantiated to a type with a capture set. Instead,
T^cs is always pure if T is always pure. For instance `List[T]^{p}` is always pure. That's
important in the context of the standard library, where such a type usually results from
an instantiation of a type variable such as `C[T]^{p}`.
Step1: refactor The logic was querying the original types of trees, but we want the rechecked types instead.
Step 2: Change the logic. The previous one was unsound. The new logic is a bot too conservative. I left comments in tests where it could be improved.
Make all operations final methods on Type or CaptureRef
Move extension methods on CaptureRef into CaptureRef itself or into CaptureOps
Previously, only asInstanceOf was excluded.
This reverts commit f1f5a05. # Conflicts: # compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Step 2: Change the logic. The previous one was unsound. The new logic is makes use of the distinction between regular and unboxed parameters.
Fix the capture set computation of a type T @reachCapability where T is not a singleton captureRef. Such types can be the results of typemaps. The capture set in this case should be the deep capture set of T.
Drop the config option that enables it.
Also, fix Seq rechecking so that elements are always box adapted
Capability references in inlined code might end up not being tracked or being redundant. Don't flag this as an error.
Give some explanation if an empty capture set was the result of an under-approximation.
Here it simply requires that you need to give an explicit type to |
Perform bounds checking before checking self types. Checking self types interpolates them, which may give an upper approximation solution that failes subsequent bounds checks. On the other hand, well-formedness checkimng should come after self types checking since otherwise we get spurious "has empty capture set, cannot be tracked" messages.
|
@natsukagami The latest example you have is not supposed to compile. What I could do is add some way to give a hint why it failed: 15 | col.add(Future(() => 25)) // error
| ^^^^^^^^^^^^^^^^
|Found: Future[Int]{val a: (async : Async^)}^{async}
|Required: Future[Int]^{}
|
|Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
|was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set. |
|
@bracevac Your latest problem should be fixed with last commit.
The conformance check was done by the capture checker. And that is run only if the language import is present. So that explains it. But it was still a bug since no error should have been issued. |
|
@natsukagami For the latest example, maybe you could try explicit capture set polymorphism? |
|
@bracevac I think it would be good to get this merged soon. We are getter further and further away from the main branch, in a good way. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The design has changed quite a bit relative to #20470. It is written up as a doc comment on object cc.Existentials.