Skip to content

Commit 8b27ecb

Browse files
oderskyodersky
authored
CC: Fix maximal capability handling and expand aliases (#22341)
## 1. 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. ## 2. Expand aliases when mapping explicit types in Setup This is necessary because the compiler is free in previous phases to dealias or not. Therefore, capture checking should not depend on aliasing. The main difference is that now arguments to type aliases are not necessarily boxed. They are boxed only if they need boxing in the dealiased type.
2 parents 0f9e502 + ec86d5e commit 8b27ecb

33 files changed

+211
-128
lines changed

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

+14-1
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,8 @@ object ccConfig:
4646
*/
4747
def useSealed(using Context) =
4848
Feature.sourceVersion.stable != SourceVersion.`3.5`
49-
end ccConfig
5049

50+
end ccConfig
5151

5252
/** Are we at checkCaptures phase? */
5353
def isCaptureChecking(using Context): Boolean =
@@ -629,6 +629,19 @@ class CleanupRetains(using Context) extends TypeMap:
629629
RetainingType(tp, Nil, byName = annot.symbol == defn.RetainsByNameAnnot)
630630
case _ => mapOver(tp)
631631

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

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

+2-2
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

+9-5
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

+10-8
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
@@ -277,7 +278,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
277278
paramInfos = tp.paramInfos.mapConserve(_.dropAllRetains.bounds),
278279
resType = this(tp.resType))
279280
case _ =>
280-
mapOver(tp)
281+
mapFollowingAliases(tp)
281282
addVar(addCaptureRefinements(normalizeCaptures(tp1)), ctx.owner)
282283
end apply
283284
end mapInferred
@@ -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) =
@@ -363,7 +364,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
363364
// Map references to capability classes C to C^
364365
if t.derivesFromCapability && !t.isSingleton && t.typeSymbol != defn.Caps_Exists
365366
then CapturingType(t, defn.universalCSImpliedByCapability, boxed = false)
366-
else normalizeCaptures(mapOver(t))
367+
else normalizeCaptures(mapFollowingAliases(t))
367368
end toCapturing
368369

369370
def fail(msg: Message) =
@@ -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) && (tp.dealias eq tp) =>
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

+6
Original file line numberDiff line numberDiff line change
@@ -2846,6 +2846,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28462846
false
28472847
Existential.isExistentialVar(tp1) && canInstantiateWith(assocExistentials)
28482848

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

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

34823488
object MatchReducer:

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

+5-2
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

+4-1
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/boundschecks2.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,6 @@ object test {
88

99
val foo: C[Tree^] = ??? // error
1010
type T = C[Tree^] // error
11-
val bar: T -> T = ???
11+
//val bar: T -> T = ??? // --> boundschecks3.scala for what happens if we uncomment
1212
val baz: C[Tree^] -> Unit = ??? // error
1313
}

‎tests/neg-custom-args/captures/boundschecks3.check

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
-- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 -----------------------------------------------------
2+
11 | val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
3+
| ^^^^^^
4+
| test.C[box test.Tree^] captures the root capability `cap` in invariant position

‎tests/neg-custom-args/captures/boundschecks3.scala

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
object test {
2+
3+
class Tree
4+
5+
def f[X <: Tree](x: X): Unit = ()
6+
7+
class C[X <: Tree](x: X)
8+
9+
val foo: C[Tree^] = ??? // hidden error
10+
type T = C[Tree^] // hidden error
11+
val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
12+
val baz: C[Tree^] -> Unit = ??? // hidden error
13+
}

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

+14
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:10 ------------------------------
2+
14 | x.value(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:10 ------------------------------
9+
28 | x.value(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/neg-custom-args/captures/box-adapt-cases.scala

+8-8
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,29 @@
11
trait Cap { def use(): Int }
22

33
def test1(): Unit = {
4-
type Id[X] = [T] -> (op: X => T) -> T
4+
class Id[X](val value: [T] -> (op: X => T) -> T)
55

66
val x: Id[Cap^] = ???
7-
x(cap => cap.use())
7+
x.value(cap => cap.use())
88
}
99

1010
def test2(io: Cap^): Unit = {
11-
type Id[X] = [T] -> (op: X -> T) -> T
11+
class Id[X](val value: [T] -> (op: X -> T) -> T)
1212

1313
val x: Id[Cap^{io}] = ???
14-
x(cap => cap.use()) // error
14+
x.value(cap => cap.use()) // error
1515
}
1616

1717
def test3(io: Cap^): Unit = {
18-
type Id[X] = [T] -> (op: X ->{io} T) -> T
18+
class Id[X](val value: [T] -> (op: X ->{io} T) -> T)
1919

2020
val x: Id[Cap^{io}] = ???
21-
x(cap => cap.use()) // ok
21+
x.value(cap => cap.use()) // ok
2222
}
2323

2424
def test4(io: Cap^, fs: Cap^): Unit = {
25-
type Id[X] = [T] -> (op: X ->{io} T) -> T
25+
class Id[X](val value: [T] -> (op: X ->{io} T) -> T)
2626

2727
val x: Id[Cap^{io, fs}] = ???
28-
x(cap => cap.use()) // error
28+
x.value(cap => cap.use()) // error
2929
}

‎tests/neg-custom-args/captures/box-adapt-cov.scala

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
trait Cap
22

33
def test1(io: Cap^) = {
4-
type Op[X] = [T] -> Unit -> X
4+
class Op[+X](val value: [T] -> Unit -> X)
55
val f: Op[Cap^{io}] = ???
6-
val x: [T] -> Unit -> Cap^{io} = f // error
6+
val x: [T] -> Unit -> Cap^{io} = f.value // error
77
}
88

99
def test2(io: Cap^) = {
10-
type Op[X] = [T] -> Unit -> X^{io}
10+
class Op[+X](val value: [T] -> Unit -> X^{io})
1111
val f: Op[Cap^{io}] = ???
12-
val x: Unit -> Cap^{io} = f[Unit] // error
13-
val x1: Unit ->{io} Cap^{io} = f[Unit] // ok
12+
val x: Unit -> Cap^{io} = f.value[Unit] // error
13+
val x1: Unit ->{io} Cap^{io} = f.value[Unit] // ok
1414
}

‎tests/neg-custom-args/captures/box-adapt-depfun.scala

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
11
trait Cap { def use(): Int }
22

33
def test1(io: Cap^): Unit = {
4-
type Id[X] = [T] -> (op: X ->{io} T) -> T
4+
class Id[X](val value: [T] -> (op: X ->{io} T) -> T)
55

66
val x: Id[Cap]^{io} = ???
7-
x(cap => cap.use()) // ok
7+
x.value(cap => cap.use()) // ok
88
}
99

1010
def test2(io: Cap^): Unit = {
11-
type Id[X] = [T] -> (op: (x: X) ->{io} T) -> T
11+
class Id[X](val value: [T] -> (op: (x: X) ->{io} T) -> T)
1212

1313
val x: Id[Cap^{io}] = ???
14-
x(cap => cap.use())
14+
x.value(cap => cap.use())
1515
// should work when the expected type is a dependent function
1616
}
1717

1818
def test3(io: Cap^): Unit = {
19-
type Id[X] = [T] -> (op: (x: X) ->{} T) -> T
19+
class Id[X](val value: [T] -> (op: (x: X) ->{} T) -> T)
2020

2121
val x: Id[Cap^{io}] = ???
22-
x(cap => cap.use()) // error
22+
x.value(cap => cap.use()) // error
2323
}

‎tests/neg-custom-args/captures/box-adapt-typefun.scala

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
trait Cap { def use(): Int }
22

33
def test1(io: Cap^): Unit = {
4-
type Op[X] = [T] -> X -> Unit
4+
class Op[X](val value: [T] -> X -> Unit)
55
val f: [T] -> (Cap^{io}) -> Unit = ???
6-
val op: Op[Cap^{io}] = f // error
6+
val op: Op[Cap^{io}] = Op(f) // was error, now ok
77
}
88

99
def test2(io: Cap^): Unit = {
10-
type Lazy[X] = [T] -> Unit -> X
10+
class Lazy[X](val value: [T] -> Unit -> X)
1111
val f: Lazy[Cap^{io}] = ???
12-
val test: [T] -> Unit -> (Cap^{io}) = f // error
12+
val test: [T] -> Unit -> (Cap^{io}) = f.value // error
1313
}

‎tests/neg-custom-args/captures/capt1.check

+6-6
Original file line numberDiff line numberDiff line change
@@ -36,15 +36,15 @@
3636
-- Error: tests/neg-custom-args/captures/capt1.scala:34:16 -------------------------------------------------------------
3737
34 | val z2 = h[() -> Cap](() => x) // error // error
3838
| ^^^^^^^^^
39-
| Type variable X of method h cannot be instantiated to () -> box C^ since
40-
| the part box C^ of that type captures the root capability `cap`.
39+
| Type variable X of method h cannot be instantiated to () -> (ex$15: caps.Exists) -> C^{ex$15} since
40+
| the part C^{ex$15} of that type captures the root capability `cap`.
4141
-- Error: tests/neg-custom-args/captures/capt1.scala:34:30 -------------------------------------------------------------
4242
34 | val z2 = h[() -> Cap](() => x) // error // error
4343
| ^
44-
| reference (x : C^) is not included in the allowed capture set {}
45-
| of an enclosing function literal with expected type () -> box C^
44+
| reference (x : C^) is not included in the allowed capture set {}
45+
| of an enclosing function literal with expected type () -> (ex$15: caps.Exists) -> C^{ex$15}
4646
-- Error: tests/neg-custom-args/captures/capt1.scala:36:13 -------------------------------------------------------------
4747
36 | val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // error
4848
| ^^^^^^^^^^^^^^^^^^^^^^^
49-
| Type variable X of method h cannot be instantiated to box () ->{x} Cap since
50-
| the part Cap of that type captures the root capability `cap`.
49+
| Type variable X of method h cannot be instantiated to box () ->{x} (ex$20: caps.Exists) -> C^{ex$20} since
50+
| the part C^{ex$20} of that type captures the root capability `cap`.

‎tests/neg-custom-args/captures/cc-ex-conformance.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -21,5 +21,5 @@ def Test =
2121
val ex3: EX3 = ???
2222
val ex4: EX4 = ???
2323
val _: EX4 = ex3 // ok
24-
val _: EX4 = ex4
24+
val _: EX4 = ex4 // error (???) Probably since we also introduce existentials on expansion
2525
val _: EX3 = ex4 // error

0 commit comments

Comments
 (0)