Skip to content

Make reach refinement shallow #19171

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

Merged
merged 3 commits into from
Dec 6, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 47 additions & 16 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -236,35 +236,66 @@ extension (tp: Type)
* (2) all covariant occurrences of cap replaced by `x*`, provided there
* are no occurrences in `T` at other variances. (1) is standard, whereas
* (2) is new.
*
* For (2), multiple-flipped covariant occurrences of cap won't be replaced.
* In other words,
*
* - For xs: List[File^] ==> List[File^{xs*}], the cap is replaced;
* - while f: [R] -> (op: File^ => R) -> R remains unchanged.
*
* Without this restriction, the signature of functions like withFile:
*
* (path: String) -> [R] -> (op: File^ => R) -> R
*
* could be refined to
*
* (path: String) -> [R] -> (op: File^{withFile*} => R) -> R
*
* which is clearly unsound.
*
* Why is this sound? Covariant occurrences of cap must represent capabilities
* that are reachable from `x`, so they are included in the meaning of `{x*}`.
* At the same time, encapsulation is still maintained since no covariant
* occurrences of cap are allowed in instance types of type variables.
*/
def withReachCaptures(ref: Type)(using Context): Type =
object narrowCaps extends TypeMap:
class CheckContraCaps extends TypeTraverser:
var ok = true
def apply(t: Type) = t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal =>
if variance > 0 then
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
else
ok = false
t
case _ => t match
case t @ CapturingType(p, cs) =>
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
case t =>
mapOver(t)
def traverse(t: Type): Unit =
if ok then
t match
case CapturingType(_, cs) if cs.isUniversal && variance <= 0 =>
ok = false
case _ =>
traverseChildren(t)

object narrowCaps extends TypeMap:
/** Has the variance been flipped at this point? */
private var isFlipped: Boolean = false

def apply(t: Type) =
val saved = isFlipped
try
if variance <= 0 then isFlipped = true
t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
case _ => t match
case t @ CapturingType(p, cs) =>
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
case t =>
mapOver(t)
finally isFlipped = saved
ref match
case ref: CaptureRef if ref.isTrackableRef =>
val tp1 = narrowCaps(tp)
if narrowCaps.ok then
val checker = new CheckContraCaps
checker.traverse(tp)
if checker.ok then
val tp1 = narrowCaps(tp)
if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
tp1
else
capt.println(i"cannot narrow $tp of $ref to $tp1")
capt.println(i"cannot narrow $tp of $ref")
tp
case _ =>
tp
Expand Down
18 changes: 18 additions & 0 deletions tests/neg-custom-args/captures/refine-reach-shallow.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
import language.experimental.captureChecking
trait IO
def test1(): Unit =
val f: IO^ => IO^ = x => x
val g: IO^ => IO^{f*} = f // error
def test2(): Unit =
val f: [R] -> (IO^ => R) -> R = ???
val g: [R] -> (IO^{f*} => R) -> R = f // error
def test3(): Unit =
val f: [R] -> (IO^ -> R) -> R = ???
val g: [R] -> (IO^{f*} -> R) -> R = f // error
def test4(): Unit =
val xs: List[IO^] = ???
val ys: List[IO^{xs*}] = xs // ok
def test5(): Unit =
val f: [R] -> (IO^ -> R) -> IO^ = ???
val g: [R] -> (IO^ -> R) -> IO^{f*} = f // ok
val h: [R] -> (IO^{f*} -> R) -> IO^ = f // error
8 changes: 8 additions & 0 deletions tests/neg-custom-args/captures/refine-withFile.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
import language.experimental.captureChecking

trait File
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
def main(): Unit =
val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error
val leaked = g[File^{f*}]("test")(f => f) // boom