Skip to content

Commit 606268f

Browse files
LinyxusLinyxus
authored
Adjustments to the capability trilogy (#23428)
Fixes #23421. This PR includes the following two changes: 1. In `capToFresh`, turn `cap`s in invariant occurrences also to `Fresh`es. Previously, in the follow code: ``` val xs: ArrayBuffer[() ->{cap} Unit] = ... ``` The `cap` is kept intact since it is invariant. Now, it gets converted into a `Fresh` owned by `xs`. 2. In `toResultInResults`, convert fresh caps of `def`-method with only type parameters into result caps, just like parameterless defs. Specifically, for the following code: ``` def empty[T]: ArrayBuffer[T]^ = ... ``` The `^` will be turned into a result cap, just like what happens for a parameterless def: ``` def mkRef: Ref^ = ... ``` The `^` is a result cap that gets instantiated to a new fresh at each application of `mkRef`. Doing the same thing for `empty` is the arguably more desirable behavior.
2 parents d995b33 + 57b09a3 commit 606268f

File tree

14 files changed

+121
-30
lines changed

14 files changed

+121
-30
lines changed

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

Lines changed: 19 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ import annotation.constructorOnly
2121
import ast.tpd
2222
import printing.{Printer, Showable}
2323
import printing.Texts.Text
24-
import reporting.Message
24+
import reporting.{Message, trace}
2525
import NameOps.isImpureFunction
2626
import annotation.internal.sharable
2727

@@ -693,7 +693,7 @@ object Capabilities:
693693
thisMap =>
694694

695695
override def apply(t: Type) =
696-
if variance <= 0 then t
696+
if variance < 0 then t
697697
else t match
698698
case t @ CapturingType(_, _) =>
699699
mapOver(t)
@@ -703,6 +703,8 @@ object Capabilities:
703703
this(CapturingType(parent1, ann.tree.toCaptureSet))
704704
else
705705
t.derivedAnnotatedType(parent1, ann)
706+
case defn.RefinedFunctionOf(_) =>
707+
t // stop at dependent function types
706708
case _ =>
707709
mapFollowingAliases(t)
708710

@@ -784,7 +786,7 @@ object Capabilities:
784786
abstract class CapMap extends BiTypeMap:
785787
override def mapOver(t: Type): Type = t match
786788
case t @ FunctionOrMethod(args, res) if variance > 0 && !t.isAliasFun =>
787-
t // `t` should be mapped in this case by a different call to `mapCap`.
789+
t // `t` should be mapped in this case by a different call to `toResult`. See [[toResultInResults]].
788790
case t: (LazyRef | TypeVar) =>
789791
mapConserveSuper(t)
790792
case _ =>
@@ -849,7 +851,8 @@ object Capabilities:
849851
end toResult
850852

851853
/** Map global roots in function results to result roots. Also,
852-
* map roots in the types of parameterless def methods.
854+
* map roots in the types of def methods that are parameterless
855+
* or have only type parameters.
853856
*/
854857
def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(tp: Type)(using Context): Type =
855858
val m = new TypeMap with FollowAliasesMap:
@@ -878,8 +881,19 @@ object Capabilities:
878881
throw ex
879882
m(tp) match
880883
case tp1: ExprType if sym.is(Method, butNot = Accessor) =>
884+
// Map the result of parameterless `def` methods.
881885
tp1.derivedExprType(toResult(tp1.resType, tp1, fail))
886+
case tp1: PolyType if !tp1.resType.isInstanceOf[MethodicType] =>
887+
// Map also the result type of method with only type parameters.
888+
// This way, the `^` in the following method will be mapped to a `ResultCap`:
889+
// ```
890+
// object Buffer:
891+
// def empty[T]: Buffer[T]^
892+
// ```
893+
// This is more desirable than interpreting `^` as a `Fresh` at the level of `Buffer.empty`
894+
// in most cases.
895+
tp1.derivedLambdaType(resType = toResult(tp1.resType, tp1, fail))
882896
case tp1 => tp1
883897
end toResultInResults
884898

885-
end Capabilities
899+
end Capabilities

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ import printing.{Showable, Printer}
1414
import printing.Texts.*
1515
import util.{SimpleIdentitySet, Property}
1616
import typer.ErrorReporting.Addenda
17-
import util.common.alwaysTrue
1817
import scala.collection.{mutable, immutable}
1918
import TypeComparer.ErrorNote
2019
import CCState.*

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ import reporting.Message
1818
import printing.{Printer, Texts}, Texts.{Text, Str}
1919
import collection.mutable
2020
import CCState.*
21-
import dotty.tools.dotc.util.NoSourcePosition
2221
import CheckCaptures.CheckerAPI
2322
import NamerOps.methodType
2423
import NameKinds.{CanThrowEvidenceName, TryOwnerName}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@
33
| ^
44
| Type argument test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[test.Tree^]
55
|
6-
| where: ^ refers to the universal root capability
6+
| where: ^ refers to a fresh root capability in the type of value foo
77
|
88
| longer explanation available when compiling with `-explain`
99
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:10:11 --------------------------------
1010
10 | type T = C[Tree^] // error
1111
| ^
1212
| Type argument test.Tree^ does not conform to upper bound test.Tree in inferred type test.C[test.Tree^]
1313
|
14-
| where: ^ refers to the universal root capability
14+
| where: ^ refers to a fresh root capability in the type of type T
1515
|
1616
| longer explanation available when compiling with `-explain`
1717
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/boundschecks3.scala:11:11 --------------------------------

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

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,3 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:8:10 -------------------------------
2-
8 | x.value(cap => cap.use()) // error, was OK
3-
| ^^^^^^^^^^^^^^^^
4-
| Found: (cap: Cap^?) => Int
5-
| Required: Cap^ =>² Int
6-
|
7-
| where: => refers to the universal root capability
8-
| =>² refers to a fresh root capability created in method test1
9-
| ^ refers to the universal root capability
10-
|
11-
| longer explanation available when compiling with `-explain`
121
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:15:10 ------------------------------
132
15 | x.value(cap => cap.use()) // error
143
| ^^^^^^^^^^^^^^^^

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ def test1(): Unit = {
55
class Id[X](val value: [T] -> (op: X => T) -> T)
66

77
val x: Id[Cap^] = ???
8-
x.value(cap => cap.use()) // error, was OK
8+
x.value(cap => cap.use())
99
}
1010

1111
def test2(io: Cap^): Unit = {

‎tests/neg-custom-args/captures/cc-fresh-levels.check‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
Flag -source set repeatedly
2+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-fresh-levels.scala:14:10 ------------------------------
3+
14 | r.put(x) // error
4+
| ^
5+
| Found: IO^{x}
6+
| Required: IO^
7+
|
8+
| where: ^ refers to a fresh root capability in the type of value r
9+
|
10+
| longer explanation available when compiling with `-explain`
11+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-fresh-levels.scala:17:10 ------------------------------
12+
17 | r.put(innerIO) // error
13+
| ^^^^^^^
14+
| Found: IO^{innerIO}
15+
| Required: IO^
16+
|
17+
| where: ^ refers to a fresh root capability in the type of value r
18+
|
19+
| longer explanation available when compiling with `-explain`
20+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-fresh-levels.scala:18:9 -------------------------------
21+
18 | runIO: innerIO => // error
22+
| ^
23+
|Found: (innerIO: IO^?) ->? Unit
24+
|Required: IO^ => Unit
25+
|
26+
|where: => refers to a fresh root capability created in method test1 when checking argument to parameter op of method runIO
27+
| ^ refers to the universal root capability
28+
19 | r.put(innerIO)
29+
|
30+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/cc-fresh-levels.scala‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
//> using options -source 3.7
2+
import language.experimental.captureChecking
3+
import caps.*
4+
class IO
5+
class Ref[X](init: X):
6+
private var _data = init
7+
def get: X = _data
8+
def put(y: X): Unit = _data = y
9+
def runIO(op: IO^ => Unit): Unit = ()
10+
def test1(a: IO^, b: IO^, c: IO^): Unit =
11+
val r: Ref[IO^] = Ref(a)
12+
r.put(b) // ok
13+
def outer(x: IO^): Unit =
14+
r.put(x) // error
15+
r.put(c) // ok
16+
runIO: (innerIO: IO^) =>
17+
r.put(innerIO) // error
18+
runIO: innerIO => // error
19+
r.put(innerIO)

‎tests/neg-custom-args/captures/class-level-attack.check‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
-- Error: tests/neg-custom-args/captures/class-level-attack.scala:12:24 ------------------------------------------------
2+
12 | val r: Ref[IO^] = Ref[IO^](io) // error:
3+
| ^^^
4+
| Type variable X of constructor Ref cannot be instantiated to IO^ since
5+
| that type captures the root capability `cap`.
6+
|
7+
| where: ^ refers to the universal root capability
8+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:26 ---------------------------
9+
17 | def set(x: IO^) = r.put(x) // error
10+
| ^
11+
| Found: IO^{x}
12+
| Required: IO^
13+
|
14+
| where: ^ refers to a fresh root capability in the type of value r
15+
|
16+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/class-level-attack.scala‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,8 @@ class C(io: IO^):
1313
//Type variable X of constructor Ref cannot be instantiated to box IO^ since
1414
//that type captures the root capability `cap`.
1515
// where: ^ refers to the universal root capability
16-
val r2: Ref[IO^] = Ref(io) // error:
17-
//Error: Ref[IO^{io}] does not conform to Ref[IO^] (since Refs are invariant)
18-
def set(x: IO^) = r.put(x)
16+
val r2: Ref[IO^] = Ref(io)
17+
def set(x: IO^) = r.put(x) // error
1918

2019
def outer(outerio: IO^) =
2120
val c = C(outerio)

0 commit comments

Comments
 (0)