Skip to content

Commit 63080f0

Browse files
oderskyodersky
committed
Pre-type closure bodies if expected type is a parametric function.
Pre-type closure bodies with expected result type if expected type is a parametric function. This avoids turning fresh caps in their result type into result caps
1 parent 6b56e7b commit 63080f0

File tree

13 files changed

+79
-40
lines changed

13 files changed

+79
-40
lines changed

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

Lines changed: 11 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -922,28 +922,22 @@ class CheckCaptures extends Recheck, SymTransformer:
922922
val paramType = freshToCap(paramTpt.nuType)
923923
checkConformsExpr(argType, paramType, param)
924924
.showing(i"compared expected closure formal $argType against $param with ${paramTpt.nuType}", capt)
925-
if ccConfig.preTypeClosureResults && !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially) then
926-
// Check whether the closure's result conforms to the expected type
927-
// This constrains parameter types of the closure which can give better
928-
// error messages.
929-
// But if the closure is an eta expanded method reference it's better to not constrain
925+
if !pt.isInstanceOf[RefinedType]
926+
&& !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially)
927+
then
928+
// If the closure is not an eta expansion and the expected type is a parametric
929+
// function type, check whether the closure's result conforms to the expected
930+
// result type. This constrains parameter types of the closure which can give better
931+
// error messages. It also prevents mapping fresh to result caps in the closure's
932+
// result type.
933+
// If the closure is an eta expanded method reference it's better to not constrain
930934
// its internals early since that would give error messages in generated code
931935
// which are less intelligible. An example is the line `a = x` in
932936
// neg-custom-args/captures/vars.scala. That's why this code is conditioned.
933937
// to apply only to closures that are not eta expansions.
934938
assert(paramss1.isEmpty)
935-
val respt0 = pt match
936-
case defn.RefinedFunctionOf(rinfo) =>
937-
val paramTypes = params.map(_.asInstanceOf[ValDef].tpt.nuType)
938-
rinfo.instantiate(paramTypes)
939-
case _ =>
940-
resType
941-
val respt = resultToFresh(respt0, Origin.LambdaExpected(respt0))
942-
val res = resultToFresh(mdef.tpt.nuType, Origin.LambdaActual(mdef.tpt.nuType))
943-
// We need to open existentials here in order not to get vars mixed up in them
944-
// We do the proper check with existentials when we are finished with the closure block.
945-
capt.println(i"pre-check closure $expr of type $res against $respt")
946-
checkConformsExpr(res, respt, expr)
939+
capt.println(i"pre-check closure $expr of type ${mdef.tpt.nuType} against $resType")
940+
checkConformsExpr(mdef.tpt.nuType, resType, expr)
947941
case _ =>
948942
case Nil =>
949943

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

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,6 @@ object ccConfig:
1010
/** If enabled, cache capture sets of infos capabilties */
1111
inline val cacheCaptureSetOfInfo = false
1212

13-
/** If enabled, use a special path in recheckClosure for closures
14-
* to compare the result tpt of the anonymous functon with the expected
15-
* result type. This can narrow the scope of error messages.
16-
*/
17-
inline val preTypeClosureResults = false
18-
1913
/** If this and `preTypeClosureResults` are both enabled, disable `preTypeClosureResults`
2014
* for eta expansions. This can improve some error messages.
2115
*/

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
6 | bar( () => f ) // error
1111
| ^^^^^^^
1212
| Found: () ->{f} () ->{f} Unit
13-
| Required: () -> () ->? Unit
13+
| Required: () -> () ->{f} Unit
1414
| Note that capability (f : Proc^) is not included in capture set {}.
1515
|
1616
| longer explanation available when compiling with `-explain`

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

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -48,14 +48,11 @@
4848
| Note that capability io.type is not included in capture set {}.
4949
|
5050
| longer explanation available when compiling with `-explain`
51-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:4 --------------------------------
51+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:10 -------------------------------
5252
44 | io => () => io.use() // error
53-
| ^^^^^^^^^^^^^^^^^^^^
54-
| Found: (io: Capp^) ->? () ->{io} Unit
55-
| Required: Capp^ -> () -> Unit
56-
|
57-
| where: ^ refers to the universal root capability
58-
|
59-
| Note that capability io.type is not included in capture set {}.
53+
| ^^^^^^^^^^^^^^
54+
| Found: () ->{io} Unit
55+
| Required: () ->? Unit
56+
| Note that capability (io : Capp^) is not included in capture set {}.
6057
|
6158
| longer explanation available when compiling with `-explain`

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ def bar() = {
1212
val leak = withCap(cap => mkId(cap)) // error
1313
}
1414

15-
package test2:
15+
object test2:
1616
trait Cap { def use(): Int }
1717
type Id[X] = [T] -> (op: X => T) -> T
1818
def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)

‎tests/neg-custom-args/captures/leaked-curried-shared.scala‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
trait Cap extends caps.SharedCapability:
2+
def use(): Unit
3+
4+
def withCap[T](op: (x: Cap) => T): T = ???
5+
6+
trait Box:
7+
val get: () ->{} () => Cap
8+
9+
def main(): Unit =
10+
val leaked = withCap: (io: Cap) =>
11+
class Fuzz extends Box, Pure:
12+
self =>
13+
val get: () ->{} () ->{io} Cap =
14+
() => () => io // error
15+
class Foo extends Box, Pure:
16+
val get: () ->{} () ->{io} Cap =
17+
() => () => io // error
18+
new Foo
19+
val bad = leaked.get()().use() // using a leaked capability
20+

‎tests/neg-custom-args/captures/leaked-curried.check‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,11 @@
66
17 | () => () => io // error
77
| ^^
88
| reference (io : Cap^) is not included in the allowed capture set {} of the self type of class Foo
9+
-- Error: tests/neg-custom-args/captures/leaked-curried.scala:13:15 ----------------------------------------------------
10+
13 | val get: () ->{} () ->{io} Cap^ = // error
11+
| ^^^^^^^^^^^^^^^^^^^^^^
12+
| Separation failure: value get's type () -> () ->{io} Cap^ hides non-local parameter io
13+
-- Error: tests/neg-custom-args/captures/leaked-curried.scala:16:15 ----------------------------------------------------
14+
16 | val get: () ->{} () ->{io} Cap^ = // error
15+
| ^^^^^^^^^^^^^^^^^^^^^^
16+
| Separation failure: value get's type () -> () ->{io} Cap^ hides non-local parameter io

‎tests/neg-custom-args/captures/leaked-curried.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ def main(): Unit =
1010
val leaked = withCap: (io: Cap^) =>
1111
class Fuzz extends Box, Pure:
1212
self =>
13-
val get: () ->{} () ->{io} Cap^ =
13+
val get: () ->{} () ->{io} Cap^ = // error
1414
() => () => io // error
1515
class Foo extends Box, Pure:
16-
val get: () ->{} () ->{io} Cap^ =
16+
val get: () ->{} () ->{io} Cap^ = // error
1717
() => () => io // error
1818
new Foo
1919
val bad = leaked.get()().use() // using a leaked capability

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,3 +133,15 @@
133133
| ^^^^^^^^
134134
| Local reach capability xs* leaks into capture scope of method runAll2.
135135
| To allow this, the parameter xs should be declared with a @use annotation
136+
-- Error: tests/neg-custom-args/captures/reaches.scala:62:36 -----------------------------------------------------------
137+
62 | val leaked = usingFile[File^{id*}]: f => // error: separation
138+
| ^
139+
| Separation failure: Illegal access to cap of value id which is hidden by the previous definition
140+
| of value id with type File^ -> File^².
141+
| This type hides capabilities {cap}
142+
|
143+
| where: ^ refers to the universal root capability
144+
| ^² refers to a fresh root capability in the type of value id
145+
| cap is a fresh root capability created in value id
146+
63 | val f1: File^{id*} = id(f)
147+
64 | f1

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ def attack2 =
5959
val id: File^ -> File^ = x => x // error
6060
// val id: File^ -> File^{fresh}
6161

62-
val leaked = usingFile[File^{id*}]: f => // now ok
62+
val leaked = usingFile[File^{id*}]: f => // error: separation
6363
val f1: File^{id*} = id(f)
6464
f1
6565

0 commit comments

Comments
 (0)