Skip to content

Commit 8f8a15f

Browse files
committed
Go back to sealed checking
Check that type parameters of methods and parent traits don't get instantiated with types containing a `cap` anywhere in covariant or invariant position.
1 parent 4226a33 commit 8f8a15f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

49 files changed

+268
-228
lines changed

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,12 +45,11 @@ object ccConfig:
4545
/** If true, use "sealed" as encapsulation mechanism, meaning that we
4646
* check that type variable instantiations don't have `cap` in any of
4747
* their capture sets. This is an alternative of the original restriction
48-
* that `cap` can't be boxed or unboxed. It is used in 3.3 and 3.4 but
49-
* dropped again in 3.5.
48+
* that `cap` can't be boxed or unboxed. It is dropped in 3.5 but used
49+
* again in 3.6.
5050
*/
5151
def useSealed(using Context) =
52-
Feature.sourceVersion.stable == SourceVersion.`3.3`
53-
|| Feature.sourceVersion.stable == SourceVersion.`3.4`
52+
Feature.sourceVersion.stable != SourceVersion.`3.5`
5453
end ccConfig
5554

5655

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

Lines changed: 36 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -174,8 +174,7 @@ object CheckCaptures:
174174
def part = if t eq tp then "" else i"the part $t of "
175175
report.error(
176176
em"""$what cannot $have $tp since
177-
|${part}that type captures the root capability `cap`.
178-
|$addendum""",
177+
|${part}that type captures the root capability `cap`.$addendum""",
179178
pos)
180179
traverse(parent)
181180
case t =>
@@ -686,23 +685,34 @@ class CheckCaptures extends Recheck, SymTransformer:
686685
else ownType
687686
end instantiate
688687

688+
def disallowCapInTypeArgs(fn: Tree, sym: Symbol, args: List[Tree])(using Context): Unit =
689+
def isExempt = sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
690+
if ccConfig.useSealed && !isExempt then
691+
val paramNames = atPhase(thisPhase.prev):
692+
fn.tpe.widenDealias match
693+
case tl: TypeLambda => tl.paramNames
694+
case ref: AppliedType if ref.typeSymbol.isClass => ref.typeSymbol.typeParams.map(_.name)
695+
case t =>
696+
println(i"parent type: $t")
697+
args.map(_ => EmptyTypeName)
698+
for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do
699+
def where = if sym.exists then i" in an argument of $sym" else ""
700+
val (addendum, pos) =
701+
if arg.isInferred
702+
then ("\nThis is often caused by a local capability$where\nleaking as part of its result.", fn.srcPos)
703+
else if arg.span.exists then ("", arg.srcPos)
704+
else ("", fn.srcPos)
705+
disallowRootCapabilitiesIn(arg.knownType, NoSymbol,
706+
i"Type variable $pname of $sym", "be instantiated to", addendum, pos)
707+
end disallowCapInTypeArgs
708+
689709
override def recheckTypeApply(tree: TypeApply, pt: Type)(using Context): Type =
690-
val meth = tree.symbol
691-
if ccConfig.useSealed then
692-
val TypeApply(fn, args) = tree
693-
val polyType = atPhase(thisPhase.prev):
694-
fn.tpe.widen.asInstanceOf[TypeLambda]
695-
def isExempt(sym: Symbol) =
696-
sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
697-
for case (arg: TypeTree, formal, pname) <- args.lazyZip(polyType.paramRefs).lazyZip((polyType.paramNames)) do
698-
if !isExempt(meth) then
699-
def where = if meth.exists then i" in an argument of $meth" else ""
700-
disallowRootCapabilitiesIn(arg.knownType, NoSymbol,
701-
i"Sealed type variable $pname", "be instantiated to",
702-
i"This is often caused by a local capability$where\nleaking as part of its result.",
703-
tree.srcPos)
710+
val meth = tree.fun match
711+
case fun @ Select(qual, nme.apply) => qual.symbol.orElse(fun.symbol)
712+
case fun => fun.symbol
713+
disallowCapInTypeArgs(tree.fun, meth, tree.args)
704714
val res = Existential.toCap(super.recheckTypeApply(tree, pt))
705-
includeCallCaptures(meth, res, tree.srcPos)
715+
includeCallCaptures(tree.symbol, res, tree.srcPos)
706716
checkContains(tree)
707717
res
708718
end recheckTypeApply
@@ -806,7 +816,7 @@ class CheckCaptures extends Recheck, SymTransformer:
806816
case _ => ""
807817
s"an anonymous function$location"
808818
else encl.show
809-
(NoSymbol, i"\nNote that $sym does not count as local since it is captured by $enclStr")
819+
(NoSymbol, i"\n\nNote that $sym does not count as local since it is captured by $enclStr")
810820
case _ =>
811821
(sym, "")
812822
disallowRootCapabilitiesIn(
@@ -927,6 +937,11 @@ class CheckCaptures extends Recheck, SymTransformer:
927937
checkSubset(thisSet,
928938
CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
929939
selfType.srcPos, cs1description = " captured by this self type")
940+
for case tpt: TypeTree <- impl.parents do
941+
tpt.tpe match
942+
case AppliedType(fn, args) =>
943+
disallowCapInTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_)))
944+
case _ =>
930945
inNestedLevelUnless(cls.is(Module)):
931946
super.recheckClassDef(tree, impl, cls)
932947
finally
@@ -950,8 +965,8 @@ class CheckCaptures extends Recheck, SymTransformer:
950965
val tp = super.recheckTry(tree, pt)
951966
if ccConfig.useSealed && Feature.enabled(Feature.saferExceptions) then
952967
disallowRootCapabilitiesIn(tp, ctx.owner,
953-
"result of `try`", "have type",
954-
"This is often caused by a locally generated exception capability leaking as part of its result.",
968+
"The result of `try`", "have type",
969+
"\nThis is often caused by a locally generated exception capability leaking as part of its result.",
955970
tree.srcPos)
956971
tp
957972

@@ -1592,8 +1607,7 @@ class CheckCaptures extends Recheck, SymTransformer:
15921607
&& !arg.typeSymbol.name.is(WildcardParamName)
15931608
then
15941609
CheckCaptures.disallowRootCapabilitiesIn(arg, NoSymbol,
1595-
"Array", "have element type",
1596-
"Since arrays are mutable, they have to be treated like variables,\nso their element type must be sealed.",
1610+
"Array", "have element type", "",
15971611
pos)
15981612
traverseChildren(t)
15991613
case defn.RefinedFunctionOf(rinfo: MethodType) =>

tests/neg-custom-args/captures/box-adapt-cases.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ def test1(): Unit = {
44
type Id[X] = [T] -> (op: X => T) -> T
55

66
val x: Id[Cap^] = ???
7-
x(cap => cap.use()) // error, OK under sealed
7+
x(cap => cap.use())
88
}
99

1010
def test2(io: Cap^): Unit = {

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,8 @@ def handle[E <: Exception, R <: Top](op: (CT[E] @retains(caps.cap)) => R)(handl
2020
catch case ex: E => handler(ex)
2121

2222
def test: Unit =
23-
val b = handle[Exception, () => Nothing] {
23+
val b = handle[Exception, () => Nothing] { // error
2424
(x: CanThrow[Exception]) => () => raise(new Exception)(using x)
25-
} { // error
25+
} {
2626
(ex: Exception) => ???
2727
}

tests/neg-custom-args/captures/capt1.check

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -33,22 +33,18 @@
3333
29 | def m() = if x == null then y else y
3434
|
3535
| longer explanation available when compiling with `-explain`
36-
-- Error: tests/neg-custom-args/captures/capt1.scala:34:12 -------------------------------------------------------------
36+
-- Error: tests/neg-custom-args/captures/capt1.scala:34:16 -------------------------------------------------------------
3737
34 | val z2 = h[() -> Cap](() => x) // error // error
38-
| ^^^^^^^^^^^^
39-
| Sealed type variable X cannot be instantiated to () -> box C^ since
40-
| the part box C^ of that type captures the root capability `cap`.
41-
| This is often caused by a local capability in an argument of method h
42-
| leaking as part of its result.
38+
| ^^^^^^^^^
39+
| Type variable X of method h cannot be instantiated to () -> box C^ since
40+
| the part box C^ of that type captures the root capability `cap`.
4341
-- Error: tests/neg-custom-args/captures/capt1.scala:34:30 -------------------------------------------------------------
4442
34 | val z2 = h[() -> Cap](() => x) // error // error
4543
| ^
4644
| (x : C^) cannot be referenced here; it is not included in the allowed capture set {}
4745
| of an enclosing function literal with expected type () -> box C^
48-
-- Error: tests/neg-custom-args/captures/capt1.scala:36:12 -------------------------------------------------------------
46+
-- Error: tests/neg-custom-args/captures/capt1.scala:36:13 -------------------------------------------------------------
4947
36 | val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // error
50-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
51-
| Sealed type variable X cannot be instantiated to box () ->{x} Cap since
52-
| the part Cap of that type captures the root capability `cap`.
53-
| This is often caused by a local capability in an argument of method h
54-
| leaking as part of its result.
48+
| ^^^^^^^^^^^^^^^^^^^^^^^
49+
| Type variable X of method h cannot be instantiated to box () ->{x} Cap since
50+
| the part Cap of that type captures the root capability `cap`.

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
//> using options -source 3.4
2-
// (to make sure we use the sealed policy)
1+
2+
33
import annotation.retains
44
class C
55
def f(x: C @retains(caps.cap), y: C): () -> C =

tests/neg-custom-args/captures/effect-swaps-explicit.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
//> using options -source 3.4
2-
// (to make sure we use the sealed policy)
1+
2+
33
object boundary:
44

55
final class Label[-T] // extends caps.Capability

tests/neg-custom-args/captures/effect-swaps.check

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,3 +22,8 @@
2222
73 | fr.await.ok
2323
|
2424
| longer explanation available when compiling with `-explain`
25+
-- Error: tests/neg-custom-args/captures/effect-swaps.scala:66:15 ------------------------------------------------------
26+
66 | Result.make: // error: local reference leaks
27+
| ^^^^^^^^^^^
28+
|local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]^):
29+
| box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result

tests/neg-custom-args/captures/effect-swaps.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ def test[T, E](using Async) =
6363
fr.await.ok
6464

6565
def fail4[T, E](fr: Future[Result[T, E]]^) =
66-
Result.make: // should be errorm but inders Result[Any, Any]
66+
Result.make: // error: local reference leaks
6767
Future: fut ?=>
6868
fr.await.ok
6969

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ class File:
55
def write(x: String): Unit = ???
66

77
class Service:
8-
var file: File^ = uninitialized // OK, was error under sealed
9-
def log = file.write("log") // error, was OK under sealed
8+
var file: File^ = uninitialized // error, was OK under unsealed
9+
def log = file.write("log") // OK, was error under unsealed
1010

1111
def withFile[T](op: (l: caps.Capability) ?-> (f: File^{l}) => T): T =
1212
op(using caps.cap)(new File)

0 commit comments

Comments
 (0)