Skip to content

Commit

Permalink
Implement sealed type parameters (#17422)
Browse files Browse the repository at this point in the history
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.

Based on #17377
  • Loading branch information
odersky committed May 10, 2023
2 parents e614f23 + a8f583d commit d6c643c
Show file tree
Hide file tree
Showing 57 changed files with 469 additions and 308 deletions.
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
Original file line number Diff line number Diff line change
Expand Up @@ -464,8 +464,8 @@ trait UntypedTreeInfo extends TreeInfo[Untyped] { self: Trees.Instance[Untyped]
}
}

/** Under pureFunctions: A builder and extractor for `=> T`, which is an alias for `{*}-> T`.
* Only trees of the form `=> T` are matched; trees written directly as `{*}-> T`
/** Under pureFunctions: A builder and extractor for `=> T`, which is an alias for `->{cap} T`.
* Only trees of the form `=> T` are matched; trees written directly as `->{cap} T`
* are ignored by the extractor.
*/
object ImpureByNameTypeTree:
Expand Down
4 changes: 4 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import core.*
import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
import ast.{tpd, untpd}
import Decorators.*, NameOps.*
import config.SourceVersion
import config.Printers.capt
import util.Property.Key
import tpd.*
Expand All @@ -19,6 +20,9 @@ private[cc] def retainedElems(tree: Tree)(using Context): List[Tree] = tree matc
case Apply(_, Typed(SeqLiteral(elems, _), _) :: Nil) => elems
case _ => Nil

def allowUniversalInBoxed(using Context) =
Feature.sourceVersion.isAtLeast(SourceVersion.`3.3`)

/** An exception thrown if a @retains argument is not syntactically a CaptureRef */
class IllegalCaptureRef(tpe: Type) extends Exception

Expand Down
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ object CaptureSet:
/** The empty capture set `{}` */
val empty: CaptureSet.Const = Const(emptySet)

/** The universal capture set `{*}` */
/** The universal capture set `{cap}` */
def universal(using Context): CaptureSet =
defn.captureRoot.termRef.singletonCaptureSet

Expand Down Expand Up @@ -429,7 +429,7 @@ object CaptureSet:

/** Roughly: the intersection of all constant known supersets of this set.
* The aim is to find an as-good-as-possible constant set that is a superset
* of this set. The universal set {*} is a sound fallback.
* of this set. The universal set {cap} is a sound fallback.
*/
final def upperApprox(origin: CaptureSet)(using Context): CaptureSet =
if computingApprox then universal
Expand Down
160 changes: 95 additions & 65 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,20 @@ object CheckCaptures:
if remaining.accountsFor(firstRef) then
report.warning(em"redundant capture: $remaining already accounts for $firstRef", ann.srcPos)

def disallowRootCapabilitiesIn(tp: Type, what: String, have: String, addendum: String, pos: SrcPos)(using Context) =
val check = new TypeTraverser:
def traverse(t: Type) =
if variance >= 0 then
t.captureSet.disallowRootCapability: () =>
def part = if t eq tp then "" else i"the part $t of "
report.error(
em"""$what cannot $have $tp since
|${part}that type captures the root capability `cap`.
|$addendum""",
pos)
traverseChildren(t)
check.traverse(tp)

class CheckCaptures extends Recheck, SymTransformer:
thisPhase =>

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

override def recheckTry(tree: Try, pt: Type)(using Context): Type =
val tp = super.recheckTry(tree, pt)
if allowUniversalInBoxed && Feature.enabled(Feature.saferExceptions) then
disallowRootCapabilitiesIn(tp,
"Result of `try`", "have type",
"This is often caused by a locally generated exception capability leaking as part of its result.",
tree.srcPos)
tp

/* Currently not needed, since capture checking takes place after ElimByName.
* Keep around in case we need to get back to it
def recheckByNameArg(tree: Tree, pt: Type)(using Context): Type =
Expand Down Expand Up @@ -588,7 +611,7 @@ class CheckCaptures extends Recheck, SymTransformer:
}
checkNotUniversal(parent)
case _ =>
checkNotUniversal(typeToCheck)
if !allowUniversalInBoxed then checkNotUniversal(typeToCheck)
super.recheckFinish(tpe, tree, pt)

/** Massage `actual` and `expected` types using the methods below before checking conformance */
Expand Down Expand Up @@ -771,21 +794,22 @@ class CheckCaptures extends Recheck, SymTransformer:
val criticalSet = // the set which is not allowed to have `cap`
if covariant then cs1 // can't box with `cap`
else expected.captureSet // can't unbox with `cap`
if criticalSet.isUniversal && expected.isValueType then
if criticalSet.isUniversal && expected.isValueType && !allowUniversalInBoxed then
// We can't box/unbox the universal capability. Leave `actual` as it is
// so we get an error in checkConforms. This tends to give better error
// messages than disallowing the root capability in `criticalSet`.
if ctx.settings.YccDebug.value then
println(i"cannot box/unbox $actual vs $expected")
actual
else
// Disallow future addition of `cap` to `criticalSet`.
criticalSet.disallowRootCapability { () =>
report.error(
em"""$actual cannot be box-converted to $expected
|since one of their capture sets contains the root capability `cap`""",
pos)
}
if !allowUniversalInBoxed then
// Disallow future addition of `cap` to `criticalSet`.
criticalSet.disallowRootCapability { () =>
report.error(
em"""$actual cannot be box-converted to $expected
|since one of their capture sets contains the root capability `cap`""",
pos)
}
if !insertBox then // unboxing
markFree(criticalSet, pos)
adaptedType(!boxed)
Expand Down Expand Up @@ -860,7 +884,7 @@ class CheckCaptures extends Recheck, SymTransformer:

/** Check that self types of subclasses conform to self types of super classes.
* (See comment below how this is achieved). The check assumes that classes
* without an explicit self type have the universal capture set `{*}` on the
* without an explicit self type have the universal capture set `{cap}` on the
* self type. If a class without explicit self type is not `effectivelyFinal`
* it is checked that the inferred self type is universal, in order to assure
* that joint and separate compilation give the same result.
Expand Down Expand Up @@ -917,9 +941,9 @@ class CheckCaptures extends Recheck, SymTransformer:
* that this type parameter can't see.
* For example, when capture checking the following expression:
*
* def usingLogFile[T](op: (f: {*} File) => T): T = ...
* def usingLogFile[T](op: (f: {cap} File) => T): T = ...
*
* usingLogFile[box ?1 () -> Unit] { (f: {*} File) => () => { f.write(0) } }
* usingLogFile[box ?1 () -> Unit] { (f: {cap} File) => () => { f.write(0) } }
*
* We may propagate `f` into ?1, making ?1 ill-formed.
* This also causes soundness issues, since `f` in ?1 should be widened to `cap`,
Expand Down Expand Up @@ -986,61 +1010,67 @@ class CheckCaptures extends Recheck, SymTransformer:
* - Heal ill-formed capture sets of type parameters. See `healTypeParam`.
*/
def postCheck(unit: tpd.Tree)(using Context): Unit =
unit.foreachSubTree {
case _: InferredTypeTree =>
case tree: TypeTree if !tree.span.isZeroExtent =>
tree.knownType.foreachPart { tp =>
checkWellformedPost(tp, tree.srcPos)
tp match
case AnnotatedType(_, annot) if annot.symbol == defn.RetainsAnnot =>
warnIfRedundantCaptureSet(annot.tree)
val checker = new TreeTraverser:
def traverse(tree: Tree)(using Context): Unit =
traverseChildren(tree)
check(tree)
def check(tree: Tree) = tree match
case _: InferredTypeTree =>
case tree: TypeTree if !tree.span.isZeroExtent =>
tree.knownType.foreachPart { tp =>
checkWellformedPost(tp, tree.srcPos)
tp match
case AnnotatedType(_, annot) if annot.symbol == defn.RetainsAnnot =>
warnIfRedundantCaptureSet(annot.tree)
case _ =>
}
case t: ValOrDefDef
if t.tpt.isInstanceOf[InferredTypeTree] && !Synthetics.isExcluded(t.symbol) =>
val sym = t.symbol
val isLocal =
sym.owner.ownersIterator.exists(_.isTerm)
|| sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
sym.is(Private) // private symbols can always have inferred types
|| sym.name.is(DefaultGetterName) // default getters are exempted since otherwise it would be
// too annoying. This is a hole since a defualt getter's result type
// might leak into a type variable.
|| // non-local symbols cannot have inferred types since external capture types are not inferred
isLocal // local symbols still need explicit types if
&& !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
def isNotPureThis(ref: CaptureRef) = ref match {
case ref: ThisType => !ref.cls.isPureClass
case _ => true
}
if !canUseInferred then
val inferred = t.tpt.knownType
def checkPure(tp: Type) = tp match
case CapturingType(_, refs)
if !refs.elems.filter(isNotPureThis).isEmpty =>
val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
report.error(
em"""Non-local $sym cannot have an inferred$resultStr type
|$inferred
|with non-empty capture set $refs.
|The type needs to be declared explicitly.""".withoutDisambiguation(),
t.srcPos)
case _ =>
inferred.foreachPart(checkPure, StopAt.Static)
case t @ TypeApply(fun, args) =>
fun.knownType.widen match
case tl: PolyType =>
val normArgs = args.lazyZip(tl.paramInfos).map { (arg, bounds) =>
arg.withType(arg.knownType.forceBoxStatus(
bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
}
checkBounds(normArgs, tl)
case _ =>
}
case t: ValOrDefDef
if t.tpt.isInstanceOf[InferredTypeTree] && !Synthetics.isExcluded(t.symbol) =>
val sym = t.symbol
val isLocal =
sym.owner.ownersIterator.exists(_.isTerm)
|| sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
sym.is(Private) // private symbols can always have inferred types
|| sym.name.is(DefaultGetterName) // default getters are exempted since otherwise it would be
// too annoying. This is a hole since a defualt getter's result type
// might leak into a type variable.
|| // non-local symbols cannot have inferred types since external capture types are not inferred
isLocal // local symbols still need explicit types if
&& !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
def isNotPureThis(ref: CaptureRef) = ref match {
case ref: ThisType => !ref.cls.isPureClass
case _ => true
}
if !canUseInferred then
val inferred = t.tpt.knownType
def checkPure(tp: Type) = tp match
case CapturingType(_, refs)
if !refs.elems.filter(isNotPureThis).isEmpty =>
val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
report.error(
em"""Non-local $sym cannot have an inferred$resultStr type
|$inferred
|with non-empty capture set $refs.
|The type needs to be declared explicitly.""".withoutDisambiguation(),
t.srcPos)
case _ =>
inferred.foreachPart(checkPure, StopAt.Static)
case t @ TypeApply(fun, args) =>
fun.knownType.widen match
case tl: PolyType =>
val normArgs = args.lazyZip(tl.paramInfos).map { (arg, bounds) =>
arg.withType(arg.knownType.forceBoxStatus(
bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
}
checkBounds(normArgs, tl)
case _ =>

args.foreach(healTypeParam(_))
case _ =>
}
args.foreach(healTypeParam(_))
case _ =>
end check
end checker
checker.traverse(unit)
if !ctx.reporter.errorsReported then
// We dont report errors here if previous errors were reported, because other
// errors often result in bad applied types, but flagging these bad types gives
Expand Down
24 changes: 20 additions & 4 deletions compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ extends tpd.TreeTraverser:
val sym = tp.typeSymbol
if sym.isClass then
sym == defn.AnyClass
// we assume Any is a shorthand of {*} Any, so if Any is an upper
// we assume Any is a shorthand of {cap} Any, so if Any is an upper
// bound, the type is taken to be impure.
else superTypeIsImpure(tp.superType)
case tp: (RefinedOrRecType | MatchType) =>
Expand Down Expand Up @@ -155,7 +155,7 @@ extends tpd.TreeTraverser:
case CapturingType(parent, refs) =>
needsVariable(parent)
&& refs.isConst // if refs is a variable, no need to add another
&& !refs.isUniversal // if refs is {*}, an added variable would not change anything
&& !refs.isUniversal // if refs is {cap}, an added variable would not change anything
case _ =>
false
}.showing(i"can have inferred capture $tp = $result", capt)
Expand Down Expand Up @@ -411,11 +411,28 @@ extends tpd.TreeTraverser:
boxed = tree.symbol.is(Mutable), // types of mutable variables are boxed
exact = tree.symbol.allOverriddenSymbols.hasNext // types of symbols that override a parent don't get a capture set
)
if allowUniversalInBoxed && tree.symbol.is(Mutable)
&& !tree.symbol.hasAnnotation(defn.UncheckedCapturesAnnot)
then
CheckCaptures.disallowRootCapabilitiesIn(tpt.knownType,
i"Mutable variable ${tree.symbol.name}", "have type",
"This restriction serves to prevent local capabilities from escaping the scope where they are defined.",
tree.srcPos)
traverse(tree.rhs)
case tree @ TypeApply(fn, args) =>
traverse(fn)
for case arg: TypeTree <- args do
transformTT(arg, boxed = true, exact = false) // type arguments in type applications are boxed

if allowUniversalInBoxed then
val polyType = fn.tpe.widen.asInstanceOf[TypeLambda]
for case (arg: TypeTree, pinfo, pname) <- args.lazyZip(polyType.paramInfos).lazyZip((polyType.paramNames)) do
if pinfo.bounds.hi.hasAnnotation(defn.Caps_SealedAnnot) then
def where = if fn.symbol.exists then i" in the body of ${fn.symbol}" else ""
CheckCaptures.disallowRootCapabilitiesIn(arg.knownType,
i"Sealed type variable $pname", " be instantiated to",
i"This is often caused by a local capability$where\nleaking as part of its result.",
tree.srcPos)
case _ =>
traverseChildren(tree)
tree match
Expand Down Expand Up @@ -494,11 +511,10 @@ extends tpd.TreeTraverser:

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

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

def isDuringSetup(using Context): Boolean =
ctx.property(IsDuringSetupKey).isDefined

end Setup
6 changes: 3 additions & 3 deletions compiler/src/dotty/tools/dotc/cc/Synthetics.scala
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,9 @@ object Synthetics:

/** Add capture dependencies to the type of the `apply` or `copy` method of a case class.
* An apply method in a case class like this:
* case class CC(a: {d} A, b: B, {*} c: C)
* case class CC(a: {d} A, b: B, {cap} c: C)
* would get type
* def apply(a': {d} A, b: B, {*} c': C): {a', c'} CC { val a = {a'} A, val c = {c'} C }
* def apply(a': {d} A, b: B, {cap} c': C): {a', c'} CC { val a = {a'} A, val c = {c'} C }
* where `'` is used to indicate the difference between parameter symbol and refinement name.
* Analogous for the copy method.
*/
Expand Down Expand Up @@ -123,7 +123,7 @@ object Synthetics:
case _ =>
info

/** Augment an unapply of type `(x: C): D` to `(x: {*} C): {x} D` */
/** Augment an unapply of type `(x: C): D` to `(x: {cap} C): {x} D` */
private def addUnapplyCaptures(info: Type)(using Context): Type = info match
case info: MethodType =>
val paramInfo :: Nil = info.paramInfos: @unchecked
Expand Down
2 changes: 2 additions & 0 deletions compiler/src/dotty/tools/dotc/config/SourceVersion.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ enum SourceVersion:

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

def isAtMost(v: SourceVersion) = stable.ordinal <= v.ordinal

object SourceVersion extends Property.Key[SourceVersion]:
def defaultSourceVersion = `3.3`

Expand Down
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Definitions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ class Definitions {
* }
* ImpureXYZFunctionN follow this template:
*
* type ImpureXYZFunctionN[-T0,...,-T{N-1}, +R] = {*} XYZFunctionN[T0,...,T{N-1}, R]
* type ImpureXYZFunctionN[-T0,...,-T{N-1}, +R] = {cap} XYZFunctionN[T0,...,T{N-1}, R]
*/
private def newFunctionNType(name: TypeName): Symbol = {
val impure = name.startsWith("Impure")
Expand Down Expand Up @@ -973,6 +973,7 @@ class Definitions {
@tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
@tu lazy val Caps_unsafeUnbox: Symbol = CapsUnsafeModule.requiredMethod("unsafeUnbox")
@tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg")
@tu lazy val Caps_SealedAnnot: ClassSymbol = requiredClass("scala.caps.Sealed")

// Annotation base classes
@tu lazy val AnnotationClass: ClassSymbol = requiredClass("scala.annotation.Annotation")
Expand Down Expand Up @@ -1021,6 +1022,7 @@ class Definitions {
@tu lazy val UncheckedAnnot: ClassSymbol = requiredClass("scala.unchecked")
@tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable")
@tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance")
@tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
@tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
@tu lazy val WithPureFunsAnnot: ClassSymbol = requiredClass("scala.annotation.internal.WithPureFuns")
@tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/core/Flags.scala
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,7 @@ object Flags {
val (SuperParamAliasOrScala2x @ _, SuperParamAlias @ _, Scala2x @ _) = newFlags(26, "<super-param-alias>", "<scala-2.x>")

/** A parameter with a default value / an impure untpd.FunctionWithMods type */
val (_, HasDefault @ _, Impure @ _) = newFlags(27, "<hasdefault>", "<{*}>")
val (_, HasDefault @ _, Impure @ _) = newFlags(27, "<hasdefault>", "<impure>")

/** An extension method, or a collective extension instance */
val (Extension @ _, ExtensionMethod @ _, _) = newFlags(28, "<extension>")
Expand Down
Loading

0 comments on commit d6c643c

Please sign in to comment.