Skip to content

Commit

Permalink
Correct rules for CapSet; update definition for Contains; fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
noti0na1 committed Nov 24, 2024
1 parent 82c7e0a commit a8c624e
Show file tree
Hide file tree
Showing 9 changed files with 42 additions and 27 deletions.
23 changes: 19 additions & 4 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,8 @@ trait CaptureRef extends TypeProxy, ValueType:
* x: x1.type /\ x1 subsumes y ==> x subsumes y
* TODO: Document path cases
*/
final def subsumes(y: CaptureRef)(using Context): Boolean =
// import reporting.trace
final def subsumes(y: CaptureRef)(using Context): Boolean = // trace.force(i"subsumes $this, $y"):

def subsumingRefs(x: Type, y: Type): Boolean = x match
case x: CaptureRef => y match
Expand Down Expand Up @@ -135,14 +136,28 @@ trait CaptureRef extends TypeProxy, ValueType:
case _ => false
|| viaInfo(y.info)(subsumingRefs(this, _))
case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
case y: TypeRef if y.symbol.info.derivesFrom(defn.Caps_CapSet) =>
y.info match
case _: TypeAlias => y.captureSetOfInfo.elems.forall(this.subsumes)
case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
case _ => false
|| this.match
case ReachCapability(x1) => x1.subsumes(y.stripReach)
case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
case x: TermParamRef => subsumesExistentially(x, y)
case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
x.captureSetOfInfo.elems.exists(_.subsumes(y))
case x: TypeRef => assumedContainsOf(x).contains(y)
case x: TypeRef if assumedContainsOf(x).contains(y) => true
case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
x.info match
case _: TypeAlias =>
x.captureSetOfInfo.elems.exists(_.subsumes(y))
case TypeBounds(lo: CaptureRef, _) =>
lo.subsumes(y)
case _ =>
x.captureSetOfInfo.elems.exists(_.subsumes(y))
case AnnotatedType(parent, ann)
if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
ann.tree.toCaptureSet.elems.exists(_.subsumes(y))
case _ => false
end subsumes

Expand Down
4 changes: 2 additions & 2 deletions library/src/scala/caps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,12 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
/** A type constraint expressing that the capture set `C` needs to contain
* the capability `R`
*/
sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]

/** The only implementation of `Contains`. The constraint that `{R} <: C` is
* added separately by the capture checker.
*/
given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()

/** A wrapper indicating a type variable in a capture argument list of a
* @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/capture-poly.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ import caps.*
trait Foo extends Capability

trait CaptureSet:
type C <: CapSet^
type C^

def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a
Expand Down
8 changes: 8 additions & 0 deletions tests/neg-custom-args/captures/i22005.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
import caps.*

class IO
class File(io: IO^)

class Handler[C^]:
def f(file: File^): File^{C^} = file // error
def g(file: File^{C^}): File^ = file // ok
16 changes: 8 additions & 8 deletions tests/neg-custom-args/captures/use-capset.check
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
-- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 ---------------------------------------------------------
7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
-- Error: tests/neg-custom-args/captures/use-capset.scala:5:50 ---------------------------------------------------------
5 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
| ^^^^^^^
| Capture set parameter C leaks into capture scope of method g.
| To allow this, the type C should be declared with a @use annotation
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 -----------------------------------
13 | val _: () -> Unit = h // error: should be ->{io}
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:11:22 -----------------------------------
11 | val _: () -> Unit = h // error: should be ->{io}
| ^
| Found: (h : () ->{io} Unit)
| Required: () -> Unit
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 -----------------------------------
15 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 -----------------------------------
13 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io}
| ^^
| Found: (h2 : () ->? (x$0: List[box Object^]^{}) ->{io} Object^{io})
| Required: () -> List[box Object^{io}] -> Object^{io}
| Found: (h2 : () ->? (x$0: List[box Object^{io}]^{}) ->{io} Object^{io})
| Required: () -> List[box Object^{io}] -> Object^{io}
|
| longer explanation available when compiling with `-explain`
2 changes: 0 additions & 2 deletions tests/neg-custom-args/captures/use-capset.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
import caps.{use, CapSet}



def f[C^](@use xs: List[Object^{C^}]): Unit = ???

private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error
Expand Down
7 changes: 0 additions & 7 deletions tests/neg/cc-poly-2.check
Original file line number Diff line number Diff line change
@@ -1,10 +1,3 @@
-- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:13:15 ---------------------------------------------------------
13 | f[Nothing](d) // error
| ^
| Found: (d : Test.D^)
| Required: Test.D
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/cc-poly-2.scala:14:19 ---------------------------------------------------------
14 | f[CapSet^{c1}](d) // error
| ^
Expand Down
2 changes: 1 addition & 1 deletion tests/neg/cc-poly-2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ object Test:

def test(c1: C, c2: C) =
val d: D^ = D()
f[Nothing](d) // error
// f[Nothing](d) // already rule out at typer
f[CapSet^{c1}](d) // error
val x = f(d)
val _: D^{c1} = x // error
5 changes: 3 additions & 2 deletions tests/pos/cc-poly-source-capability.scala
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,14 @@ import caps.use

def test1(async1: Async, @use others: List[Async]) =
val src = Source[CapSet^{async1, others*}]
val _: Set[Listener^{async1, others*}] = src.allListeners
val lst1 = listener(async1)
val lsts = others.map(listener)
val _: List[Listener^{others*}] = lsts
src.register{lst1}
src.register(listener(async1))
lsts.foreach(src.register)
others.map(listener).foreach(src.register)
lsts.foreach(src.register(_)) // TODO: why we need to use _ explicitly here?
others.map(listener).foreach(src.register(_))
val ls = src.allListeners
val _: Set[Listener^{async1, others*}] = ls

Expand Down

0 comments on commit a8c624e

Please sign in to comment.