Skip to content

Commit 90749ea

Browse files
oderskyodersky
committed
Fix special capture set handling in recheckApply, Step 1
Step1: refactor The logic was querying the original types of trees, but we want the rechecked types instead.
1 parent 4333d3e commit 90749ea

File tree

12 files changed

+101
-62
lines changed

12 files changed

+101
-62
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -274,8 +274,8 @@ extension (tp: Type)
274274
case _ =>
275275
tp
276276

277-
/** Is type known to be always pure by its class structure,
278-
* so that adding a capture set to it would not make sense?
277+
/** Is type known to be always pure by its class structure?
278+
* In that case, adding a capture set to it would not make sense.
279279
*/
280280
def isAlwaysPure(using Context): Boolean = tp.dealias match
281281
case tp: (TypeRef | AppliedType) =>

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

Lines changed: 35 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -463,8 +463,8 @@ class CheckCaptures extends Recheck, SymTransformer:
463463

464464
/** A specialized implementation of the selection rule.
465465
*
466-
* E |- f: f{ m: Cr R }^Cf
467-
* -----------------------
466+
* E |- f: T{ m: R^Cr }^{f}
467+
* ------------------------
468468
* E |- f.m: R^C
469469
*
470470
* The implementation picks as `C` one of `{f}` or `Cr`, depending on the
@@ -507,17 +507,6 @@ class CheckCaptures extends Recheck, SymTransformer:
507507
selType
508508
}//.showing(i"recheck sel $tree, $qualType = $result")
509509

510-
/** A specialized implementation of the apply rule.
511-
*
512-
* E |- f: Ra ->Cf Rr^Cr
513-
* E |- a: Ra^Ca
514-
* ---------------------
515-
* E |- f a: Rr^C
516-
*
517-
* The implementation picks as `C` one of `{f, a}` or `Cr`, depending on the
518-
* outcome of a `mightSubcapture` test. It picks `{f, a}` if this might subcapture Cr
519-
* and Cr otherwise.
520-
*/
521510
override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
522511
val meth = tree.fun.symbol
523512

@@ -552,31 +541,47 @@ class CheckCaptures extends Recheck, SymTransformer:
552541
tp.derivedCapturingType(forceBox(parent), refs)
553542
mapArgUsing(forceBox)
554543
else
555-
handleCall(meth, tree, () => Existential.toCap(super.recheckApply(tree, pt))) match
556-
case appType @ CapturingType(appType1, refs) =>
557-
tree.fun match
558-
case Select(qual, _)
559-
if !tree.fun.symbol.isConstructor
560-
&& !qual.tpe.isBoxedCapturing
561-
&& !tree.args.exists(_.tpe.isBoxedCapturing)
562-
&& qual.tpe.captureSet.mightSubcapture(refs)
563-
&& tree.args.forall(_.tpe.captureSet.mightSubcapture(refs))
564-
=>
565-
val callCaptures = tree.args.foldLeft(qual.tpe.captureSet): (cs, arg) =>
566-
cs ++ arg.tpe.captureSet
567-
appType.derivedCapturingType(appType1, callCaptures)
568-
.showing(i"narrow $tree: $appType, refs = $refs, qual-cs = ${qual.tpe.captureSet} = $result", capt)
569-
case _ => appType
570-
case appType => appType
544+
handleCall(meth, tree, () => super.recheckApply(tree, pt))
571545
end recheckApply
572546

573-
override def recheckArg(arg: Tree, formal: Type)(using Context): Type =
547+
protected override
548+
def recheckArg(arg: Tree, formal: Type)(using Context): Type =
574549
val argType = recheck(arg, formal)
575550
if unboxedArgs.remove(arg) && ccConfig.useUnboxedParams then
576551
capt.println(i"charging deep capture set of $arg: ${argType} = ${CaptureSet.deepCaptureSet(argType)}")
577552
markFree(CaptureSet.deepCaptureSet(argType), arg.srcPos)
578553
argType
579554

555+
/** A specialized implementation of the apply rule.
556+
*
557+
* E |- f: Ra ->Cf Rr^Cr
558+
* E |- a: Ra^Ca
559+
* ---------------------
560+
* E |- f a: Rr^C
561+
*
562+
* The implementation picks as `C` one of `{f, a}` or `Cr`, depending on the
563+
* outcome of a `mightSubcapture` test. It picks `{f, a}` if this might subcapture Cr
564+
* and Cr otherwise.
565+
*/
566+
protected override
567+
def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
568+
Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes)) match
569+
case appType @ CapturingType(appType1, refs)
570+
if qualType.exists
571+
&& !tree.fun.symbol.isConstructor
572+
&& !qualType.isBoxedCapturing // TODO: This is not strng enough, we also have
573+
// to exclude existentials in function results
574+
&& !argTypes.exists(_.isBoxedCapturing)
575+
&& qualType.captureSet.mightSubcapture(refs)
576+
&& argTypes.forall(_.captureSet.mightSubcapture(refs))
577+
=>
578+
val callCaptures = tree.args.foldLeft(qualType.captureSet): (cs, arg) =>
579+
cs ++ arg.tpe.captureSet
580+
appType.derivedCapturingType(appType1, callCaptures)
581+
.showing(i"narrow $tree: $appType, refs = $refs, qual-cs = ${qualType.captureSet} = $result", capt)
582+
case appType =>
583+
appType
584+
580585
private def isDistinct(xs: List[Type]): Boolean = xs match
581586
case x :: xs1 => xs1.isEmpty || !xs1.contains(x) && isDistinct(xs1)
582587
case Nil => true

‎compiler/src/dotty/tools/dotc/transform/Recheck.scala

Lines changed: 21 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -202,11 +202,13 @@ abstract class Recheck extends Phase, SymTransformer:
202202
tree.tpe
203203

204204
def recheckSelect(tree: Select, pt: Type)(using Context): Type =
205-
val Select(qual, name) = tree
205+
recheckSelection(tree, recheckSelectQualifier(tree), tree.name, pt)
206+
207+
def recheckSelectQualifier(tree: Select)(using Context): Type =
206208
val proto =
207209
if tree.symbol == defn.Any_asInstanceOf then WildcardType
208210
else AnySelectionProto
209-
recheckSelection(tree, recheck(qual, proto).widenIfUnstable, name, pt)
211+
recheck(tree.qualifier, proto).widenIfUnstable
210212

211213
def recheckSelection(tree: Select, qualType: Type, name: Name,
212214
sharpen: Denotation => Denotation)(using Context): Type =
@@ -292,8 +294,23 @@ abstract class Recheck extends Phase, SymTransformer:
292294
protected def recheckArg(arg: Tree, formal: Type)(using Context): Type =
293295
recheck(arg, formal)
294296

297+
/** A hook to check all the parts of an application:
298+
* @param tree the application `fn(args)`
299+
* @param qualType if the `fn` is a select `q.m`, the type of the qualifier `q`,
300+
* otherwise NoType
301+
* @param funType the method type of `fn`
302+
* @param argTypes the types of the arguments
303+
*/
304+
protected def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
305+
constFold(tree, instantiate(funType, argTypes, tree.fun.symbol))
306+
295307
def recheckApply(tree: Apply, pt: Type)(using Context): Type =
296-
val funtpe0 = recheck(tree.fun)
308+
val (funtpe0, qualType) = tree.fun match
309+
case fun: Select =>
310+
val qualType = recheckSelectQualifier(fun)
311+
(recheckSelection(fun, qualType, fun.name, WildcardType), qualType)
312+
case _ =>
313+
(recheck(tree.fun), NoType)
297314
// reuse the tree's type on signature polymorphic methods, instead of using the (wrong) rechecked one
298315
val funtpe1 = if tree.fun.symbol.originalSignaturePolymorphic.exists then tree.fun.tpe else funtpe0
299316
funtpe1.widen match
@@ -316,7 +333,7 @@ abstract class Recheck extends Phase, SymTransformer:
316333
assert(formals.isEmpty)
317334
Nil
318335
val argTypes = recheckArgs(tree.args, formals, fntpe.paramRefs)
319-
constFold(tree, instantiate(fntpe, argTypes, tree.fun.symbol))
336+
recheckApplication(tree, qualType, fntpe1, argTypes)
320337
//.showing(i"typed app $tree : $fntpe with ${tree.args}%, % : $argTypes%, % = $result")
321338
case tp =>
322339
assert(false, i"unexpected type of ${tree.fun}: $tp")

‎tests/neg-custom-args/captures/caseclass/Test_2.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,4 +22,4 @@ def test(c: C) =
2222

2323
val y4 = y3 match
2424
case Ref(xx) => xx
25-
val y4c: () ->{x3} Unit = y4
25+
val y4c: () ->{y3} Unit = y4

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,16 @@
3434
| that type captures the root capability `cap`.
3535
| This is often caused by a local capability in an argument of constructor Id
3636
| leaking as part of its result.
37+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:57:6 ---------------------------------------
38+
57 | id(() => f.write()) // error
39+
| ^^^^^^^^^^^^^^^^^^^
40+
| Found: () => Unit
41+
| Required: () ->? Unit
42+
|
43+
| Note that the universal capability `cap`
44+
| cannot be included in capture set ?
45+
|
46+
| longer explanation available when compiling with `-explain`
3747
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:64:27 --------------------------------------
3848
64 | val f1: File^{id*} = id(f) // error, since now id(f): File^
3949
| ^^^^^

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ class Id[-A, +B >: A]():
5454
def test =
5555
val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
5656
usingFile: f =>
57-
id(() => f.write()) // escape, if it was not for the error above
57+
id(() => f.write()) // error
5858

5959
def attack2 =
6060
val id: File^ -> File^ = x => x

‎tests/neg-custom-args/captures/unsound-reach-2.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ def bad(): Unit =
2020

2121
var escaped: File^{backdoor*} = null
2222
withFile("hello.txt"): f =>
23-
boom.use(f): // error
23+
boom.use(f):
2424
new Consumer[File^{backdoor*}]: // error
2525
def apply(f1: File^{backdoor*}) =
2626
escaped = f1

‎tests/neg-custom-args/captures/unsound-reach-3.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ def bad(): Unit =
1616
val boom: Foo[File^{backdoor*}] = backdoor
1717

1818
var escaped: File^{backdoor*} = null
19-
withFile("hello.txt"): f =>
20-
escaped = boom.use(f) // error
19+
withFile("hello.txt"): f => // error
20+
escaped = boom.use(f)
2121
// boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed
2222
// f: File^, so there is no reach capabilities
2323

‎tests/neg-custom-args/captures/unsound-reach-4.check

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
-- Error: tests/neg-custom-args/captures/unsound-reach-4.scala:22:19 ---------------------------------------------------
2-
22 | escaped = boom.use(f) // error
3-
| ^^^^^^^^
4-
| Reach capability backdoor* and universal capability cap cannot both
5-
| appear in the type (x: F): box File^{backdoor*} of this expression
1+
-- Error: tests/neg-custom-args/captures/unsound-reach-4.scala:21:25 ---------------------------------------------------
2+
21 | withFile("hello.txt"): f => // error
3+
| ^
4+
| Reach capability backdoor* and universal capability cap cannot both
5+
| appear in the type (f: File^) ->{backdoor*} Unit of this expression
6+
22 | escaped = boom.use(f)

‎tests/neg-custom-args/captures/unsound-reach-4.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,5 +18,5 @@ def bad(): Unit =
1818
val boom: Foo[File^{backdoor*}] = backdoor
1919

2020
var escaped: File^{backdoor*} = null
21-
withFile("hello.txt"): f =>
22-
escaped = boom.use(f) // error
21+
withFile("hello.txt"): f => // error
22+
escaped = boom.use(f)

0 commit comments

Comments
 (0)