Skip to content

Commit 09e4e0f

Browse files
oderskyodersky
committed
Use a different criterion to plug unsoundness for reach capabilities
Enforce an analogous restriction to the one for creating reach capabilities for all values. The type of a value cannot both have a reach capability with variance >= 0 and at the same time a universal capability with variance <= 0.
1 parent fa7680b commit 09e4e0f

File tree

8 files changed

+78
-43
lines changed

8 files changed

+78
-43
lines changed

‎compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

Lines changed: 66 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -249,6 +249,67 @@ class CheckCaptures extends Recheck, SymTransformer:
249249
else i"references $cs1$cs1description are not all",
250250
pos, provenance)
251251

252+
def showRef(ref: CaptureRef)(using Context): String =
253+
ctx.printer.toTextCaptureRef(ref).show
254+
255+
// Uses 4-space indent as a trial
256+
def checkReachCapsIsolated(tpe: Type, pos: SrcPos)(using Context): Unit =
257+
258+
object checker extends TypeTraverser:
259+
var seenRefs: Map[Boolean, Int] = Map.empty
260+
var seenReach: CaptureRef | Null = null
261+
def traverse(tp: Type) =
262+
tp match
263+
case CapturingType(parent, refs) =>
264+
traverse(parent)
265+
for ref <- refs.elems do
266+
if ref.isReach && !ref.stripReach.isInstanceOf[TermParamRef]
267+
|| ref.isRootCapability
268+
then
269+
val isReach = ref.isReach
270+
def register() =
271+
seenRefs = seenRefs.updated(isReach, variance)
272+
seenReach = ref
273+
seenRefs.get(isReach) match
274+
case None => register()
275+
case Some(v) => if v != 0 && variance == 0 then register()
276+
case _ =>
277+
traverseChildren(tp)
278+
279+
checker.traverse(tpe)
280+
//println(i"check $tpe = ${checker.seenRefs}")
281+
if checker.seenRefs.size == 2
282+
&& checker.seenRefs(true) >= 0
283+
&& checker.seenRefs(false) <= 0
284+
then
285+
report.error(
286+
em"""Reach capability ${showRef(checker.seenReach.nn)} and universal capability cap cannot both
287+
|appear in the type $tpe of this expression""",
288+
pos)
289+
290+
end checkReachCapsIsolated
291+
292+
// Uses 4-space indent as a trial
293+
def checkReachCapsOnlyCovariant(tpe: Type, pos: SrcPos)(using Context): Unit =
294+
val checker = new TypeTraverser:
295+
def traverse(tp: Type) =
296+
tp match
297+
case CapturingType(parent, refs) =>
298+
traverse(parent)
299+
if variance <= 0 then
300+
for ref <- refs.elems do
301+
if ref.isReach then
302+
val prefix = if variance == 0 then "in" else "contra"
303+
report.error(
304+
em"""Reach capability ${showRef(ref)} is not allowed to appear in ${prefix}variant position
305+
|in argument type $tpe""",
306+
pos
307+
)
308+
case _ =>
309+
traverseChildren(tp)
310+
checker.traverse(tpe)
311+
end checkReachCapsOnlyCovariant
312+
252313
/** The current environment */
253314
private val rootEnv: Env = inContext(ictx):
254315
Env(defn.RootClass, EnvKind.Regular, CaptureSet.empty, null)
@@ -456,27 +517,8 @@ class CheckCaptures extends Recheck, SymTransformer:
456517
// Uses 4-space indent as a trial
457518
override def recheckArg(arg: Tree, pt: Type)(using Context) =
458519
val argType = recheck(arg, pt)
459-
460-
def checkOnlyCovariantReachCaps = new TypeTraverser:
461-
def traverse(tp: Type) =
462-
tp match
463-
case CapturingType(parent, refs) =>
464-
traverse(parent)
465-
if variance <= 0 then
466-
for ref <- refs.elems do
467-
if ref.isReach then
468-
val prefix = if variance == 0 then "in" else "contra"
469-
report.error(
470-
em"""Reach capability ${ctx.printer.toTextCaptureRef(ref).show} is not allowed to appear in ${prefix}variant position
471-
|in argument type ${argType.widen}""",
472-
arg.srcPos
473-
)
474-
case _ =>
475-
traverseChildren(tp)
476-
477-
checkOnlyCovariantReachCaps.traverse(argType.widen)
520+
//checkReachCapsOnlyCovariant(argType.widen, arg.srcPos)
478521
argType
479-
end recheckArg
480522

481523
private def isDistinct(xs: List[Type]): Boolean = xs match
482524
case x :: xs1 => xs1.isEmpty || !xs1.contains(x) && isDistinct(xs1)
@@ -804,8 +846,10 @@ class CheckCaptures extends Recheck, SymTransformer:
804846
report.error(ex.getMessage.nn)
805847
tree.tpe
806848
finally curEnv = saved
807-
if tree.isTerm && !pt.isBoxedCapturing then
808-
markFree(res.boxedCaptureSet, tree.srcPos)
849+
if tree.isTerm then
850+
checkReachCapsIsolated(res.widen, tree.srcPos)
851+
if !pt.isBoxedCapturing then
852+
markFree(res.boxedCaptureSet, tree.srcPos)
809853
res
810854

811855
override def recheckFinish(tpe: Type, tree: Tree, pt: Type)(using Context): Type =

‎tests/neg-custom-args/captures/i15749a.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,4 @@ def test =
1919
def forceWrapper[A](mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
2020
// Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
2121
// `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
22-
strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // error
22+
strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error

‎tests/neg-custom-args/captures/reaches.check

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,3 @@
4141
| Required: File^{id*}
4242
|
4343
| longer explanation available when compiling with `-explain`
44-
-- Error: tests/neg-custom-args/captures/reaches.scala:67:10 -----------------------------------------------------------
45-
67 | ps.map((x, y) => compose(x, y)) // error
46-
| ^^^^^^^^^^^^^^^^^^^^^^
47-
|Reach capability ps* is not allowed to appear in contravariant position
48-
|in argument type (x$1: (box (x$0: A^?) ->{ps*} A^?, box (x$0: A^?) ->{ps*} A^?)^?) ->? box (x$0: A^?) ->{ps*} A^?

‎tests/neg-custom-args/captures/reaches.scala

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -60,10 +60,3 @@ def attack2 =
6060
val f1: File^{id*} = id(f) // error
6161
f1
6262

63-
def compose[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
64-
z => g(f(z))
65-
66-
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
67-
ps.map((x, y) => compose(x, y)) // error
68-
// unfortunately this does not work. x and y have type A ->{ps*} A, and that
69-
// type is not allowed to appear contra-variantly in the argument

‎tests/neg-custom-args/captures/refine-withFile.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
import language.experimental.captureChecking
2+
import scala.concurrent.duration.DurationConversions.spanConvert
23

34
trait File
45
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
56
def main(): Unit =
67
val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
78
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error
8-
val leaked = g[File^{f*}]("test")(f => f) // error
9+
val leaked = g[File^{f*}]("test")(f => f)

‎tests/neg/unsound-reach-2.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,8 @@ def bad(): Unit =
1818

1919
var escaped: File^{backdoor*} = null
2020
withFile("hello.txt"): f =>
21-
boom.use(f):
22-
new Consumer[File^{backdoor*}]: // error
21+
boom.use(f): // error
22+
new Consumer[File^{backdoor*}]:
2323
def apply(f1: File^{backdoor*}) =
2424
escaped = f1
2525

‎tests/neg/unsound-reach.check

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
1-
-- Error: tests/neg/unsound-reach.scala:18:17 --------------------------------------------------------------------------
1+
-- Error: tests/neg/unsound-reach.scala:18:9 ---------------------------------------------------------------------------
22
18 | boom.use(f): (f1: File^{backdoor*}) => // error
3-
| ^
4-
| Reach capability backdoor* is not allowed to appear in contravariant position
5-
| in argument type (f1: box File^{backdoor*}) ->? Unit
6-
19 | escaped = f1
3+
| ^^^^^^^^
4+
| Reach capability backdoor* and universal capability cap cannot both
5+
| appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression

‎tests/pos-custom-args/captures/reaches.scala

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,9 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
3535
def compose2[A, B, C](f: A => B, g: B => C): A => C =
3636
z => g(f(z))
3737

38+
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
39+
ps.map((x, y) => compose1(x, y))
40+
3841
@annotation.capability class IO
3942

4043
def test(io: IO) =

0 commit comments

Comments
 (0)