Skip to content

Commit 384d32a

Browse files
committed
New scheme to reject root captures
Reject root captures by considering unbox operations. This allows us to ignore root captures buried under type applications.
1 parent eacdc2e commit 384d32a

File tree

12 files changed

+147
-105
lines changed

12 files changed

+147
-105
lines changed

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

+25-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ package dotc
33
package cc
44

55
import core.*
6-
import Types.*, Symbols.*, Contexts.*, Annotations.*
6+
import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
77
import ast.{tpd, untpd}
88
import Decorators.*, NameOps.*
99
import config.Printers.capt
@@ -85,3 +85,27 @@ extension (tp: Type)
8585
isImpure = true).appliedTo(args)
8686
case _ =>
8787
tp
88+
89+
extension (sym: Symbol)
90+
91+
/** Does this symbol allow results carrying the universal capability?
92+
* Currently this is true only for function type applies (since their
93+
* results are unboxed) and `erasedValue` since this function is magic in
94+
* that is allows to conjure global capabilies from nothing (aside: can we find a
95+
* more controlled way to achieve this?).
96+
* But it could be generalized to other functions that so that they can take capability
97+
* classes as arguments.
98+
*/
99+
def allowsRootCapture(using Context): Boolean =
100+
sym == defn.Compiletime_erasedValue
101+
|| defn.isFunctionClass(sym.maybeOwner)
102+
103+
def unboxesResult(using Context): Boolean =
104+
def containsEnclTypeParam(tp: Type): Boolean = tp.strippedDealias match
105+
case tp @ TypeRef(pre: ThisType, _) => tp.symbol.is(Param)
106+
case tp: TypeParamRef => true
107+
case tp: AndOrType => containsEnclTypeParam(tp.tp1) || containsEnclTypeParam(tp.tp2)
108+
case tp: RefinedType => containsEnclTypeParam(tp.parent) || containsEnclTypeParam(tp.refinedInfo)
109+
case _ => false
110+
containsEnclTypeParam(sym.info.finalResultType)
111+
&& !sym.allowsRootCapture

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

+10
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,10 @@ sealed abstract class CaptureSet extends Showable:
172172
def - (ref: CaptureRef)(using Context): CaptureSet =
173173
this -- ref.singletonCaptureSet
174174

175+
def disallowRootCapability(handler: () => Unit)(using Context): this.type =
176+
if isUniversal then handler()
177+
this
178+
175179
def filter(p: CaptureRef => Boolean)(using Context): CaptureSet =
176180
if this.isConst then
177181
val elems1 = elems.filter(p)
@@ -276,6 +280,7 @@ object CaptureSet:
276280
var deps: Deps = emptySet
277281
def isConst = isSolved
278282
def isAlwaysEmpty = false
283+
var addRootHandler: () => Unit = () => ()
279284

280285
private def recordElemsState()(using VarState): Boolean =
281286
varState.getElems(this) match
@@ -296,6 +301,7 @@ object CaptureSet:
296301
def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
297302
if !isConst && recordElemsState() then
298303
elems ++= newElems
304+
if isUniversal then addRootHandler()
299305
// assert(id != 2 || elems.size != 2, this)
300306
(CompareResult.OK /: deps) { (r, dep) =>
301307
r.andAlso(dep.tryInclude(newElems, this))
@@ -312,6 +318,10 @@ object CaptureSet:
312318
else
313319
CompareResult.fail(this)
314320

321+
override def disallowRootCapability(handler: () => Unit)(using Context): this.type =
322+
addRootHandler = handler
323+
super.disallowRootCapability(handler)
324+
315325
private var computingApprox = false
316326

317327
final def upperApprox(origin: CaptureSet)(using Context): CaptureSet =

compiler/src/dotty/tools/dotc/transform/Recheck.scala

+1
Original file line numberDiff line numberDiff line change
@@ -329,6 +329,7 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
329329
case tree: Alternative => recheckAlternative(tree, pt)
330330
case tree: PackageDef => recheckPackageDef(tree)
331331
case tree: Thicket => defn.NothingType
332+
case tree: Import => defn.NothingType
332333

333334
tree match
334335
case tree: NameTree => recheckNamed(tree, pt)

compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala

+20-57
Original file line numberDiff line numberDiff line change
@@ -76,16 +76,6 @@ object CheckCaptures:
7676
if remaining.accountsFor(firstRef) then
7777
report.warning(em"redundant capture: $remaining already accounts for $firstRef", ann.srcPos)
7878

79-
/** Does this function allow type arguments carrying the universal capability?
80-
* Currently this is true only for `erasedValue` since this function is magic in
81-
* that is allows to conjure global capabilies from nothing (aside: can we find a
82-
* more controlled way to achieve this?).
83-
* But it could be generalized to other functions that so that they can take capability
84-
* classes as arguments.
85-
*/
86-
private def allowUniversalArguments(fn: Tree)(using Context): Boolean =
87-
fn.symbol == defn.Compiletime_erasedValue
88-
8979
class CheckCaptures extends Recheck:
9080
thisPhase =>
9181

@@ -309,6 +299,26 @@ class CheckCaptures extends Recheck:
309299
includeBoxedCaptures(res, tree.srcPos)
310300
res
311301

302+
override def recheckFinish(tpe: Type, tree: Tree, pt: Type)(using Context): Type =
303+
val typeToCheck = tree match
304+
case _: Ident | _: Select | _: Apply | _: TypeApply if tree.symbol.unboxesResult =>
305+
tpe
306+
case _: Try =>
307+
tpe
308+
case ValDef(_, tpt, _) if tree.symbol.is(Mutable) =>
309+
tree.symbol.info
310+
case _ =>
311+
NoType
312+
if typeToCheck.exists then
313+
typeToCheck.widenDealias match
314+
case wtp @ CapturingType(parent, refs, _) =>
315+
refs.disallowRootCapability { () =>
316+
val kind = if tree.isInstanceOf[ValDef] then "mutable variable" else "expression"
317+
report.error(em"the $kind's type $wtp is not allowed to capture the root capability `*`", tree.srcPos)
318+
}
319+
case _ =>
320+
super.recheckFinish(tpe, tree, pt)
321+
312322
override def checkUnit(unit: CompilationUnit)(using Context): Unit =
313323
Setup(preRecheckPhase, thisPhase, recheckDef)
314324
.traverse(ctx.compilationUnit.tpdTree)
@@ -319,45 +329,6 @@ class CheckCaptures extends Recheck:
319329
show(unit.tpdTree) // this dows not print tree, but makes its variables visible for dependency printing
320330
}
321331

322-
def checkNotGlobal(tree: Tree, tp: Type, isVar: Boolean, allArgs: Tree*)(using Context): Unit =
323-
for ref <- tp.captureSet.elems do
324-
val isGlobal = ref match
325-
case ref: TermRef => ref.isRootCapability
326-
case _ => false
327-
if isGlobal then
328-
val what = if ref.isRootCapability then "universal" else "global"
329-
val notAllowed = i" is not allowed to capture the $what capability $ref"
330-
def msg =
331-
if allArgs.isEmpty then
332-
i"${if isVar then "type of mutable variable" else "result type"} ${tree.knownType}$notAllowed"
333-
else tree match
334-
case tree: InferredTypeTree =>
335-
i"""inferred type argument ${tree.knownType}$notAllowed
336-
|
337-
|The inferred arguments are: [${allArgs.map(_.knownType)}%, %]"""
338-
case _ => s"type argument$notAllowed"
339-
report.error(msg, tree.srcPos)
340-
341-
def checkNotGlobal(tree: Tree, allArgs: Tree*)(using Context): Unit =
342-
tree match
343-
case LambdaTypeTree(_, restpt) =>
344-
checkNotGlobal(restpt, allArgs*)
345-
case _ =>
346-
checkNotGlobal(tree, tree.knownType, isVar = false, allArgs*)
347-
348-
def checkNotGlobalDeep(tree: Tree)(using Context): Unit =
349-
val checker = new TypeTraverser:
350-
def traverse(tp: Type): Unit = tp match
351-
case tp: TypeRef =>
352-
tp.info match
353-
case TypeBounds(_, hi) => traverse(hi)
354-
case _ =>
355-
case tp: TermRef =>
356-
case _ =>
357-
checkNotGlobal(tree, tp, isVar = true)
358-
traverseChildren(tp)
359-
checker.traverse(tree.knownType)
360-
361332
object PostCheck extends TreeTraverser:
362333
def traverse(tree: Tree)(using Context) = trace{i"post check $tree"} {
363334
tree match
@@ -370,10 +341,6 @@ class CheckCaptures extends Recheck:
370341
checkWellformedPost(annot.tree)
371342
case _ =>
372343
}
373-
case tree1 @ TypeApply(fn, args) if !allowUniversalArguments(fn) =>
374-
for arg <- args do
375-
//println(i"checking $arg in $tree: ${tree.knownType.captureSet}")
376-
checkNotGlobal(arg, args*)
377344
case t: ValOrDefDef if t.tpt.isInstanceOf[InferredTypeTree] =>
378345
val sym = t.symbol
379346
val isLocal =
@@ -396,10 +363,6 @@ class CheckCaptures extends Recheck:
396363
|The type needs to be declared explicitly.""", t.srcPos)
397364
case _ =>
398365
inferred.foreachPart(checkPure, StopAt.Static)
399-
case t: ValDef if t.symbol.is(Mutable) =>
400-
checkNotGlobalDeep(t.tpt)
401-
case t: Try =>
402-
checkNotGlobal(t)
403366
case _ =>
404367
traverseChildren(tree)
405368
}

tests/neg-custom-args/captures/capt-test.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ def handle[E <: Exception, R <: Top](op: (CanThrow[E]) => R)(handler: E => R): R
1919
catch case ex: E => handler(ex)
2020

2121
def test: Unit =
22-
val b = handle[Exception, () => Nothing] { // error
22+
val b = handle[Exception, () => Nothing] {
2323
(x: CanThrow[Exception]) => () => raise(new Exception)(using x)
24-
} {
24+
} { // error
2525
(ex: Exception) => ???
2626
}
+19-7
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,20 @@
1-
-- Error: tests/neg-custom-args/captures/real-try.scala:10:2 -----------------------------------------------------------
2-
10 | try // error
1+
-- Error: tests/neg-custom-args/captures/real-try.scala:12:2 -----------------------------------------------------------
2+
12 | try // error
33
| ^
4-
| result type {*} () -> Unit is not allowed to capture the universal capability *.type
5-
11 | () => foo(1)
6-
12 | catch
7-
13 | case _: Ex1 => ???
8-
14 | case _: Ex2 => ???
4+
| the expression's type {*} () -> Unit is not allowed to capture the root capability `*`
5+
13 | () => foo(1)
6+
14 | catch
7+
15 | case _: Ex1 => ???
8+
16 | case _: Ex2 => ???
9+
-- Error: tests/neg-custom-args/captures/real-try.scala:18:2 -----------------------------------------------------------
10+
18 | try // error
11+
| ^
12+
| the expression's type {*} () -> ? Cell[Unit] is not allowed to capture the root capability `*`
13+
19 | () => Cell(foo(1))
14+
20 | catch
15+
21 | case _: Ex1 => ???
16+
22 | case _: Ex2 => ???
17+
-- Error: tests/neg-custom-args/captures/real-try.scala:30:4 -----------------------------------------------------------
18+
30 | b.x // error
19+
| ^^^
20+
| the expression's type box {*} () -> Unit is not allowed to capture the root capability `*`

tests/neg-custom-args/captures/real-try.scala

+16
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,25 @@ class Ex2 extends Exception("Ex2")
66
def foo(i: Int): (CanThrow[Ex1], CanThrow[Ex2]) ?-> Unit =
77
if i > 0 then throw new Ex1 else throw new Ex2
88

9+
class Cell[+T](val x: T)
10+
911
def test() =
1012
try // error
1113
() => foo(1)
1214
catch
1315
case _: Ex1 => ???
1416
case _: Ex2 => ???
17+
18+
try // error
19+
() => Cell(foo(1))
20+
catch
21+
case _: Ex1 => ???
22+
case _: Ex2 => ???
23+
24+
val b = try // ok here, but error on use
25+
Cell(() => foo(1))//: Cell[box {ev} () => Unit] <: Cell[box {*} () => Unit]
26+
catch
27+
case _: Ex1 => ???
28+
case _: Ex2 => ???
29+
30+
b.x // error
+30-16
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,11 @@
1+
-- Error: tests/neg-custom-args/captures/try.scala:24:3 ----------------------------------------------------------------
2+
22 | val a = handle[Exception, CanThrow[Exception]] {
3+
23 | (x: CanThrow[Exception]) => x
4+
24 | }{ // error
5+
| ^
6+
| the expression's type {*} CT[Exception] is not allowed to capture the root capability `*`
7+
25 | (ex: Exception) => ???
8+
26 | }
19
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:28:43 ------------------------------------------
210
28 | val b = handle[Exception, () -> Nothing] { // error
311
| ^
@@ -7,19 +15,25 @@
715
30 | } {
816

917
longer explanation available when compiling with `-explain`
10-
-- Error: tests/neg-custom-args/captures/try.scala:22:28 ---------------------------------------------------------------
11-
22 | val a = handle[Exception, CanThrow[Exception]] { // error
12-
| ^^^^^^^^^^^^^^^^^^^
13-
| type argument is not allowed to capture the universal capability (* : Any)
14-
-- Error: tests/neg-custom-args/captures/try.scala:34:11 ---------------------------------------------------------------
15-
34 | val xx = handle { // error
16-
| ^^^^^^
17-
| inferred type argument {*} () -> Int is not allowed to capture the universal capability (* : Any)
18-
|
19-
| The inferred arguments are: [? Exception, {*} () -> Int]
20-
-- Error: tests/neg-custom-args/captures/try.scala:46:13 ---------------------------------------------------------------
21-
46 |val global = handle { // error
22-
| ^^^^^^
23-
| inferred type argument {*} () -> Int is not allowed to capture the universal capability (* : Any)
24-
|
25-
| The inferred arguments are: [? Exception, {*} () -> Int]
18+
-- Error: tests/neg-custom-args/captures/try.scala:39:4 ----------------------------------------------------------------
19+
34 | val xx = handle {
20+
35 | (x: CanThrow[Exception]) =>
21+
36 | () =>
22+
37 | raise(new Exception)(using x)
23+
38 | 22
24+
39 | } { // error
25+
| ^
26+
| the expression's type {*} () -> Int is not allowed to capture the root capability `*`
27+
40 | (ex: Exception) => () => 22
28+
41 | }
29+
-- Error: tests/neg-custom-args/captures/try.scala:51:2 ----------------------------------------------------------------
30+
46 |val global = handle {
31+
47 | (x: CanThrow[Exception]) =>
32+
48 | () =>
33+
49 | raise(new Exception)(using x)
34+
50 | 22
35+
51 |} { // error
36+
| ^
37+
| the expression's type {*} () -> Int is not allowed to capture the root capability `*`
38+
52 | (ex: Exception) => () => 22
39+
53 |}

tests/neg-custom-args/captures/try.scala

+6-6
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ def handle[E <: Exception, R <: Top](op: CanThrow[E] => R)(handler: E => R): R =
1919
catch case ex: E => handler(ex)
2020

2121
def test =
22-
val a = handle[Exception, CanThrow[Exception]] { // error
22+
val a = handle[Exception, CanThrow[Exception]] {
2323
(x: CanThrow[Exception]) => x
24-
}{
24+
}{ // error
2525
(ex: Exception) => ???
2626
}
2727

@@ -31,23 +31,23 @@ def test =
3131
(ex: Exception) => ???
3232
}
3333

34-
val xx = handle { // error
34+
val xx = handle {
3535
(x: CanThrow[Exception]) =>
3636
() =>
3737
raise(new Exception)(using x)
3838
22
39-
} {
39+
} { // error
4040
(ex: Exception) => () => 22
4141
}
4242
val yy = xx :: Nil
4343
yy // OK
4444

4545

46-
val global = handle { // error
46+
val global = handle {
4747
(x: CanThrow[Exception]) =>
4848
() =>
4949
raise(new Exception)(using x)
5050
22
51-
} {
51+
} { // error
5252
(ex: Exception) => () => 22
5353
}

tests/neg-custom-args/captures/try3.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,12 @@ def raise[E <: Exception](ex: E)(using CanThrow[E]): Nothing =
1414

1515
@main def Test: Int =
1616
def f(a: Boolean) =
17-
handle { // error
17+
handle {
1818
if !a then raise(IOException())
1919
(b: Boolean) =>
2020
if !b then raise(IOException())
2121
0
22-
} {
22+
} { // error
2323
ex => (b: Boolean) => -1
2424
}
2525
val g = f(true)

0 commit comments

Comments
 (0)