Skip to content

Commit 43c6ee7

Browse files
authored
Implement boxing for singleton type arguments (#23418)
A type `A[b.type]` with a singleton type argument is converted to `A[box b.type^{b}]` so that the box status is recorded. Since box status only comes with CapturingTypes we have to convert the singleton type to a capturing type. Fixes #23207
2 parents d944b61 + d269b89 commit 43c6ee7

File tree

6 files changed

+99
-40
lines changed

6 files changed

+99
-40
lines changed

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

Lines changed: 38 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,39 @@ extension (tp: Type)
203203
case _ =>
204204
tp
205205

206+
/** If `tp` is an unboxed capturing type or a function returning an unboxed capturing type,
207+
* convert it to be boxed.
208+
*/
209+
def boxDeeply(using Context): Type =
210+
def recur(tp: Type): Type = tp.dealiasKeepAnnotsAndOpaques match
211+
case tp @ CapturingType(parent, refs) =>
212+
if tp.isBoxed || parent.derivesFrom(defn.Caps_CapSet) then tp
213+
else tp.boxed
214+
case tp @ AnnotatedType(parent, ann) =>
215+
if ann.symbol.isRetains && !parent.derivesFrom(defn.Caps_CapSet)
216+
then CapturingType(parent, ann.tree.toCaptureSet, boxed = true)
217+
else tp.derivedAnnotatedType(parent.boxDeeply, ann)
218+
case tp: (Capability & SingletonType) if tp.isTrackableRef && !tp.isAlwaysPure =>
219+
recur(CapturingType(tp, CaptureSet(tp)))
220+
case tp1 @ AppliedType(tycon, args) if defn.isNonRefinedFunction(tp1) =>
221+
val res = args.last
222+
val boxedRes = recur(res)
223+
if boxedRes eq res then tp
224+
else tp1.derivedAppliedType(tycon, args.init :+ boxedRes)
225+
case tp1 @ defn.RefinedFunctionOf(rinfo: MethodType) =>
226+
val boxedRinfo = recur(rinfo)
227+
if boxedRinfo eq rinfo then tp
228+
else boxedRinfo.toFunctionType(alwaysDependent = true)
229+
case tp1: MethodOrPoly =>
230+
val res = tp1.resType
231+
val boxedRes = recur(res)
232+
if boxedRes eq res then tp
233+
else tp1.derivedLambdaType(resType = boxedRes)
234+
case _ => tp
235+
tp match
236+
case tp: MethodOrPoly => tp // don't box results of methods outside refinements
237+
case _ => recur(tp)
238+
206239
/** The capture set consisting of all top-level captures of `tp` that appear under a box.
207240
* Unlike for `boxed` this also considers parents of capture types, unions and
208241
* intersections, and type proxies other than abstract types.
@@ -621,9 +654,12 @@ object ContainsImpl:
621654
object ContainsParam:
622655
def unapply(sym: Symbol)(using Context): Option[(TypeRef, Capability)] =
623656
sym.info.dealias match
624-
case AppliedType(tycon, (cs: TypeRef) :: (ref: Capability) :: Nil)
657+
case AppliedType(tycon, (cs: TypeRef) :: arg2 :: Nil)
625658
if tycon.typeSymbol == defn.Caps_ContainsTrait
626-
&& cs.typeSymbol.isAbstractOrParamType => Some((cs, ref))
659+
&& cs.typeSymbol.isAbstractOrParamType =>
660+
arg2.stripCapturing match // ref.type was converted to box ref.type^{ref} by boxing
661+
case ref: Capability => Some((cs, ref))
662+
case _ => None
627663
case _ => None
628664

629665
/** A class encapsulating the assumulator logic needed for `CaptureSet.ofTypeDeeply`

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

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -684,6 +684,7 @@ class CheckCaptures extends Recheck, SymTransformer:
684684
// - the selection is either a trackable capture reference or a pure type
685685
if noWiden(selType, pt)
686686
|| qualType.isBoxedCapturing
687+
|| selType.isBoxedCapturing
687688
|| selWiden.isBoxedCapturing
688689
|| selType.isTrackableRef
689690
|| selWiden.captureSet.isAlwaysEmpty
@@ -882,7 +883,7 @@ class CheckCaptures extends Recheck, SymTransformer:
882883
val cs = csArg.nuType.captureSet
883884
val ref = refArg.nuType
884885
capt.println(i"check contains $cs , $ref")
885-
ref match
886+
ref.stripCapturing match
886887
case ref: Capability if ref.isTracked =>
887888
checkElem(ref, cs, tree.srcPos)
888889
case _ =>
@@ -1677,7 +1678,7 @@ class CheckCaptures extends Recheck, SymTransformer:
16771678
actual.isSingleton
16781679
&& expected.match
16791680
case expected: PathSelectionProto => !expected.sym.isOneOf(UnstableValueFlags)
1680-
case _ => expected.isSingleton || expected == LhsProto
1681+
case _ => expected.stripCapturing.isSingleton || expected == LhsProto
16811682

16821683
/** Adapt `actual` type to `expected` type. This involves:
16831684
* - narrow toplevel captures of `x`'s underlying type to `{x}` according to CC's VAR rule
@@ -1686,7 +1687,14 @@ class CheckCaptures extends Recheck, SymTransformer:
16861687
*/
16871688
def adapt(actual: Type, expected: Type, tree: Tree)(using Context): Type =
16881689
if noWiden(actual, expected) then
1689-
actual
1690+
expected match
1691+
case expected @ CapturingType(_, _) if expected.isBoxed =>
1692+
// actual is a singleton type and expected is of the form box x.type^cs.
1693+
// Convert actual to the same form.
1694+
actual.boxDeeply
1695+
.showing(i"adapt single $actual / $result vs $expected", capt)
1696+
case _ =>
1697+
actual
16901698
else
16911699
// Compute the widened type. Drop `@use` and `@consume` annotations from the type,
16921700
// since they obscures the capturing type.

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

Lines changed: 4 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -162,37 +162,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
162162
else symd
163163
end transformSym
164164

165-
/** If `tp` is an unboxed capturing type or a function returning an unboxed capturing type,
166-
* convert it to be boxed.
167-
*/
168-
private def box(tp: Type)(using Context): Type =
169-
def recur(tp: Type): Type = tp.dealiasKeepAnnotsAndOpaques match
170-
case tp @ CapturingType(parent, refs) =>
171-
if tp.isBoxed || parent.derivesFrom(defn.Caps_CapSet) then tp
172-
else tp.boxed
173-
case tp @ AnnotatedType(parent, ann) =>
174-
if ann.symbol.isRetains && !parent.derivesFrom(defn.Caps_CapSet)
175-
then CapturingType(parent, ann.tree.toCaptureSet, boxed = true)
176-
else tp.derivedAnnotatedType(box(parent), ann)
177-
case tp1 @ AppliedType(tycon, args) if defn.isNonRefinedFunction(tp1) =>
178-
val res = args.last
179-
val boxedRes = recur(res)
180-
if boxedRes eq res then tp
181-
else tp1.derivedAppliedType(tycon, args.init :+ boxedRes)
182-
case tp1 @ defn.RefinedFunctionOf(rinfo: MethodType) =>
183-
val boxedRinfo = recur(rinfo)
184-
if boxedRinfo eq rinfo then tp
185-
else boxedRinfo.toFunctionType(alwaysDependent = true)
186-
case tp1: MethodOrPoly =>
187-
val res = tp1.resType
188-
val boxedRes = recur(res)
189-
if boxedRes eq res then tp
190-
else tp1.derivedLambdaType(resType = boxedRes)
191-
case _ => tp
192-
tp match
193-
case tp: MethodOrPoly => tp // don't box results of methods outside refinements
194-
case _ => recur(tp)
195-
196165
private trait SetupTypeMap extends FollowAliasesMap:
197166
private var isTopLevel = true
198167

@@ -257,9 +226,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
257226
CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
258227
case tp @ AppliedType(tycon, args)
259228
if !defn.isFunctionClass(tp.dealias.typeSymbol) && (tp.dealias eq tp) =>
260-
tp.derivedAppliedType(tycon, args.mapConserve(box))
229+
tp.derivedAppliedType(tycon, args.mapConserve(_.boxDeeply))
261230
case tp: RealTypeBounds =>
262-
tp.derivedTypeBounds(tp.lo, box(tp.hi))
231+
tp.derivedTypeBounds(tp.lo, tp.hi.boxDeeply)
263232
case tp: LazyRef =>
264233
normalizeCaptures(tp.ref)
265234
case _ =>
@@ -542,7 +511,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
542511
if tree.isInferred
543512
then transformInferredType(tree.tpe)
544513
else transformExplicitType(tree.tpe, sym, freshen = !boxed, tptToCheck = tree)
545-
if boxed then transformed = box(transformed)
514+
if boxed then transformed = transformed.boxDeeply
546515
tree.setNuType(
547516
if sym.hasAnnotation(defn.UncheckedCapturesAnnot) then makeUnchecked(transformed)
548517
else transformed)
@@ -612,7 +581,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
612581

613582
case tree @ SeqLiteral(elems, tpt: TypeTree) =>
614583
traverse(elems)
615-
tpt.setNuType(box(transformInferredType(tpt.tpe)))
584+
tpt.setNuType(transformInferredType(tpt.tpe).boxDeeply)
616585

617586
case tree @ Try(body, catches, finalizer) =>
618587
val tryOwner = firstCanThrowEvidence(body) match
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:15:17 ---------------------------------------
2+
15 | val a: A = box.x // error
3+
| ^^^^^
4+
| Found: (box.x : (b : B^{io})^{b})
5+
| Required: A
6+
|
7+
| longer explanation available when compiling with `-explain`
8+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:16:11 ---------------------------------------
9+
16 | b.getBox.x // error
10+
| ^^^^^^^^^^
11+
| Found: (Box[(b : B^{io})^{b}]#x : (b : B^{io})^{b})
12+
| Required: A^?
13+
|
14+
| longer explanation available when compiling with `-explain`
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import language.experimental.captureChecking
2+
import caps.*
3+
4+
case class Box[T](x: T)
5+
6+
class A:
7+
def getBox: Box[this.type] = Box(this)
8+
9+
def leak(io: AnyRef^): A =
10+
class B extends A:
11+
val hide: AnyRef^{io} = io
12+
13+
val b = new B
14+
val box = b.getBox
15+
val a: A = box.x // error
16+
b.getBox.x // error
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
class Box[+T](x: T)
2+
3+
def Test(c: Object^): Unit =
4+
val x: Object^{c} = c
5+
6+
val x2: x.type^{x} = x
7+
val x3: x.type = x2
8+
9+
val b: Box[x.type] = Box(x)
10+
val b1: Box[x.type^{x}] = b
11+
val b2: Box[x.type] = b1
12+
13+
14+
15+
16+

0 commit comments

Comments
 (0)