Skip to content

Commit 05bce38

Browse files
committed
Implement sealed type variables
Abolish restriction that box/unbox cannot be done with `cap`. Instead, do a deep check for `cap` - in type arguments for `sealed` type variables - in the types of mutable vars - in the type of `try` under the `saferExceptions` language import The caps.unsafe.{unsafeBox, unsafeUnbox, unsafeBoxFunArg} methods are not longer needed and are deprecated. Instead there is an annotation annotation.unchecked.uncheckedCaptures that can be added to a mutable variable to turn off checking its type. These changes in behavior are introduced in 3.3. Older source versions still support the old behavior (which corresponds to the paper). So to run examples in the paper as described there, they need a `-source 3.2` or a language import. import language.`3.2`.
1 parent 8eb125d commit 05bce38

Some content is hidden

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

48 files changed

+371
-221
lines changed

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ import core.*
66
import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
77
import ast.{tpd, untpd}
88
import Decorators.*, NameOps.*
9+
import config.SourceVersion
910
import config.Printers.capt
1011
import util.Property.Key
1112
import tpd.*
@@ -19,6 +20,9 @@ private[cc] def retainedElems(tree: Tree)(using Context): List[Tree] = tree matc
1920
case Apply(_, Typed(SeqLiteral(elems, _), _) :: Nil) => elems
2021
case _ => Nil
2122

23+
def allowUniversalInBoxed(using Context) =
24+
Feature.sourceVersion.isAtLeast(SourceVersion.`3.3`)
25+
2226
/** An exception thrown if a @retains argument is not syntactically a CaptureRef */
2327
class IllegalCaptureRef(tpe: Type) extends Exception
2428

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

Lines changed: 33 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,20 @@ object CheckCaptures:
128128
if remaining.accountsFor(firstRef) then
129129
report.warning(em"redundant capture: $remaining already accounts for $firstRef", ann.srcPos)
130130

131+
def disallowRootCapabilitiesIn(tp: Type, what: String, have: String, addendum: String, pos: SrcPos)(using Context) =
132+
val check = new TypeTraverser:
133+
def traverse(t: Type) =
134+
if variance >= 0 then
135+
t.captureSet.disallowRootCapability: () =>
136+
def part = if t eq tp then "" else i"the part $t of "
137+
report.error(
138+
em"""$what cannot $have $tp since
139+
|${part}that type captures the root capability `cap`.
140+
|$addendum""",
141+
pos)
142+
traverseChildren(t)
143+
check.traverse(tp)
144+
131145
class CheckCaptures extends Recheck, SymTransformer:
132146
thisPhase =>
133147

@@ -525,6 +539,15 @@ class CheckCaptures extends Recheck, SymTransformer:
525539
case _ =>
526540
super.recheckTyped(tree)
527541

542+
override def recheckTry(tree: Try, pt: Type)(using Context): Type =
543+
val tp = super.recheckTry(tree, pt)
544+
if allowUniversalInBoxed && Feature.enabled(Feature.saferExceptions) then
545+
disallowRootCapabilitiesIn(tp,
546+
"Result of `try`", "have type",
547+
"This is often caused by a locally generated exception capability leaking as part of its result.",
548+
tree.srcPos)
549+
tp
550+
528551
/* Currently not needed, since capture checking takes place after ElimByName.
529552
* Keep around in case we need to get back to it
530553
def recheckByNameArg(tree: Tree, pt: Type)(using Context): Type =
@@ -588,7 +611,7 @@ class CheckCaptures extends Recheck, SymTransformer:
588611
}
589612
checkNotUniversal(parent)
590613
case _ =>
591-
checkNotUniversal(typeToCheck)
614+
if !allowUniversalInBoxed then checkNotUniversal(typeToCheck)
592615
super.recheckFinish(tpe, tree, pt)
593616

594617
/** Massage `actual` and `expected` types using the methods below before checking conformance */
@@ -771,21 +794,22 @@ class CheckCaptures extends Recheck, SymTransformer:
771794
val criticalSet = // the set which is not allowed to have `cap`
772795
if covariant then cs1 // can't box with `cap`
773796
else expected.captureSet // can't unbox with `cap`
774-
if criticalSet.isUniversal && expected.isValueType then
797+
if criticalSet.isUniversal && expected.isValueType && !allowUniversalInBoxed then
775798
// We can't box/unbox the universal capability. Leave `actual` as it is
776799
// so we get an error in checkConforms. This tends to give better error
777800
// messages than disallowing the root capability in `criticalSet`.
778801
if ctx.settings.YccDebug.value then
779802
println(i"cannot box/unbox $actual vs $expected")
780803
actual
781804
else
782-
// Disallow future addition of `cap` to `criticalSet`.
783-
criticalSet.disallowRootCapability { () =>
784-
report.error(
785-
em"""$actual cannot be box-converted to $expected
786-
|since one of their capture sets contains the root capability `cap`""",
787-
pos)
788-
}
805+
if !allowUniversalInBoxed then
806+
// Disallow future addition of `cap` to `criticalSet`.
807+
criticalSet.disallowRootCapability { () =>
808+
report.error(
809+
em"""$actual cannot be box-converted to $expected
810+
|since one of their capture sets contains the root capability `cap`""",
811+
pos)
812+
}
789813
if !insertBox then // unboxing
790814
markFree(criticalSet, pos)
791815
adaptedType(!boxed)

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

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -411,11 +411,28 @@ extends tpd.TreeTraverser:
411411
boxed = tree.symbol.is(Mutable), // types of mutable variables are boxed
412412
exact = tree.symbol.allOverriddenSymbols.hasNext // types of symbols that override a parent don't get a capture set
413413
)
414+
if allowUniversalInBoxed && tree.symbol.is(Mutable)
415+
&& !tree.symbol.hasAnnotation(defn.UncheckedCapturesAnnot)
416+
then
417+
CheckCaptures.disallowRootCapabilitiesIn(tpt.knownType,
418+
i"Mutable variable ${tree.symbol.name}", "have type",
419+
"This restriction serves to prevent local capabilities from escaping the scope where they are defined.",
420+
tree.srcPos)
414421
traverse(tree.rhs)
415422
case tree @ TypeApply(fn, args) =>
416423
traverse(fn)
417424
for case arg: TypeTree <- args do
418425
transformTT(arg, boxed = true, exact = false) // type arguments in type applications are boxed
426+
427+
if allowUniversalInBoxed then
428+
val polyType = fn.tpe.widen.asInstanceOf[TypeLambda]
429+
for case (arg: TypeTree, pinfo, pname) <- args.lazyZip(polyType.paramInfos).lazyZip((polyType.paramNames)) do
430+
if pinfo.bounds.hi.hasAnnotation(defn.Caps_SealedAnnot) then
431+
def where = if fn.symbol.exists then i" in the body of ${fn.symbol}" else ""
432+
CheckCaptures.disallowRootCapabilitiesIn(arg.knownType,
433+
i"Sealed type variable $pname", " be instantiated to",
434+
i"This is often caused by a local capability$where\nleaking as part of its result.",
435+
tree.srcPos)
419436
case _ =>
420437
traverseChildren(tree)
421438
tree match
@@ -494,11 +511,10 @@ extends tpd.TreeTraverser:
494511

495512
def apply(tree: Tree)(using Context): Unit =
496513
traverse(tree)(using ctx.withProperty(Setup.IsDuringSetupKey, Some(())))
497-
end Setup
498514

499515
object Setup:
500516
val IsDuringSetupKey = new Property.Key[Unit]
501517

502518
def isDuringSetup(using Context): Boolean =
503519
ctx.property(IsDuringSetupKey).isDefined
504-
520+
end Setup

compiler/src/dotty/tools/dotc/config/SourceVersion.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ enum SourceVersion:
1818

1919
def isAtLeast(v: SourceVersion) = stable.ordinal >= v.ordinal
2020

21+
def isAtMost(v: SourceVersion) = stable.ordinal <= v.ordinal
22+
2123
object SourceVersion extends Property.Key[SourceVersion]:
2224
def defaultSourceVersion = `3.3`
2325

compiler/src/dotty/tools/dotc/core/Definitions.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -973,6 +973,7 @@ class Definitions {
973973
@tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
974974
@tu lazy val Caps_unsafeUnbox: Symbol = CapsUnsafeModule.requiredMethod("unsafeUnbox")
975975
@tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg")
976+
@tu lazy val Caps_SealedAnnot: ClassSymbol = requiredClass("scala.caps.Sealed")
976977

977978
// Annotation base classes
978979
@tu lazy val AnnotationClass: ClassSymbol = requiredClass("scala.annotation.Annotation")
@@ -1021,6 +1022,7 @@ class Definitions {
10211022
@tu lazy val UncheckedAnnot: ClassSymbol = requiredClass("scala.unchecked")
10221023
@tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable")
10231024
@tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance")
1025+
@tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
10241026
@tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
10251027
@tu lazy val WithPureFunsAnnot: ClassSymbol = requiredClass("scala.annotation.internal.WithPureFuns")
10261028
@tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")

compiler/src/dotty/tools/dotc/core/Types.scala

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3960,10 +3960,15 @@ object Types {
39603960

39613961
protected def toPInfo(tp: Type)(using Context): PInfo
39623962

3963+
/** If `tparam` is a sealed type parameter symbol of a polymorphic method, add
3964+
* a @caps.Sealed annotation to the upperbound in `tp`.
3965+
*/
3966+
protected def addSealed(tparam: ParamInfo, tp: Type)(using Context): Type = tp
3967+
39633968
def fromParams[PI <: ParamInfo.Of[N]](params: List[PI], resultType: Type)(using Context): Type =
39643969
if (params.isEmpty) resultType
39653970
else apply(params.map(_.paramName))(
3966-
tl => params.map(param => toPInfo(tl.integrate(params, param.paramInfo))),
3971+
tl => params.map(param => toPInfo(addSealed(param, tl.integrate(params, param.paramInfo)))),
39673972
tl => tl.integrate(params, resultType))
39683973
}
39693974

@@ -4285,6 +4290,16 @@ object Types {
42854290
resultTypeExp: PolyType => Type)(using Context): PolyType =
42864291
unique(new PolyType(paramNames)(paramInfosExp, resultTypeExp))
42874292

4293+
override protected def addSealed(tparam: ParamInfo, tp: Type)(using Context): Type =
4294+
tparam match
4295+
case tparam: Symbol if tparam.is(Sealed) =>
4296+
tp match
4297+
case tp @ TypeBounds(lo, hi) =>
4298+
tp.derivedTypeBounds(lo,
4299+
AnnotatedType(hi, Annotation(defn.Caps_SealedAnnot, tparam.span)))
4300+
case _ => tp
4301+
case _ => tp
4302+
42884303
def unapply(tl: PolyType): Some[(List[LambdaParam], Type)] =
42894304
Some((tl.typeParams, tl.resType))
42904305
}

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -3152,7 +3152,9 @@ object Parsers {
31523152
* id [HkTypeParamClause] TypeParamBounds
31533153
*
31543154
* DefTypeParamClause::= ‘[’ DefTypeParam {‘,’ DefTypeParam} ‘]’
3155-
* DefTypeParam ::= {Annotation} id [HkTypeParamClause] TypeParamBounds
3155+
* DefTypeParam ::= {Annotation}
3156+
* [`sealed`] -- under captureChecking
3157+
* id [HkTypeParamClause] TypeParamBounds
31563158
*
31573159
* TypTypeParamClause::= ‘[’ TypTypeParam {‘,’ TypTypeParam} ‘]’
31583160
* TypTypeParam ::= {Annotation} id [HkTypePamClause] TypeBounds
@@ -3162,24 +3164,25 @@ object Parsers {
31623164
*/
31633165
def typeParamClause(ownerKind: ParamOwner): List[TypeDef] = inBrackets {
31643166

3165-
def variance(vflag: FlagSet): FlagSet =
3166-
if ownerKind == ParamOwner.Def || ownerKind == ParamOwner.TypeParam then
3167-
syntaxError(em"no `+/-` variance annotation allowed here")
3168-
in.nextToken()
3169-
EmptyFlags
3170-
else
3171-
in.nextToken()
3172-
vflag
3167+
def checkVarianceOK(): Boolean =
3168+
val ok = ownerKind != ParamOwner.Def && ownerKind != ParamOwner.TypeParam
3169+
if !ok then syntaxError(em"no `+/-` variance annotation allowed here")
3170+
in.nextToken()
3171+
ok
31733172

31743173
def typeParam(): TypeDef = {
31753174
val isAbstractOwner = ownerKind == ParamOwner.Type || ownerKind == ParamOwner.TypeParam
31763175
val start = in.offset
3177-
val mods =
3178-
annotsAsMods()
3179-
| (if (ownerKind == ParamOwner.Class) Param | PrivateLocal else Param)
3180-
| (if isIdent(nme.raw.PLUS) then variance(Covariant)
3181-
else if isIdent(nme.raw.MINUS) then variance(Contravariant)
3182-
else EmptyFlags)
3176+
var mods = annotsAsMods() | Param
3177+
if ownerKind == ParamOwner.Class then mods |= PrivateLocal
3178+
if Feature.ccEnabled && in.token == SEALED then
3179+
if ownerKind == ParamOwner.Def then mods |= Sealed
3180+
else syntaxError(em"`sealed` modifier only allowed for method type parameters")
3181+
in.nextToken()
3182+
if isIdent(nme.raw.PLUS) && checkVarianceOK() then
3183+
mods |= Covariant
3184+
else if isIdent(nme.raw.MINUS) && checkVarianceOK() then
3185+
mods |= Contravariant
31833186
atSpan(start, nameStart) {
31843187
val name =
31853188
if (isAbstractOwner && in.token == USCORE) {

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

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ package transform
44

55
import core.*
66
import Symbols.*, Contexts.*, Types.*, ContextOps.*, Decorators.*, SymDenotations.*
7-
import Flags.*, SymUtils.*, NameKinds.*, Denotations.Denotation
7+
import Flags.*, SymUtils.*, NameKinds.*, Denotations.{Denotation, SingleDenotation}
88
import ast.*
99
import Names.Name
1010
import Phases.Phase
@@ -22,7 +22,7 @@ import StdNames.nme
2222
import reporting.trace
2323
import annotation.constructorOnly
2424
import cc.CaptureSet.IdempotentCaptRefMap
25-
import dotty.tools.dotc.core.Denotations.SingleDenotation
25+
import annotation.tailrec
2626

2727
object Recheck:
2828
import tpd.*
@@ -406,7 +406,14 @@ abstract class Recheck extends Phase, SymTransformer:
406406
NoType
407407

408408
def recheckStats(stats: List[Tree])(using Context): Unit =
409-
stats.foreach(recheck(_))
409+
@tailrec def traverse(stats: List[Tree])(using Context): Unit = stats match
410+
case (imp: Import) :: rest =>
411+
traverse(rest)(using ctx.importContext(imp, imp.symbol))
412+
case stat :: rest =>
413+
recheck(stat)
414+
traverse(rest)
415+
case _ =>
416+
traverse(stats)
410417

411418
def recheckDef(tree: ValOrDefDef, sym: Symbol)(using Context): Unit =
412419
inContext(ctx.localContext(tree, sym)) {

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

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -506,7 +506,12 @@ object Checking {
506506
// note: this is not covered by the next test since terms can be abstract (which is a dual-mode flag)
507507
// but they can never be one of ClassOnlyFlags
508508
if !sym.isClass && sym.isOneOf(ClassOnlyFlags) then
509-
fail(em"only classes can be ${(sym.flags & ClassOnlyFlags).flagsString}")
509+
val illegal = sym.flags & ClassOnlyFlags
510+
if sym.is(TypeParam) && illegal == Sealed && Feature.ccEnabled && cc.allowUniversalInBoxed then
511+
if !sym.owner.is(Method) then
512+
fail(em"only method type parameters can be sealed")
513+
else
514+
fail(em"only classes can be ${illegal.flagsString}")
510515
if (sym.is(AbsOverride) && !sym.owner.is(Trait))
511516
fail(AbstractOverrideOnlyInTraits(sym))
512517
if sym.is(Trait) then

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -608,7 +608,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
608608
ownType match
609609
case ownType: TermRef if ownType.symbol.is(ConstructorProxy) =>
610610
findRef(name, pt, EmptyFlags, ConstructorProxy, tree.srcPos) match
611-
case shadowed: TermRef =>
611+
case shadowed: TermRef if !shadowed.symbol.maybeOwner.isEmptyPackage =>
612612
pt match
613613
case pt: FunOrPolyProto =>
614614
def err(shadowedIsApply: Boolean) =
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package scala.annotation
2+
package unchecked
3+
4+
/** An annotation for mutable variables that are allowed to capture
5+
* the root capability `cap`. Allowing this is not capture safe since
6+
* it can cause leakage of capabilities from local scopes by assigning
7+
* values retaining such capabilties to the annotated variable in
8+
* an outer scope.
9+
*/
10+
class uncheckedCaptures extends StaticAnnotation
11+
12+

library/src/scala/caps.scala

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,15 @@ import annotation.experimental
2727
* avoids the error that would be raised when unboxing `*`.
2828
*/
2929
extension [T, U](f: T => U) def unsafeBoxFunArg: T => U = f
30+
3031
end unsafe
3132

33+
/** An annotation that expresses the sealed modifier on a type parameter
34+
* Should not be directly referred to in source
35+
*/
36+
@deprecated("The Sealed annotation should not be directly used in source code.\nUse the `sealed` modifier on type parameters instead.")
37+
class Sealed extends annotation.Annotation
38+
3239
/** Mixing in this trait forces a trait or class to be pure, i.e.
3340
* have no capabilities retained in its self type.
3441
*/

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
7+
x(cap => cap.use()) // was error, now OK
88
}
99

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

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,14 @@ def raise[E <: Exception](e: E): Nothing throws E = throw e
1414
def foo(x: Boolean): Int throws Fail =
1515
if x then 1 else raise(Fail())
1616

17-
def handle[E <: Exception, R <: Top](op: (CanThrow[E]) => R)(handler: E => R): R =
17+
def handle[E <: Exception, sealed R <: Top](op: (CanThrow[E]) => R)(handler: E => R): R =
1818
val x: CanThrow[E] = ???
1919
try op(x)
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: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,7 @@
4040
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:24 ----------------------------------------
4141
32 | val z2 = h[() -> Cap](() => x) // error
4242
| ^^^^^^^
43-
| Found: () ->{x} Cap
43+
| Found: () ->{x} box C^
4444
| Required: () -> box C^
4545
|
4646
| longer explanation available when compiling with `-explain`
47-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:33:5 -----------------------------------------
48-
33 | (() => C()) // error
49-
| ^^^^^^^^^
50-
| Found: () ->? Cap
51-
| Required: () -> box C^
52-
|
53-
| longer explanation available when compiling with `-explain`

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ def foo() =
3030
val x: C @retains(caps.cap) = ???
3131
def h[X](a: X)(b: X) = a
3232
val z2 = h[() -> Cap](() => x) // error
33-
(() => C()) // error
33+
(() => C())
3434
val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // ok
3535
val z4 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // what was inferred for z3
3636

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@ class CC
22
type Cap = CC^
33

44
def test(cap1: Cap, cap2: Cap) =
5-
var b: List[String => String] = Nil // was error, now OK
6-
val bc = b.head // error
5+
var b: List[String => String] = Nil // error
6+
val bc = b.head // was error, now OK

0 commit comments

Comments
 (0)