Skip to content

Commit 19e6529

Browse files
committed
Enable existential capabilities
Enabled from 3.5. There are still a number of open questions - Clarify type inference with existentials propagating into capture sets. Right now, no pos or run test exercises this. - Also map arguments of function to existentials (at least double flip ones). - Adapt reach capabilities and drop previous restrictions.
1 parent 8d60973 commit 19e6529

File tree

10 files changed

+161
-153
lines changed

10 files changed

+161
-153
lines changed

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

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import StdNames.nme
1515
import config.Feature
1616
import collection.mutable
1717
import CCState.*
18+
import reporting.Message
1819

1920
private val Captures: Key[CaptureSet] = Key()
2021

@@ -26,7 +27,8 @@ object ccConfig:
2627
*/
2728
inline val allowUnsoundMaps = false
2829

29-
val useExistentials = false
30+
def useExistentials(using Context) =
31+
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.5`)
3032

3133
/** If true, use `sealed` as encapsulation mechanism instead of the
3234
* previous global retriction that `cap` can't be boxed or unboxed.
@@ -69,6 +71,11 @@ class CCState:
6971
*/
7072
var levelError: Option[CaptureSet.CompareResult.LevelError] = None
7173

74+
/** Warnings relating to upper approximations of capture sets with
75+
* existentially bound variables.
76+
*/
77+
val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer()
78+
7279
private var curLevel: Level = outermostLevel
7380
private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
7481

@@ -356,6 +363,7 @@ extension (tp: Type)
356363
ok = false
357364
case _ =>
358365
traverseChildren(t)
366+
end CheckContraCaps
359367

360368
object narrowCaps extends TypeMap:
361369
/** Has the variance been flipped at this point? */
@@ -368,12 +376,19 @@ extension (tp: Type)
368376
t.dealias match
369377
case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
370378
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
379+
case t @ FunctionOrMethod(args, res @ Existential(_, _))
380+
if args.forall(_.isAlwaysPure) =>
381+
// Also map existentials in results to reach capabilities if all
382+
// preceding arguments are known to be always pure
383+
apply(t.derivedFunctionOrMethod(args, Existential.toCap(res)))
371384
case _ => t match
372385
case t @ CapturingType(p, cs) =>
373386
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
374387
case t =>
375388
mapOver(t)
376389
finally isFlipped = saved
390+
end narrowCaps
391+
377392
ref match
378393
case ref: CaptureRef if ref.isTrackableRef =>
379394
val checker = new CheckContraCaps

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

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -562,7 +562,14 @@ object CaptureSet:
562562
universal
563563
else
564564
computingApprox = true
565-
try computeApprox(origin).ensuring(_.isConst)
565+
try
566+
val approx = computeApprox(origin).ensuring(_.isConst)
567+
if approx.elems.exists(Existential.isExistentialVar(_)) then
568+
ccState.approxWarnings +=
569+
em"""Capture set variable $this gets upper-approximated
570+
|to existential variable from $approx, using {cap} instead."""
571+
universal
572+
else approx
566573
finally computingApprox = false
567574

568575
/** The intersection of all upper approximations of dependent sets */
@@ -757,9 +764,8 @@ object CaptureSet:
757764
CompareResult.OK
758765
else
759766
source.tryInclude(bimap.backward(elem), this)
760-
.showing(i"propagating new elem $elem backward from $this to $source = $result", capt)
761-
.andAlso:
762-
addNewElem(elem)
767+
.showing(i"propagating new elem $elem backward from $this to $source = $result", captDebug)
768+
.andAlso(addNewElem(elem))
763769

764770
/** For a BiTypeMap, supertypes of the mapped type also constrain
765771
* the source via the inverse type mapping and vice versa. That is, if

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

Lines changed: 61 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -223,6 +223,9 @@ class CheckCaptures extends Recheck, SymTransformer:
223223
if tpt.isInstanceOf[InferredTypeTree] then
224224
interpolator().traverse(tpt.knownType)
225225
.showing(i"solved vars in ${tpt.knownType}", capt)
226+
for msg <- ccState.approxWarnings do
227+
report.warning(msg, tpt.srcPos)
228+
ccState.approxWarnings.clear()
226229

227230
/** Assert subcapturing `cs1 <: cs2` */
228231
def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
@@ -492,7 +495,7 @@ class CheckCaptures extends Recheck, SymTransformer:
492495
tp.derivedCapturingType(forceBox(parent), refs)
493496
mapArgUsing(forceBox)
494497
else
495-
super.recheckApply(tree, pt) match
498+
Existential.toCap(super.recheckApply(tree, pt)) match
496499
case appType @ CapturingType(appType1, refs) =>
497500
tree.fun match
498501
case Select(qual, _)
@@ -505,7 +508,7 @@ class CheckCaptures extends Recheck, SymTransformer:
505508
val callCaptures = tree.args.foldLeft(qual.tpe.captureSet): (cs, arg) =>
506509
cs ++ arg.tpe.captureSet
507510
appType.derivedCapturingType(appType1, callCaptures)
508-
.showing(i"narrow $tree: $appType, refs = $refs, qual = ${qual.tpe.captureSet} --> $result", capt)
511+
.showing(i"narrow $tree: $appType, refs = $refs, qual-cs = ${qual.tpe.captureSet} = $result", capt)
509512
case _ => appType
510513
case appType => appType
511514
end recheckApply
@@ -591,7 +594,7 @@ class CheckCaptures extends Recheck, SymTransformer:
591594
i"Sealed type variable $pname", "be instantiated to",
592595
i"This is often caused by a local capability$where\nleaking as part of its result.",
593596
tree.srcPos)
594-
super.recheckTypeApply(tree, pt)
597+
Existential.toCap(super.recheckTypeApply(tree, pt))
595598

596599
override def recheckBlock(tree: Block, pt: Type)(using Context): Type =
597600
inNestedLevel(super.recheckBlock(tree, pt))
@@ -624,7 +627,12 @@ class CheckCaptures extends Recheck, SymTransformer:
624627
// Example is the line `a = x` in neg-custom-args/captures/vars.scala.
625628
// For all other closures, early constraints are preferred since they
626629
// give more localized error messages.
627-
checkConformsExpr(res, pt, expr)
630+
val res1 = Existential.toCapDeeply(res)
631+
val pt1 = Existential.toCapDeeply(pt)
632+
// We need to open existentials here in order not to get vars mixed up in them
633+
// We do the proper check with existentials when we are finished with the closure block.
634+
capt.println(i"pre-check closure $expr of type $res1 against $pt1")
635+
checkConformsExpr(res1, pt1, expr)
628636
recheckDef(mdef, mdef.symbol)
629637
res
630638
finally
@@ -1009,35 +1017,50 @@ class CheckCaptures extends Recheck, SymTransformer:
10091017
*/
10101018
def adaptBoxed(actual: Type, expected: Type, pos: SrcPos, covariant: Boolean, alwaysConst: Boolean, boxErrors: BoxErrors)(using Context): Type =
10111019

1012-
/** Adapt the inner shape type: get the adapted shape type, and the capture set leaked during adaptation
1013-
* @param boxed if true we adapt to a boxed expected type
1014-
*/
1015-
def adaptShape(actualShape: Type, boxed: Boolean): (Type, CaptureSet) = actualShape match
1016-
case FunctionOrMethod(aargs, ares) =>
1017-
val saved = curEnv
1018-
curEnv = Env(
1019-
curEnv.owner, EnvKind.NestedInOwner,
1020-
CaptureSet.Var(curEnv.owner, level = currentLevel),
1021-
if boxed then null else curEnv)
1022-
try
1023-
val (eargs, eres) = expected.dealias.stripCapturing match
1024-
case FunctionOrMethod(eargs, eres) => (eargs, eres)
1025-
case _ => (aargs.map(_ => WildcardType), WildcardType)
1026-
val aargs1 = aargs.zipWithConserve(eargs):
1027-
adaptBoxed(_, _, pos, !covariant, alwaysConst, boxErrors)
1028-
val ares1 = adaptBoxed(ares, eres, pos, covariant, alwaysConst, boxErrors)
1029-
val resTp =
1030-
if (aargs1 eq aargs) && (ares1 eq ares) then actualShape // optimize to avoid redundant matches
1031-
else actualShape.derivedFunctionOrMethod(aargs1, ares1)
1032-
(resTp, CaptureSet(curEnv.captured.elems))
1033-
finally curEnv = saved
1034-
case _ =>
1035-
(actualShape, CaptureSet())
1020+
def recur(actual: Type, expected: Type, covariant: Boolean): Type =
1021+
1022+
/** Adapt the inner shape type: get the adapted shape type, and the capture set leaked during adaptation
1023+
* @param boxed if true we adapt to a boxed expected type
1024+
*/
1025+
def adaptShape(actualShape: Type, boxed: Boolean): (Type, CaptureSet) = actualShape match
1026+
case FunctionOrMethod(aargs, ares) =>
1027+
val saved = curEnv
1028+
curEnv = Env(
1029+
curEnv.owner, EnvKind.NestedInOwner,
1030+
CaptureSet.Var(curEnv.owner, level = currentLevel),
1031+
if boxed then null else curEnv)
1032+
try
1033+
val (eargs, eres) = expected.dealias.stripCapturing match
1034+
case FunctionOrMethod(eargs, eres) => (eargs, eres)
1035+
case _ => (aargs.map(_ => WildcardType), WildcardType)
1036+
val aargs1 = aargs.zipWithConserve(eargs):
1037+
recur(_, _, !covariant)
1038+
val ares1 = recur(ares, eres, covariant)
1039+
val resTp =
1040+
if (aargs1 eq aargs) && (ares1 eq ares) then actualShape // optimize to avoid redundant matches
1041+
else actualShape.derivedFunctionOrMethod(aargs1, ares1)
1042+
(resTp, CaptureSet(curEnv.captured.elems))
1043+
finally curEnv = saved
1044+
case _ =>
1045+
(actualShape, CaptureSet())
1046+
end adaptShape
10361047

1037-
def adaptStr = i"adapting $actual ${if covariant then "~~>" else "<~~"} $expected"
1048+
def adaptStr = i"adapting $actual ${if covariant then "~~>" else "<~~"} $expected"
1049+
1050+
actual match
1051+
case actual @ Existential(_, actualUnpacked) =>
1052+
return Existential.derivedExistentialType(actual):
1053+
recur(actualUnpacked, expected, covariant)
1054+
case _ =>
1055+
expected match
1056+
case expected @ Existential(_, expectedUnpacked) =>
1057+
return recur(actual, expectedUnpacked, covariant)
1058+
case _: WildcardType =>
1059+
return actual
1060+
case _ =>
1061+
1062+
trace(adaptStr, capt, show = true) {
10381063

1039-
if expected.isInstanceOf[WildcardType] then actual
1040-
else trace(adaptStr, recheckr, show = true):
10411064
// Decompose the actual type into the inner shape type, the capture set and the box status
10421065
val actualShape = if actual.isFromJavaObject then actual else actual.stripCapturing
10431066
val actualIsBoxed = actual.isBoxedCapturing
@@ -1099,6 +1122,10 @@ class CheckCaptures extends Recheck, SymTransformer:
10991122
adaptedType(!actualIsBoxed)
11001123
else
11011124
adaptedType(actualIsBoxed)
1125+
}
1126+
end recur
1127+
1128+
recur(actual, expected, covariant)
11021129
end adaptBoxed
11031130

11041131
/** If actual derives from caps.Capability, yet is not a capturing type itself,
@@ -1139,7 +1166,7 @@ class CheckCaptures extends Recheck, SymTransformer:
11391166
widened.withReachCaptures(actual), expected, pos,
11401167
covariant = true, alwaysConst = false, boxErrors)
11411168
if adapted eq widened then normalized
1142-
else adapted.showing(i"adapt boxed $actual vs $expected ===> $adapted", capt)
1169+
else adapted.showing(i"adapt boxed $actual vs $expected = $adapted", capt)
11431170
end adapt
11441171

11451172
/** Check overrides again, taking capture sets into account.
@@ -1154,13 +1181,13 @@ class CheckCaptures extends Recheck, SymTransformer:
11541181
* @param sym symbol of the field definition that is being checked
11551182
*/
11561183
override def checkSubType(actual: Type, expected: Type)(using Context): Boolean =
1157-
val expected1 = alignDependentFunction(addOuterRefs(/*Existential.strip*/(expected), actual), actual.stripCapturing)
1184+
val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
11581185
val actual1 =
11591186
val saved = curEnv
11601187
try
11611188
curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
11621189
val adapted =
1163-
adaptBoxed(/*Existential.strip*/(actual), expected1, srcPos, covariant = true, alwaysConst = true, null)
1190+
adaptBoxed(actual, expected1, srcPos, covariant = true, alwaysConst = true, null)
11641191
actual match
11651192
case _: MethodType =>
11661193
// We remove the capture set resulted from box adaptation for method types,

0 commit comments

Comments
 (0)