Skip to content

Commit

Permalink
Add constraint to capsOf
Browse files Browse the repository at this point in the history
  • Loading branch information
noti0na1 committed Dec 1, 2024
1 parent 8a15af3 commit 092b358
Show file tree
Hide file tree
Showing 7 changed files with 53 additions and 22 deletions.
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,9 @@ sealed abstract class CaptureSet extends Showable:
def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
def test(using Context) = reporting.trace(debugInfo):
elems.exists(_.subsumes(x))
|| !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
|| !x.isMaxCapability
&& !x.derivesFrom(defn.Caps_CapSet)
&& x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
comparer match
case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
case _ => test
Expand Down
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
* The info of these symbols is made fluid.
*/
def isPreCC(sym: Symbol)(using Context): Boolean =
// TODO: check type members as well
sym.isTerm && sym.maybeOwner.isClass
&& !sym.is(Module)
&& !sym.owner.is(CaptureChecked)
Expand Down Expand Up @@ -866,7 +867,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
if others.accountsFor(ref) then
report.warning(em"redundant capture: $dom already accounts for $ref", pos)

if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then
if ref.captureSetOfInfo.elems.isEmpty
&& !ref.derivesFrom(defn.Caps_Capability)
&& !ref.derivesFrom(defn.Caps_CapSet) then
val deepStr = if ref.isReach then " deep" else ""
report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos)
check(parent.captureSet, parent)
Expand Down
2 changes: 1 addition & 1 deletion library/src/scala/caps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
* @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
*/
@compileTimeOnly("Should be be used only internally by the Scala compiler")
def capsOf[CS]: Any = ???
def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ???

/** Reach capabilities x* which appear as terms in @retains annotations are encoded
* as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/capset-members.scala
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,6 @@ class Concrete3 extends Abstract[CapSet^{}]:
type C = CapSet^{} | CapSet^{}
def boom() = ()

class Concrete4 extends Abstract[CapSet^{}]:
type C = Nothing // error
class Concrete4 extends Abstract[CapSet^]:
type C = CapSet // error
def boom() = ()
17 changes: 8 additions & 9 deletions tests/neg-custom-args/captures/i21868.scala
Original file line number Diff line number Diff line change
@@ -1,14 +1,13 @@
import caps.*

trait AbstractWrong:
type C <: CapSet
def boom(): Unit^{C^} // error
type C <: CapSet
def f(): Unit^{C^} // error

trait Abstract:
type C <: CapSet^
def boom(): Unit^{C^}

class Concrete extends Abstract:
type C = Nothing
def boom() = () // error
trait Abstract1:
type C^
def f(): Unit^{C^}

class Abstract2:
type C >: CapSet <: CapSet^
def f(): Unit^{C^}
33 changes: 33 additions & 0 deletions tests/neg-custom-args/captures/i21868b.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
import caps.*

class IO

class File

trait Abstract:
type C >: CapSet <: CapSet^
def f(file: File^{C^}): Unit

class Concrete1 extends Abstract:
type C = CapSet
def f(file: File) = ()

class Concrete2(io: IO^) extends Abstract:
type C = CapSet^{io}
def f(file: File^{io}) = ()

class Concrete3(io: IO^) extends Abstract:
type C = CapSet^{io}
def f(file: File) = () // error

trait Abstract2(io: IO^):
type C >: CapSet <: CapSet^{io}
def f(file: File^{C^}): Unit

class Concrete4(io: IO^) extends Abstract2(io):
type C = CapSet
def f(file: File) = ()

class Concrete5(io1: IO^, io2: IO^) extends Abstract2(io1):
type C = CapSet^{io2} // error
def f(file: File^{io2}) = ()
10 changes: 2 additions & 8 deletions tests/pos-custom-args/captures/cc-poly-varargs.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,7 @@ def either[T1, T2, Cap^](
val left = src1.transformValuesWith(Left(_))
val right = src2.transformValuesWith(Right(_))
race[Either[T1, T2], Cap](left, right)
// An explcit type argument is required here because the second argument is
// inferred as `CapSet^{Cap^}` instead of `Cap`.
// Explcit type arguments are required here because the second argument
// is inferred as `CapSet^{Cap^}` instead of `Cap`.
// Although `CapSet^{Cap^}` subsums `Cap` in terms of capture set,
// `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.






0 comments on commit 092b358

Please sign in to comment.