Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CC: Fix maximal capability handling and expand aliases #22341

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ object ccConfig:
*/
def useSealed(using Context) =
Feature.sourceVersion.stable != SourceVersion.`3.5`
end ccConfig

end ccConfig

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

/** A typemap that follows aliases and keeps their transformed results if
* there is a change.
*/
trait FollowAliasesMap(using Context) extends TypeMap:
var follow = true // Used for debugging so that we can compare results with and w/o following.
def mapFollowingAliases(t: Type): Type =
val t1 = t.dealiasKeepAnnots
if follow && (t1 ne t) then
val t2 = apply(t1)
if t2 ne t1 then t2
else t
else mapOver(t)

/** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
* capability as a tree in a @retains annotation.
*/
Expand Down
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ trait CaptureRef extends TypeProxy, ValueType:
else
myCaptureSet = CaptureSet.Pending
val computed = CaptureSet.ofInfo(this)
if !isCaptureChecking || underlying.isProvisional then
if !isCaptureChecking || ctx.mode.is(Mode.IgnoreCaptures) || underlying.isProvisional then
myCaptureSet = null
else
myCaptureSet = computed
Expand Down Expand Up @@ -124,7 +124,7 @@ trait CaptureRef extends TypeProxy, ValueType:
(this eq y)
|| this.isRootCapability
|| y.match
case y: TermRef =>
case y: TermRef if !y.isRootCapability =>
y.prefix.match
case ypre: CaptureRef =>
this.subsumes(ypre)
Expand Down
14 changes: 9 additions & 5 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -508,8 +508,13 @@ object CaptureSet:
res.addToTrace(this)

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

/** The capture set of the type underlying CaptureRef */
def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
if ref.isTrackableRef then ref.singletonCaptureSet
else CaptureSet.universal
case ReachCapability(ref1) =>
ref1.widen.deepCaptureSet(includeTypevars = true)
.showing(i"Deep capture set of $ref: ${ref1.widen} = ${result}", capt)
case _ => ofType(ref.underlying, followResult = true)
case _ =>
if ref.isMaxCapability then ref.singletonCaptureSet
else ofType(ref.underlying, followResult = true)

/** Capture set of a type */
def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet =
Expand Down
18 changes: 10 additions & 8 deletions compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import ast.tpd, tpd.*
import transform.{PreRecheck, Recheck}, Recheck.*
import CaptureSet.{IdentityCaptRefMap, IdempotentCaptRefMap}
import Synthetics.isExcluded
import util.{Property, SimpleIdentitySet}
import util.SimpleIdentitySet
import reporting.Message
import printing.{Printer, Texts}, Texts.{Text, Str}
import collection.mutable
Expand All @@ -40,7 +40,7 @@ trait SetupAPI:

object Setup:

val name: String = "ccSetup"
val name: String = "setupCC"
val description: String = "prepare compilation unit for capture checking"

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

/** Refine a possibly applied class type C where the class has tracked parameters
Expand Down Expand Up @@ -277,7 +278,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
paramInfos = tp.paramInfos.mapConserve(_.dropAllRetains.bounds),
resType = this(tp.resType))
case _ =>
mapOver(tp)
mapFollowingAliases(tp)
addVar(addCaptureRefinements(normalizeCaptures(tp1)), ctx.owner)
end apply
end mapInferred
Expand All @@ -299,9 +300,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
* 3. Add universal capture sets to types deriving from Capability
* 4. Map `cap` in function result types to existentially bound variables.
* 5. Schedule deferred well-formed tests for types with retains annotations.
* 6. Perform normalizeCaptures
*/
private def transformExplicitType(tp: Type, tptToCheck: Tree = EmptyTree)(using Context): Type =
val toCapturing = new DeepTypeMap:
val toCapturing = new DeepTypeMap with FollowAliasesMap:
override def toString = "expand aliases"

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

def apply(t: Type) =
Expand All @@ -363,7 +364,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
// Map references to capability classes C to C^
if t.derivesFromCapability && !t.isSingleton && t.typeSymbol != defn.Caps_Exists
then CapturingType(t, defn.universalCSImpliedByCapability, boxed = false)
else normalizeCaptures(mapOver(t))
else normalizeCaptures(mapFollowingAliases(t))
end toCapturing

def fail(msg: Message) =
Expand Down Expand Up @@ -819,7 +820,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
CapturingType(OrType(parent1, tp2, tp.isSoft), refs1, tp1.isBoxed)
case tp @ OrType(tp1, tp2 @ CapturingType(parent2, refs2)) =>
CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
case tp @ AppliedType(tycon, args) if !defn.isFunctionClass(tp.dealias.typeSymbol) =>
case tp @ AppliedType(tycon, args)
if !defn.isFunctionClass(tp.dealias.typeSymbol) && (tp.dealias eq tp) =>
tp.derivedAppliedType(tycon, args.mapConserve(box))
case tp: RealTypeBounds =>
tp.derivedTypeBounds(tp.lo, box(tp.hi))
Expand Down
6 changes: 6 additions & 0 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2845,6 +2845,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
false
Existential.isExistentialVar(tp1) && canInstantiateWith(assocExistentials)

def isOpenedExistential(ref: CaptureRef)(using Context): Boolean =
openedExistentials.contains(ref)

/** bi-map taking existentials to the left of a comparison to matching
* existentials on the right. This is not a bijection. However
* we have `forwards(backwards(bv)) == bv` for an existentially bound `bv`.
Expand Down Expand Up @@ -3476,6 +3479,9 @@ object TypeComparer {

def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
comparing(_.subsumesExistentially(tp1, tp2))

def isOpenedExistential(ref: CaptureRef)(using Context) =
comparing(_.isOpenedExistential(ref))
}

object MatchReducer:
Expand Down
7 changes: 5 additions & 2 deletions compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ import util.SourcePosition
import scala.util.control.NonFatal
import scala.annotation.switch
import config.{Config, Feature}
import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, retainedElems, isRetainsLike}
import cc.*

class PlainPrinter(_ctx: Context) extends Printer {

Expand Down Expand Up @@ -297,7 +297,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
else if (annot.symbol == defn.IntoAnnot || annot.symbol == defn.IntoParamAnnot)
&& !printDebug
then atPrec(GlobalPrec)( Str("into ") ~ toText(tpe) )
else toTextLocal(tpe) ~ " " ~ toText(annot)
else if annot.isInstanceOf[CaptureAnnotation] then
toTextLocal(tpe) ~ "^" ~ toText(annot)
else
toTextLocal(tpe) ~ " " ~ toText(annot)
case FlexibleType(_, tpe) =>
"(" ~ toText(tpe) ~ ")?"
case tp: TypeVar =>
Expand Down
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/dotc/transform/Recheck.scala
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,10 @@ abstract class Recheck extends Phase, SymTransformer:

def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
val resType = recheck(tree.tpt)
if tree.rhs.isEmpty then resType
def isUninitWildcard = tree.rhs match
case Ident(nme.WILDCARD) => tree.symbol.is(Mutable)
case _ => false
if tree.rhs.isEmpty || isUninitWildcard then resType
else recheck(tree.rhs, resType)

def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/boundschecks2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,6 @@ object test {

val foo: C[Tree^] = ??? // error
type T = C[Tree^] // error
val bar: T -> T = ???
//val bar: T -> T = ??? // --> boundschecks3.scala for what happens if we uncomment
val baz: C[Tree^] -> Unit = ??? // error
}
4 changes: 4 additions & 0 deletions tests/neg-custom-args/captures/boundschecks3.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 -----------------------------------------------------
11 | val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
| ^^^^^^
| test.C[box test.Tree^] captures the root capability `cap` in invariant position
13 changes: 13 additions & 0 deletions tests/neg-custom-args/captures/boundschecks3.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
object test {

class Tree

def f[X <: Tree](x: X): Unit = ()

class C[X <: Tree](x: X)

val foo: C[Tree^] = ??? // hidden error
type T = C[Tree^] // hidden error
val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
val baz: C[Tree^] -> Unit = ??? // hidden error
}
14 changes: 14 additions & 0 deletions tests/neg-custom-args/captures/box-adapt-cases.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:14:10 ------------------------------
14 | x.value(cap => cap.use()) // error
| ^^^^^^^^^^^^^^^^
| Found: (cap: box Cap^?) ->{io} Int
| Required: (cap: box Cap^{io}) -> Int
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:28:10 ------------------------------
28 | x.value(cap => cap.use()) // error
| ^^^^^^^^^^^^^^^^
| Found: (cap: box Cap^?) ->{io, fs} Int
| Required: (cap: box Cap^{io, fs}) ->{io} Int
|
| longer explanation available when compiling with `-explain`
16 changes: 8 additions & 8 deletions tests/neg-custom-args/captures/box-adapt-cases.scala
Original file line number Diff line number Diff line change
@@ -1,29 +1,29 @@
trait Cap { def use(): Int }

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

val x: Id[Cap^] = ???
x(cap => cap.use())
x.value(cap => cap.use())
}

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

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

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

val x: Id[Cap^{io}] = ???
x(cap => cap.use()) // ok
x.value(cap => cap.use()) // ok
}

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

val x: Id[Cap^{io, fs}] = ???
x(cap => cap.use()) // error
x.value(cap => cap.use()) // error
}
10 changes: 5 additions & 5 deletions tests/neg-custom-args/captures/box-adapt-cov.scala
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
trait Cap

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

def test2(io: Cap^) = {
type Op[X] = [T] -> Unit -> X^{io}
class Op[+X](val value: [T] -> Unit -> X^{io})
val f: Op[Cap^{io}] = ???
val x: Unit -> Cap^{io} = f[Unit] // error
val x1: Unit ->{io} Cap^{io} = f[Unit] // ok
val x: Unit -> Cap^{io} = f.value[Unit] // error
val x1: Unit ->{io} Cap^{io} = f.value[Unit] // ok
}
12 changes: 6 additions & 6 deletions tests/neg-custom-args/captures/box-adapt-depfun.scala
Original file line number Diff line number Diff line change
@@ -1,23 +1,23 @@
trait Cap { def use(): Int }

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

val x: Id[Cap]^{io} = ???
x(cap => cap.use()) // ok
x.value(cap => cap.use()) // ok
}

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

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

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

val x: Id[Cap^{io}] = ???
x(cap => cap.use()) // error
x.value(cap => cap.use()) // error
}
8 changes: 4 additions & 4 deletions tests/neg-custom-args/captures/box-adapt-typefun.scala
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
trait Cap { def use(): Int }

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

def test2(io: Cap^): Unit = {
type Lazy[X] = [T] -> Unit -> X
class Lazy[X](val value: [T] -> Unit -> X)
val f: Lazy[Cap^{io}] = ???
val test: [T] -> Unit -> (Cap^{io}) = f // error
val test: [T] -> Unit -> (Cap^{io}) = f.value // error
}
12 changes: 6 additions & 6 deletions tests/neg-custom-args/captures/capt1.check
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,15 @@
-- Error: tests/neg-custom-args/captures/capt1.scala:34:16 -------------------------------------------------------------
34 | val z2 = h[() -> Cap](() => x) // error // error
| ^^^^^^^^^
| Type variable X of method h cannot be instantiated to () -> box C^ since
| the part box C^ of that type captures the root capability `cap`.
| Type variable X of method h cannot be instantiated to () -> (ex$15: caps.Exists) -> C^{ex$15} since
| the part C^{ex$15} of that type captures the root capability `cap`.
-- Error: tests/neg-custom-args/captures/capt1.scala:34:30 -------------------------------------------------------------
34 | val z2 = h[() -> Cap](() => x) // error // error
| ^
| reference (x : C^) is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> box C^
| reference (x : C^) is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> (ex$15: caps.Exists) -> C^{ex$15}
-- Error: tests/neg-custom-args/captures/capt1.scala:36:13 -------------------------------------------------------------
36 | val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // error
| ^^^^^^^^^^^^^^^^^^^^^^^
| Type variable X of method h cannot be instantiated to box () ->{x} Cap since
| the part Cap of that type captures the root capability `cap`.
| Type variable X of method h cannot be instantiated to box () ->{x} (ex$20: caps.Exists) -> C^{ex$20} since
| the part C^{ex$20} of that type captures the root capability `cap`.
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/cc-ex-conformance.scala
Original file line number Diff line number Diff line change
Expand Up @@ -21,5 +21,5 @@ def Test =
val ex3: EX3 = ???
val ex4: EX4 = ???
val _: EX4 = ex3 // ok
val _: EX4 = ex4
val _: EX4 = ex4 // error (???) Probably since we also introduce existentials on expansion
val _: EX3 = ex4 // error
Loading
Loading