Skip to content

Commit 128a2d7

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 308ab14 commit 128a2d7

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
@@ -171,8 +171,7 @@ object CheckCaptures:
171171
def part = if t eq tp then "" else i"the part $t of "
172172
report.error(
173173
em"""$what cannot $have $tp since
174-
|${part}that type captures the root capability `cap`.
175-
|$addendum""",
174+
|${part}that type captures the root capability `cap`.$addendum""",
176175
pos)
177176
traverse(parent)
178177
case t =>
@@ -681,23 +680,34 @@ class CheckCaptures extends Recheck, SymTransformer:
681680
else ownType
682681
end instantiate
683682

683+
def disallowCapInTypeArgs(fn: Tree, sym: Symbol, args: List[Tree])(using Context): Unit =
684+
def isExempt = sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
685+
if ccConfig.useSealed && !isExempt then
686+
val paramNames = atPhase(thisPhase.prev):
687+
fn.tpe.widenDealias match
688+
case tl: TypeLambda => tl.paramNames
689+
case ref: AppliedType if ref.typeSymbol.isClass => ref.typeSymbol.typeParams.map(_.name)
690+
case t =>
691+
println(i"parent type: $t")
692+
args.map(_ => EmptyTypeName)
693+
for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do
694+
def where = if sym.exists then i" in an argument of $sym" else ""
695+
val (addendum, pos) =
696+
if arg.isInferred
697+
then ("\nThis is often caused by a local capability$where\nleaking as part of its result.", fn.srcPos)
698+
else if arg.span.exists then ("", arg.srcPos)
699+
else ("", fn.srcPos)
700+
disallowRootCapabilitiesIn(arg.knownType, NoSymbol,
701+
i"Type variable $pname of $sym", "be instantiated to", addendum, pos)
702+
end disallowCapInTypeArgs
703+
684704
override def recheckTypeApply(tree: TypeApply, pt: Type)(using Context): Type =
685-
val meth = tree.symbol
686-
if ccConfig.useSealed then
687-
val TypeApply(fn, args) = tree
688-
val polyType = atPhase(thisPhase.prev):
689-
fn.tpe.widen.asInstanceOf[TypeLambda]
690-
def isExempt(sym: Symbol) =
691-
sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
692-
for case (arg: TypeTree, formal, pname) <- args.lazyZip(polyType.paramRefs).lazyZip((polyType.paramNames)) do
693-
if !isExempt(meth) then
694-
def where = if meth.exists then i" in an argument of $meth" else ""
695-
disallowRootCapabilitiesIn(arg.knownType, NoSymbol,
696-
i"Sealed type variable $pname", "be instantiated to",
697-
i"This is often caused by a local capability$where\nleaking as part of its result.",
698-
tree.srcPos)
705+
val meth = tree.fun match
706+
case fun @ Select(qual, nme.apply) => qual.symbol.orElse(fun.symbol)
707+
case fun => fun.symbol
708+
disallowCapInTypeArgs(tree.fun, meth, tree.args)
699709
val res = Existential.toCap(super.recheckTypeApply(tree, pt))
700-
includeCallCaptures(meth, res, tree.srcPos)
710+
includeCallCaptures(tree.symbol, res, tree.srcPos)
701711
checkContains(tree)
702712
res
703713
end recheckTypeApply
@@ -801,7 +811,7 @@ class CheckCaptures extends Recheck, SymTransformer:
801811
case _ => ""
802812
s"an anonymous function$location"
803813
else encl.show
804-
(NoSymbol, i"\nNote that $sym does not count as local since it is captured by $enclStr")
814+
(NoSymbol, i"\n\nNote that $sym does not count as local since it is captured by $enclStr")
805815
case _ =>
806816
(sym, "")
807817
disallowRootCapabilitiesIn(
@@ -922,6 +932,11 @@ class CheckCaptures extends Recheck, SymTransformer:
922932
checkSubset(thisSet,
923933
CaptureSet.empty.withDescription(i"of pure base class $pureBase"),
924934
selfType.srcPos, cs1description = " captured by this self type")
935+
for case tpt: TypeTree <- impl.parents do
936+
tpt.tpe match
937+
case AppliedType(fn, args) =>
938+
disallowCapInTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_)))
939+
case _ =>
925940
inNestedLevelUnless(cls.is(Module)):
926941
super.recheckClassDef(tree, impl, cls)
927942
finally
@@ -945,8 +960,8 @@ class CheckCaptures extends Recheck, SymTransformer:
945960
val tp = super.recheckTry(tree, pt)
946961
if ccConfig.useSealed && Feature.enabled(Feature.saferExceptions) then
947962
disallowRootCapabilitiesIn(tp, ctx.owner,
948-
"result of `try`", "have type",
949-
"This is often caused by a locally generated exception capability leaking as part of its result.",
963+
"The result of `try`", "have type",
964+
"\nThis is often caused by a locally generated exception capability leaking as part of its result.",
950965
tree.srcPos)
951966
tp
952967

@@ -1587,8 +1602,7 @@ class CheckCaptures extends Recheck, SymTransformer:
15871602
&& !arg.typeSymbol.name.is(WildcardParamName)
15881603
then
15891604
CheckCaptures.disallowRootCapabilitiesIn(arg, NoSymbol,
1590-
"Array", "have element type",
1591-
"Since arrays are mutable, they have to be treated like variables,\nso their element type must be sealed.",
1605+
"Array", "have element type", "",
15921606
pos)
15931607
traverseChildren(t)
15941608
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)