Skip to content

Commit ecf3428

Browse files
oderskyodersky
committed
Fix various issues with maximal capabilities
The subsumes check mistakenly allowed any capability to subsume `cap`, since `cap` is expanded as `caps.cap`, and by the path subcapturing rule `caps.cap <: caps`, where the capture set of `caps` is empty. This allowed quite a few hidden errors to go through. This commit fixes the subcapturing issue and all downstream issues caused by that fix. In particular: - Don't use path comparison for `x subsumes caps.cap` - Don't allow an opened existential on the left of a comparison to leak into a capture set on the right. This would give a "leak" error later in healCaptures. - Print pre-cc annotated capturing types with @retains annotations with `^`. The annotation is already rendered as a set in this case, but the `^` was missing. - Don't recheck `_` right hand sides of uninitialized variables. These were handled in ways that broke freshness checking. The new `uninitialied` scheme does not have this problem.
1 parent a50a1e4 commit ecf3428

File tree

15 files changed

+120
-56
lines changed

15 files changed

+120
-56
lines changed

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ object ccConfig:
4646
*/
4747
def useSealed(using Context) =
4848
Feature.sourceVersion.stable != SourceVersion.`3.5`
49+
4950
end ccConfig
5051

5152

@@ -629,6 +630,19 @@ class CleanupRetains(using Context) extends TypeMap:
629630
RetainingType(tp, Nil, byName = annot.symbol == defn.RetainsByNameAnnot)
630631
case _ => mapOver(tp)
631632

633+
/** A typemap that follows aliases and keeps their transformed results if
634+
* there is a change.
635+
*/
636+
trait FollowAliasesMap(using Context) extends TypeMap:
637+
var follow = true // Used for debugging so that we can compare results with and w/o following.
638+
def mapFollowingAliases(t: Type): Type =
639+
val t1 = t.dealiasKeepAnnots
640+
if follow && (t1 ne t) then
641+
val t2 = apply(t1)
642+
if t2 ne t1 then t2
643+
else t
644+
else mapOver(t)
645+
632646
/** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
633647
* capability as a tree in a @retains annotation.
634648
*/

‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ trait CaptureRef extends TypeProxy, ValueType:
8383
else
8484
myCaptureSet = CaptureSet.Pending
8585
val computed = CaptureSet.ofInfo(this)
86-
if !isCaptureChecking || underlying.isProvisional then
86+
if !isCaptureChecking || ctx.mode.is(Mode.IgnoreCaptures) || underlying.isProvisional then
8787
myCaptureSet = null
8888
else
8989
myCaptureSet = computed
@@ -124,7 +124,7 @@ trait CaptureRef extends TypeProxy, ValueType:
124124
(this eq y)
125125
|| this.isRootCapability
126126
|| y.match
127-
case y: TermRef =>
127+
case y: TermRef if !y.isRootCapability =>
128128
y.prefix.match
129129
case ypre: CaptureRef =>
130130
this.subsumes(ypre)

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

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -508,8 +508,13 @@ object CaptureSet:
508508
res.addToTrace(this)
509509

510510
private def levelOK(elem: CaptureRef)(using Context): Boolean =
511-
if elem.isRootCapability || Existential.isExistentialVar(elem) then
511+
if elem.isRootCapability then
512512
!noUniversal
513+
else if Existential.isExistentialVar(elem) then
514+
!noUniversal
515+
&& !TypeComparer.isOpenedExistential(elem)
516+
// Opened existentials on the left cannot be added to nested capture sets on the right
517+
// of a comparison. Test case is open-existential.scala.
513518
else elem match
514519
case elem: TermRef if level.isDefined =>
515520
elem.prefix match
@@ -1065,13 +1070,12 @@ object CaptureSet:
10651070

10661071
/** The capture set of the type underlying CaptureRef */
10671072
def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
1068-
case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
1069-
if ref.isTrackableRef then ref.singletonCaptureSet
1070-
else CaptureSet.universal
10711073
case ReachCapability(ref1) =>
10721074
ref1.widen.deepCaptureSet(includeTypevars = true)
10731075
.showing(i"Deep capture set of $ref: ${ref1.widen} = ${result}", capt)
1074-
case _ => ofType(ref.underlying, followResult = true)
1076+
case _ =>
1077+
if ref.isMaxCapability then ref.singletonCaptureSet
1078+
else ofType(ref.underlying, followResult = true)
10751079

10761080
/** Capture set of a type */
10771081
def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =

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

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ import ast.tpd, tpd.*
1313
import transform.{PreRecheck, Recheck}, Recheck.*
1414
import CaptureSet.{IdentityCaptRefMap, IdempotentCaptRefMap}
1515
import Synthetics.isExcluded
16-
import util.{Property, SimpleIdentitySet}
16+
import util.SimpleIdentitySet
1717
import reporting.Message
1818
import printing.{Printer, Texts}, Texts.{Text, Str}
1919
import collection.mutable
@@ -40,7 +40,7 @@ trait SetupAPI:
4040

4141
object Setup:
4242

43-
val name: String = "ccSetup"
43+
val name: String = "setupCC"
4444
val description: String = "prepare compilation unit for capture checking"
4545

4646
/** Recognizer for `res $throws exc`, returning `(res, exc)` in case of success */
@@ -192,11 +192,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
192192
* 3. Refine other class types C by adding capture set variables to their parameter getters
193193
* (see addCaptureRefinements), provided `refine` is true.
194194
* 4. Add capture set variables to all types that can be tracked
195+
* 5. Perform normalizeCaptures
195196
*
196197
* Polytype bounds are only cleaned using step 1, but not otherwise transformed.
197198
*/
198199
private def transformInferredType(tp: Type)(using Context): Type =
199-
def mapInferred(refine: Boolean): TypeMap = new TypeMap:
200+
def mapInferred(refine: Boolean): TypeMap = new TypeMap with FollowAliasesMap:
200201
override def toString = "map inferred"
201202

202203
/** Refine a possibly applied class type C where the class has tracked parameters
@@ -299,9 +300,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
299300
* 3. Add universal capture sets to types deriving from Capability
300301
* 4. Map `cap` in function result types to existentially bound variables.
301302
* 5. Schedule deferred well-formed tests for types with retains annotations.
303+
* 6. Perform normalizeCaptures
302304
*/
303305
private def transformExplicitType(tp: Type, tptToCheck: Tree = EmptyTree)(using Context): Type =
304-
val toCapturing = new DeepTypeMap:
306+
val toCapturing = new DeepTypeMap with FollowAliasesMap:
305307
override def toString = "expand aliases"
306308

307309
/** Expand $throws aliases. This is hard-coded here since $throws aliases in stdlib
@@ -337,7 +339,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
337339
case tp @ CapturingType(parent, refs)
338340
if (refs eq defn.universalCSImpliedByCapability) && !tp.isBoxedCapturing =>
339341
parent
340-
case tp @ CapturingType(parent, refs) => tp
341342
case _ => tp
342343

343344
def apply(t: Type) =
@@ -819,7 +820,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
819820
CapturingType(OrType(parent1, tp2, tp.isSoft), refs1, tp1.isBoxed)
820821
case tp @ OrType(tp1, tp2 @ CapturingType(parent2, refs2)) =>
821822
CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
822-
case tp @ AppliedType(tycon, args) if !defn.isFunctionClass(tp.dealias.typeSymbol) =>
823+
case tp @ AppliedType(tycon, args)
824+
if !defn.isFunctionClass(tp.dealias.typeSymbol) =>
823825
tp.derivedAppliedType(tycon, args.mapConserve(box))
824826
case tp: RealTypeBounds =>
825827
tp.derivedTypeBounds(tp.lo, box(tp.hi))

‎compiler/src/dotty/tools/dotc/core/TypeComparer.scala‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2845,6 +2845,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28452845
false
28462846
Existential.isExistentialVar(tp1) && canInstantiateWith(assocExistentials)
28472847

2848+
def isOpenedExistential(ref: CaptureRef)(using Context): Boolean =
2849+
openedExistentials.contains(ref)
2850+
28482851
/** bi-map taking existentials to the left of a comparison to matching
28492852
* existentials on the right. This is not a bijection. However
28502853
* we have `forwards(backwards(bv)) == bv` for an existentially bound `bv`.
@@ -3476,6 +3479,9 @@ object TypeComparer {
34763479

34773480
def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
34783481
comparing(_.subsumesExistentially(tp1, tp2))
3482+
3483+
def isOpenedExistential(ref: CaptureRef)(using Context) =
3484+
comparing(_.isOpenedExistential(ref))
34793485
}
34803486

34813487
object MatchReducer:

‎compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ import util.SourcePosition
1515
import scala.util.control.NonFatal
1616
import scala.annotation.switch
1717
import config.{Config, Feature}
18-
import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike}
18+
import cc.*
1919

2020
class PlainPrinter(_ctx: Context) extends Printer {
2121

@@ -297,7 +297,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
297297
else if (annot.symbol == defn.IntoAnnot || annot.symbol == defn.IntoParamAnnot)
298298
&& !printDebug
299299
then atPrec(GlobalPrec)( Str("into ") ~ toText(tpe) )
300-
else toTextLocal(tpe) ~ " " ~ toText(annot)
300+
else if annot.isInstanceOf[CaptureAnnotation] then
301+
toTextLocal(tpe) ~ "^" ~ toText(annot)
302+
else
303+
toTextLocal(tpe) ~ " " ~ toText(annot)
301304
case FlexibleType(_, tpe) =>
302305
"(" ~ toText(tpe) ~ ")?"
303306
case tp: TypeVar =>

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -255,7 +255,10 @@ abstract class Recheck extends Phase, SymTransformer:
255255

256256
def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
257257
val resType = recheck(tree.tpt)
258-
if tree.rhs.isEmpty then resType
258+
def isUninitWildcard = tree.rhs match
259+
case Ident(nme.WILDCARD) => tree.symbol.is(Mutable)
260+
case _ => false
261+
if tree.rhs.isEmpty || isUninitWildcard then resType
259262
else recheck(tree.rhs, resType)
260263

261264
def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =

‎tests/neg-custom-args/captures/box-adapt-cases.check‎

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/box-adapt-cases.scala:14:4 -------------------------------
2+
14 | x(cap => cap.use()) // error
3+
| ^^^^^^^^^^^^^^^^
4+
| Found: (cap: box Cap^?) ->{io} Int
5+
| Required: (cap: box Cap^{io}) -> Int
6+
|
7+
| longer explanation available when compiling with `-explain`
8+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:28:4 -------------------------------
9+
28 | x(cap => cap.use()) // error
10+
| ^^^^^^^^^^^^^^^^
11+
| Found: (cap: box Cap^?) ->{io, fs} Int
12+
| Required: (cap: box Cap^{io, fs}) ->{io} Int
13+
|
14+
| longer explanation available when compiling with `-explain`

‎tests/pos-custom-args/captures/boxmap-paper.scala‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,13 @@
11

2-
type Cell[+T] = [K] -> (T => K) -> K
2+
type Cell_orig[+T] = [K] -> (T => K) -> K
33

4-
def cell[T](x: T): Cell[T] =
4+
def cell_orig[T](x: T): Cell_orig[T] =
5+
[K] => (k: T => K) => k(x)
6+
7+
class Cell[+T](val value: [K] -> (T => K) -> K):
8+
def apply[K]: (T => K) -> K = value[K]
9+
10+
def cell[T](x: T): Cell[T] = Cell:
511
[K] => (k: T => K) => k(x)
612

713
def get[T](c: Cell[T]): T = c[T](identity)
@@ -22,6 +28,10 @@ def test(io: IO^) =
2228

2329
val loggedOne: () ->{io} Int = () => { io.print("1"); 1 }
2430

31+
// We have a leakage of io because type arguments to alias type `Cell` are not boxed.
32+
val c_orig: Cell[() ->{io} Int]^{io}
33+
= cell[() ->{io} Int](loggedOne)
34+
2535
val c: Cell[() ->{io} Int]
2636
= cell[() ->{io} Int](loggedOne)
2737

‎tests/pos-custom-args/captures/cc-cast.scala‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
import annotation.unchecked.uncheckedCaptures
2+
import compiletime.uninitialized
3+
4+
def foo(x: Int => Int) = ()
5+
6+
7+
object Test:
8+
def test(x: Object) =
9+
foo(x.asInstanceOf[Int => Int])
10+
11+
@uncheckedCaptures var x1: Object^ = uninitialized
12+
@uncheckedCaptures var x2: Object^ = _

0 commit comments

Comments
 (0)