Skip to content

Commit

Permalink
Make capture sets of expressions deriving Capability explicit
Browse files Browse the repository at this point in the history
When an expression has a type that derives from caps.Capability, add an
explicit capture set.

Also: Address other review comments
  • Loading branch information
odersky committed May 27, 2024
1 parent 999be5e commit 81cf8d8
Show file tree
Hide file tree
Showing 21 changed files with 92 additions and 50 deletions.
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -203,8 +203,8 @@ extension (tp: Type)
case _ =>
false

/** Does type derive from caps.Capability?, which means it references of this
* type are maximal capabilities?
/** Tests whether the type derives from `caps.Capability`, which means
* references of this type are maximal capabilities.
*/
def derivesFromCapability(using Context): Boolean = tp.dealias match
case tp: (TypeRef | AppliedType) =>
Expand Down
6 changes: 5 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,11 @@ sealed abstract class CaptureSet extends Showable:
(x eq y)
|| x.isRootCapability
|| y.match
case y: TermRef => y.prefix eq x
case y: TermRef =>
(y.prefix eq x)
|| y.info.match
case y1: CaptureRef => x.subsumes(y1)
case _ => false
case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
case _ => false
|| x.match
Expand Down
29 changes: 23 additions & 6 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1037,7 +1037,7 @@ class CheckCaptures extends Recheck, SymTransformer:
val arrow = if covariant then "~~>" else "<~~"
i"adapting $actual $arrow $expected"

def adapt(actual: Type, expected: Type, covariant: Boolean): Type = trace(adaptInfo(actual, expected, covariant), recheckr, show = true) {
def adapt(actual: Type, expected: Type, covariant: Boolean): Type = trace(adaptInfo(actual, expected, covariant), recheckr, show = true):
if expected.isInstanceOf[WildcardType] then actual
else
// Decompose the actual type into the inner shape type, the capture set and the box status
Expand Down Expand Up @@ -1117,7 +1117,22 @@ class CheckCaptures extends Recheck, SymTransformer:
adaptedType(!boxed)
else
adaptedType(boxed)
}
end adapt

/** If result derives from caps.Capability, yet is not a capturing type itself,
* make its capture set explicit.
*/
def makeCaptureSetExplicit(result: Type) = result match
case CapturingType(_, _) => result
case _ =>
if result.derivesFromCapability then
val cap: CaptureRef = actual match
case ref: CaptureRef if ref.isTracked =>
ref
case _ =>
defn.captureRoot.termRef // TODO: skolemize?
CapturingType(result, cap.singletonCaptureSet)
else result

if expected == LhsProto || expected.isSingleton && actual.isSingleton then
actual
Expand All @@ -1133,10 +1148,12 @@ class CheckCaptures extends Recheck, SymTransformer:
case _ =>
case _ =>
val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
if adapted ne actualw then
capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
adapted
else actual
makeCaptureSetExplicit:
if adapted ne actualw then
capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
adapted
else
actual
end adaptBoxed

/** Check overrides again, taking capture sets into account.
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 @@ -4,7 +4,7 @@ import annotation.experimental

@experimental object caps:

trait Capability // should be @erased
trait Capability extends Any

/** The universal capture reference */
val cap: Capability = new Capability() {}
Expand Down
22 changes: 11 additions & 11 deletions tests/neg-custom-args/captures/effect-swaps-explicit.check
Original file line number Diff line number Diff line change
@@ -1,29 +1,29 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:64:8 -------------------------
63 | Result:
64 | Future: // error, type mismatch
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:62:8 -------------------------
61 | Result:
62 | Future: // error, type mismatch
| ^
| Found: Result.Ok[box Future[box T^?]^{fr, contextual$1}]
| Required: Result[Future[T], Nothing]
65 | fr.await.ok
63 | fr.await.ok
|--------------------------------------------------------------------------------------------------------------------
|Inline stack trace
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|This location contains code that was inlined from effect-swaps-explicit.scala:41
41 | boundary(Ok(body))
|This location contains code that was inlined from effect-swaps-explicit.scala:39
39 | boundary(Ok(body))
| ^^^^^^^^
--------------------------------------------------------------------------------------------------------------------
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:74:10 ------------------------
74 | Future: fut ?=> // error: type mismatch
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:72:10 ------------------------
72 | Future: fut ?=> // error: type mismatch
| ^
| Found: Future[box T^?]^{fr, lbl}
| Required: Future[box T^?]^?
75 | fr.await.ok
73 | fr.await.ok
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:68:15 ---------------------------------------------
68 | Result.make: //lbl ?=> // error, escaping label from Result
-- Error: tests/neg-custom-args/captures/effect-swaps-explicit.scala:66:15 ---------------------------------------------
66 | Result.make: //lbl ?=> // error, escaping label from Result
| ^^^^^^^^^^^
|local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]^):
| box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result
2 changes: 0 additions & 2 deletions tests/neg-custom-args/captures/effect-swaps-explicit.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
import annotation.capability

object boundary:

final class Label[-T] // extends caps.Capability
Expand Down
18 changes: 9 additions & 9 deletions tests/neg-custom-args/captures/effect-swaps.check
Original file line number Diff line number Diff line change
@@ -1,24 +1,24 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:64:8 ----------------------------------
63 | Result:
64 | Future: // error, type mismatch
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:62:8 ----------------------------------
61 | Result:
62 | Future: // error, type mismatch
| ^
| Found: Result.Ok[box Future[box T^?]^{fr, contextual$1}]
| Required: Result[Future[T], Nothing]
65 | fr.await.ok
63 | fr.await.ok
|--------------------------------------------------------------------------------------------------------------------
|Inline stack trace
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|This location contains code that was inlined from effect-swaps.scala:41
41 | boundary(Ok(body))
|This location contains code that was inlined from effect-swaps.scala:39
39 | boundary(Ok(body))
| ^^^^^^^^
--------------------------------------------------------------------------------------------------------------------
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:74:10 ---------------------------------
74 | Future: fut ?=> // error: type mismatch
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:72:10 ---------------------------------
72 | Future: fut ?=> // error: type mismatch
| ^
| Found: Future[box T^?]^{fr, lbl}
| Required: Future[box T^?]^?
75 | fr.await.ok
73 | fr.await.ok
|
| longer explanation available when compiling with `-explain`
2 changes: 0 additions & 2 deletions tests/neg-custom-args/captures/effect-swaps.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
import annotation.capability

object boundary:

final class Label[-T] extends caps.Capability
Expand Down
21 changes: 21 additions & 0 deletions tests/neg-custom-args/captures/extending-cap-classes.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 -------------------------
7 | val x2: C1 = new C2 // error
| ^^^^^^
| Found: C2^
| Required: C1
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 -------------------------
8 | val x3: C1 = new C3 // error
| ^^^^^^
| Found: C3^
| Required: C1
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------
13 | val z2: C1 = y2 // error
| ^^
| Found: (y2 : C2)^{y2}
| Required: C1
|
| longer explanation available when compiling with `-explain`
14 changes: 14 additions & 0 deletions tests/neg-custom-args/captures/extending-cap-classes.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
class C1
class C2 extends C1, caps.Capability
class C3 extends C2

def test =
val x1: C1 = new C1
val x2: C1 = new C2 // error
val x3: C1 = new C3 // error

val y2: C2 = new C2
val y3: C3 = new C3

val z2: C1 = y2 // error

12 changes: 6 additions & 6 deletions tests/neg-custom-args/captures/usingLogFile.check
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:14 ------------------------------------------------------
23 | val later = usingLogFile { f => () => f.write(0) } // error
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:22:14 ------------------------------------------------------
22 | val later = usingLogFile { f => () => f.write(0) } // error
| ^^^^^^^^^^^^
| local reference f leaks into outer capture set of type parameter T of method usingLogFile in object Test2
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:28:23 ------------------------------------------------------
28 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:27:23 ------------------------------------------------------
27 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
| ^^^^^^^^^^^^
| local reference f leaks into outer capture set of type parameter T of method usingLogFile in object Test2
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:44:16 ------------------------------------------------------
44 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:43:16 ------------------------------------------------------
43 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
| ^^^^^^^^^
| local reference f leaks into outer capture set of type parameter T of method usingFile in object Test3
1 change: 0 additions & 1 deletion tests/neg-custom-args/captures/usingLogFile.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import java.io.*
import annotation.capability

object Test1:

Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/capt-capability.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import annotation.capability
import caps.Capability

def f1(c: Capability): () ->{c} c.type = () => c // ok
Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/filevar-tracked.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
import language.experimental.captureChecking
import language.experimental.modularity
import annotation.capability
import compiletime.uninitialized

object test1:
Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/i19751.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import language.experimental.captureChecking
import annotation.capability
import caps.cap

trait Ptr[A]
Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/logger-tracked.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import annotation.capability
import language.experimental.saferExceptions
import language.experimental.modularity

Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/logger.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import annotation.capability
import language.experimental.saferExceptions
import language.experimental.modularity

Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/null-logger.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import annotation.capability
import annotation.constructorOnly

class FileSystem extends caps.Capability
Expand Down
1 change: 0 additions & 1 deletion tests/pos-custom-args/captures/try3.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import language.experimental.erasedDefinitions
import annotation.capability
import java.io.IOException

class CanThrow[-E] extends caps.Capability
Expand Down
1 change: 0 additions & 1 deletion tests/pos-with-compiler-cc/dotc/core/Definitions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -985,7 +985,6 @@ class Definitions {
@tu lazy val BeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BeanProperty")
@tu lazy val BooleanBeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BooleanBeanProperty")
@tu lazy val BodyAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Body")
@tu lazy val CapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.capability")
@tu lazy val ChildAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Child")
@tu lazy val ContextResultCountAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ContextResultCount")
@tu lazy val ProvisionalSuperClassAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ProvisionalSuperClass")
Expand Down
1 change: 0 additions & 1 deletion tests/pos/i20237.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import language.experimental.captureChecking
import scala.annotation.capability

class Cap extends caps.Capability:
def use[T](body: Cap ?=> T) = body(using this)
Expand Down

0 comments on commit 81cf8d8

Please sign in to comment.