Yichen Xu
Yichen Xu
after rebasing this on #23324, stdlib capture checks.
An unsound snippet that should not have compiled: ```scala import language.experimental.captureChecking // Some capabilities that should be used locally trait Async: // some method def read(): Unit def usingAsync[X](op: Async^...
The reach capability appears in the expression `x.get.read()`, since `x`'s type is `Box[Async^]` and the type parameter of `Box` is covariant, it gets reach-refined to `Box[Async^{x*}]`. I have a modified...
could be a duplicate of #20272
I am assuming that we do want to hide boxes *completely* from the user. In other words, boxes are internal constructs, and only for those who really curious about what...
Instantiating type variables with a cap does not make sense, unless the cap is interpreted as an existential bound at the class level, somehow. I see here too an interaction...
I could try turning them off and see what happens. I think the freshness level is coming into play here. One thing that seems a bit interesting to me is...
I think we should replace all `ResultCap`s with `Fresh`s in the result of an application, regardless of the variance. Since what the signature actually says is: ``` empty: exists c....
Those will be caps at double-flip occurrences, then. Feels that it should be fine.
Soundness issue found: ```scala import language.experimental.captureChecking // ok def runOps(ops: List[() => Unit]): Unit = ops.foreach(op => op()) // ok def delayedRunOps(ops: List[() => Unit]): () ->{ops*} Unit = ()...