Skip to content

Commit 58baf53

Browse files
oderskyodersky
committed
Let existential variables only subsume shared capabilities
Also, implement infrastructure to add a note to a type mismatch when a failure to subsume occurs.
1 parent 641dffa commit 58baf53

11 files changed

+129
-13
lines changed

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,12 @@ class CCState:
8484
*/
8585
var levelError: Option[CaptureSet.CompareResult.LevelError] = None
8686

87+
/** Optionally, a pair of an existential variable and another capability.
88+
* Set when a subsumes check decides that an existential variable cannot be
89+
* instantiated to the other capability.
90+
*/
91+
var existentialSubsumesFailure: Option[(CaptureRef, CaptureRef)] = None
92+
8793
/** Warnings relating to upper approximations of capture sets with
8894
* existentially bound variables.
8995
*/

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -263,10 +263,11 @@ trait CaptureRef extends TypeProxy, ValueType:
263263
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
264264
|| !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
265265
case Existential.Vble(binder) =>
266-
y.stripReadOnly match
267-
case Existential.Vble(binder1) => false
268-
case Fresh(_) => false
269-
case _ => true
266+
if y.derivesFromSharedCapability then true
267+
else
268+
ccState.existentialSubsumesFailure =
269+
ccState.existentialSubsumesFailure.orElse(Some(this, y))
270+
false
270271
case _ =>
271272
this.isCap && !yIsExistential && canAddHidden && vs != VarState.HardSeparate
272273
|| y.match

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

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1218,6 +1218,19 @@ class CheckCaptures extends Recheck, SymTransformer:
12181218
|
12191219
|Note that ${msg.toString}"""
12201220

1221+
private def existentialSubsumesFailureAddenda(using Context): Addenda =
1222+
ccState.existentialSubsumesFailure match
1223+
case Some((ex @ Existential.Vble(binder), other)) =>
1224+
new Addenda:
1225+
override def toAdd(using Context): List[String] =
1226+
val ann = ex.annot.asInstanceOf[Fresh.Annot]
1227+
i"""
1228+
|
1229+
|Note that the existential capture root in ${ann.originalBinder.resType}
1230+
|cannot subsume the capability $other"""
1231+
:: Nil
1232+
case _ => NothingToAdd
1233+
12211234
/** Addendas for error messages that show where we have under-approximated by
12221235
* mapping a a capture ref in contravariant position to the empty set because
12231236
* the original result type of the map was not itself a capture ref.
@@ -1257,6 +1270,7 @@ class CheckCaptures extends Recheck, SymTransformer:
12571270
if actualBoxed eq actual then
12581271
// Only `addOuterRefs` when there is no box adaptation
12591272
expected1 = addOuterRefs(expected1, actual, tree.srcPos)
1273+
ccState.existentialSubsumesFailure = None
12601274
if isCompatible(actualBoxed, expected1) then
12611275
if debugSuccesses then tree match
12621276
case Ident(_) =>
@@ -1268,7 +1282,10 @@ class CheckCaptures extends Recheck, SymTransformer:
12681282
inContext(Fresh.printContext(actualBoxed, expected1)):
12691283
err.typeMismatch(tree.withType(actualBoxed), expected1,
12701284
addApproxAddenda(
1271-
addenda ++ CaptureSet.levelErrors ++ boxErrorAddenda(boxErrors),
1285+
addenda
1286+
++ CaptureSet.levelErrors
1287+
++ boxErrorAddenda(boxErrors)
1288+
++ existentialSubsumesFailureAddenda,
12721289
expected1))
12731290
actual
12741291
end checkConformsExpr

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

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,15 @@ object Fresh:
3131
override def tree(using Context) = New(symbol.typeRef, Nil)
3232
override def derivedAnnotation(tree: Tree)(using Context): Annotation = this
3333

34+
private var myOriginalBinder = binder
35+
def originalBinder: MethodType = myOriginalBinder.asInstanceOf[MethodType]
36+
3437
def derivedAnnotation(binder: MethodType | NoType.type)(using Context): Annotation =
35-
if this.binder eq binder then this else Annot(hidden, binder)
38+
if this.binder eq binder then this
39+
else
40+
val ann = Annot(hidden, binder)
41+
ann.myOriginalBinder = myOriginalBinder
42+
ann
3643

3744
override def hash: Int = hidden.hashCode
3845
override def eql(that: Annotation) = that match
@@ -70,6 +77,7 @@ object Fresh:
7077
val hiddenSet = CaptureSet.HiddenSet(NoSymbol)
7178
val res = AnnotatedType(defn.captureRoot.termRef, Annot(hiddenSet, binder))
7279
hiddenSet.owningCap = res
80+
//assert(hiddenSet.id != 9, binder.show)
7381
res
7482

7583
/** The initial elements (either 0 or 1) of a hidden set created for given `owner`.

‎tests/neg-custom-args/captures/cc-existential-conformance.check

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,9 @@
1414
| Found: (y : A -> A -> B^)
1515
| Required: A -> (x: A) -> B^
1616
|
17+
| Note that the existential capture root in B^
18+
| cannot subsume the capability cap
19+
|
1720
| longer explanation available when compiling with `-explain`
1821
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
1922
13 | val y: Fun[B^] = x // error
@@ -31,4 +34,7 @@
3134
| Found: (y : A -> B^)
3235
| Required: (x: A) -> B^
3336
|
37+
| Note that the existential capture root in B^
38+
| cannot subsume the capability cap
39+
|
3440
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/erased-methods2.check

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/erased-methods2.scala:21:9 -------------------------------
2+
21 | ?=> (x$2: CT[Ex2]^) // error
3+
| ^
4+
| Found: (erased x$2: CT[Ex2]^) ?->{x$1} Unit
5+
| Required: (erased x$2: CT[Ex2]^) ?->? Unit
6+
|
7+
| Note that the existential capture root in (erased x$2: CT[Ex2]^) ?=> Unit
8+
| cannot subsume the capability x$1.type
9+
22 | ?=>
10+
23 | //given (CT[Ex3]^) = x$1
11+
24 | Throw(new Ex3)
12+
|
13+
| longer explanation available when compiling with `-explain`
14+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/erased-methods2.scala:32:9 -------------------------------
15+
32 | ?=> (erased x$2: CT[Ex2]^) // error
16+
| ^
17+
| Found: (erased x$2: CT[Ex2]^) ?->{x$1} (erased x$2: CT[Ex1]^) ?->{x$1} Unit
18+
| Required: (erased x$1²: CT[Ex2]^) ?->? (erased x$2: CT[Ex1]^) ?->? Unit
19+
|
20+
| where: x$1 is a parameter in an anonymous function in method foo10a
21+
| x$1² is a reference to a value parameter
22+
|
23+
|
24+
| Note that the existential capture root in (erased x$1: CT[Ex2]^) ?=> (erased x$2: CT[Ex1]^) ?->{localcap} Unit
25+
| cannot subsume the capability x$1.type
26+
33 | ?=> (erased x$3: CT[Ex1]^)
27+
34 | ?=> Throw(new Ex3)
28+
|
29+
| longer explanation available when compiling with `-explain`

‎tests/pos-custom-args/captures/erased-methods2.scala renamed to ‎tests/neg-custom-args/captures/erased-methods2.scala

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,19 +16,19 @@ def foo8a(i: Int) =
1616
def foo9a(i: Int)
1717
: (x$1: CT[Ex3]^)
1818
?=> (x$2: CT[Ex2]^)
19-
?-> {x$1, caps.cap} Unit
19+
?=> Unit
2020
= (x$1: CT[Ex3]^)
21-
?=> (x$2: CT[Ex2]^)
21+
?=> (x$2: CT[Ex2]^) // error
2222
?=>
2323
//given (CT[Ex3]^) = x$1
2424
Throw(new Ex3)
2525

2626
def foo10a(i: Int)
2727
: (erased x$0: CT[Ex3]^)
2828
?=> (erased x$1: CT[Ex2]^)
29-
?-> {x$0, caps.cap} (erased x$2: CT[Ex1]^)
30-
?-> {x$0, x$1, caps.cap} Unit
29+
?=> (erased x$2: CT[Ex1]^)
30+
?=> Unit
3131
= (erased x$1: CT[Ex3]^)
32-
?=> (erased x$2: CT[Ex2]^)
32+
?=> (erased x$2: CT[Ex2]^) // error
3333
?=> (erased x$3: CT[Ex1]^)
3434
?=> Throw(new Ex3)

‎tests/neg-custom-args/captures/heal-tparam-cs.check

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 -------------------------------
2+
15 | localCap { c => // error
3+
| ^
4+
| Found: (x$0: Capp^) ->? () ->{x$0} Unit
5+
| Required: (c: Capp^) -> () ->{localcap} Unit
6+
|
7+
| Note that the existential capture root in () => Unit
8+
| cannot subsume the capability x$0.type
9+
16 | (c1: Capp^) => () => { c1.use() }
10+
17 | }
11+
|
12+
| longer explanation available when compiling with `-explain`
13+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:25:13 -------------------------------
14+
25 | localCap { c => // error
15+
| ^
16+
| Found: (x$0: Capp^{io}) ->? () ->{x$0} Unit
17+
| Required: (c: Capp^{io}) -> () ->{net} Unit
18+
26 | (c1: Capp^{io}) => () => { c1.use() }
19+
27 | }
20+
|
21+
| longer explanation available when compiling with `-explain`
22+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:41:10 -------------------------------
23+
41 | io => () => io.use() // error
24+
| ^^^^^^^^^^^^^^
25+
| Found: () ->{io} Unit
26+
| Required: () ->? Unit
27+
|
28+
| longer explanation available when compiling with `-explain`
29+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:10 -------------------------------
30+
44 | io => () => io.use() // error
31+
| ^^^^^^^^^^^^^^
32+
| Found: () ->{io} Unit
33+
| Required: () ->? Unit
34+
|
35+
| longer explanation available when compiling with `-explain`
36+
-- Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:10:14 ----------------------------------------------------
37+
10 | val test1 = localCap { c => // error
38+
| ^^^^^^^^
39+
| local reference c leaks into outer capture set of type parameter T of method localCap

‎tests/neg-custom-args/captures/heal-tparam-cs.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ def main(io: Capp^, net: Capp^): Unit = {
1212
}
1313

1414
val test2: (c: Capp^) -> () => Unit =
15-
localCap { c => // ok
15+
localCap { c => // error
1616
(c1: Capp^) => () => { c1.use() }
1717
}
1818

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,16 @@
5151
| Required: File^{id*}
5252
|
5353
| longer explanation available when compiling with `-explain`
54+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:37 --------------------------------------
55+
67 | val id: (x: File^) -> File^ = x => x // error
56+
| ^
57+
| Found: (x : File^)
58+
| Required: File^?
59+
|
60+
| Note that the existential capture root in File^
61+
| cannot subsume the capability x.type
62+
|
63+
| longer explanation available when compiling with `-explain`
5464
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:71:27 --------------------------------------
5565
71 | val f1: File^{id*} = id(f) // error // error
5666
| ^^^^^

‎tests/neg-custom-args/captures/reaches.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ def attack2 =
6464
f1
6565

6666
def attack3 =
67-
val id: (x: File^) -> File^ = x => x
67+
val id: (x: File^) -> File^ = x => x // error
6868
// val id: File^ -> EX C.File^C
6969

7070
val leaked = usingFile[File^{id*}]: f => // error

0 commit comments

Comments
 (0)