Skip to content

Commit 8c82038

Browse files
oderskyodersky
committed
Improve closure typing
If the closure has an expected function type with a fully defined result type, take the internalized result type as the local return type of the closure. This has the effect that some conformance tests are now done with Fresh instead Result caps. This means a now can widen a local reference to a result cap, since the comparison is done between the local reference and the internalized FreshCap. Previously this failed since we compared a local cap with result cap, and result caps only subtype other result caps. It also propagates types more aggressively into closure bodies, which sometimes reduces the error span and improves the error message.
1 parent 76fbb6b commit 8c82038

21 files changed

+208
-114
lines changed

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

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -951,6 +951,69 @@ object Capabilities:
951951
def freshToCap(param: Symbol, tp: Type)(using Context): Type =
952952
CapToFresh(Origin.Parameter(param)).inverse(tp)
953953

954+
/** The local dual of a result type of a closure type.
955+
* @param binder the method type of the anonymous function whose result is mapped
956+
* @pre the context's owner is the anonymous function
957+
*/
958+
class Internalize(binder: MethodType)(using Context) extends BiTypeMap:
959+
thisMap =>
960+
961+
val sym = ctx.owner
962+
assert(sym.isAnonymousFunction)
963+
val paramSyms = atPhase(ctx.phase.prev):
964+
// We need to ask one phase before since `sym` should not be completed as a side effect.
965+
// The result of Internalize is used to se the result type of an anonymous function, and
966+
// the new info of that function is built with the result.
967+
sym.paramSymss.head
968+
val resultToFresh = EqHashMap[ResultCap, FreshCap]()
969+
val freshToResult = EqHashMap[FreshCap, ResultCap]()
970+
971+
override def apply(t: Type) =
972+
if variance < 0 then t
973+
else t match
974+
case t: ParamRef =>
975+
if t.binder == this.binder then paramSyms(t.paramNum).termRef else t
976+
case _ => mapOver(t)
977+
978+
override def mapCapability(c: Capability, deep: Boolean): Capability = c match
979+
case r: ResultCap if r.binder == this.binder =>
980+
resultToFresh.get(r) match
981+
case Some(f) => f
982+
case None =>
983+
val f = FreshCap(Origin.LocalInstance(binder.resType))
984+
resultToFresh(r) = f
985+
freshToResult(f) = r
986+
f
987+
case _ =>
988+
super.mapCapability(c, deep)
989+
990+
class Inverse extends BiTypeMap:
991+
def apply(t: Type): Type =
992+
if variance < 0 then t
993+
else t match
994+
case t: TermRef if paramSyms.contains(t) =>
995+
binder.paramRefs(paramSyms.indexOf(t.symbol))
996+
case _ => mapOver(t)
997+
998+
override def mapCapability(c: Capability, deep: Boolean): Capability = c match
999+
case f: FreshCap if f.owner == sym =>
1000+
freshToResult.get(f) match
1001+
case Some(r) => r
1002+
case None =>
1003+
val r = ResultCap(binder)
1004+
resultToFresh(r) = f
1005+
freshToResult(f) = r
1006+
r
1007+
case _ => super.mapCapability(c, deep)
1008+
1009+
def inverse = thisMap
1010+
override def toString = thisMap.toString + ".inverse"
1011+
end Inverse
1012+
1013+
override def toString = "InternalizeClosureResult"
1014+
def inverse = Inverse()
1015+
end Internalize
1016+
9541017
/** Map top-level free existential variables one-to-one to Fresh instances */
9551018
def resultToFresh(tp: Type, origin: Origin)(using Context): Type =
9561019
val subst = new TypeMap:

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

Lines changed: 24 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ import config.Printers.{capt, recheckr, noPrinter}
1010
import config.{Config, Feature}
1111
import ast.{tpd, untpd, Trees}
1212
import Trees.*
13+
import typer.ForceDegree
14+
import typer.Inferencing.isFullyDefined
1315
import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
1416
import typer.Checking.{checkBounds, checkAppliedTypesIn}
1517
import typer.ErrorReporting.{Addenda, NothingToAdd, err}
@@ -25,7 +27,7 @@ import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
2527
import reporting.{trace, Message, OverrideError}
2628
import Annotations.Annotation
2729
import Capabilities.*
28-
import dotty.tools.dotc.util.common.alwaysTrue
30+
import util.common.alwaysTrue
2931

3032
/** The capture checker */
3133
object CheckCaptures:
@@ -916,6 +918,7 @@ class CheckCaptures extends Recheck, SymTransformer:
916918
* { def $anonfun(...) = ...; closure($anonfun, ...)}
917919
*/
918920
override def recheckClosureBlock(mdef: DefDef, expr: Closure, pt: Type)(using Context): Type =
921+
val anonfun = mdef.symbol
919922

920923
def matchParams(paramss: List[ParamClause], pt: Type): Unit =
921924
//println(i"match $mdef against $pt")
@@ -931,7 +934,19 @@ class CheckCaptures extends Recheck, SymTransformer:
931934
val paramType = freshToCap(param.symbol, paramTpt.nuType)
932935
checkConformsExpr(argType, paramType, param)
933936
.showing(i"compared expected closure formal $argType against $param with ${paramTpt.nuType}", capt)
934-
if !pt.isInstanceOf[RefinedType]
937+
if ccConfig.newScheme then
938+
if resType.isValueType && isFullyDefined(resType, ForceDegree.none) then
939+
val localResType = pt match
940+
case RefinedType(_, _, mt: MethodType) =>
941+
inContext(ctx.withOwner(anonfun)):
942+
Internalize(mt)(resType)
943+
case _ => resType
944+
mdef.tpt.updNuType(localResType)
945+
// Make sure we affect the info of the anonfun by the previous updNuType
946+
// unless the info is already defined in a previous phase and does not change.
947+
assert(!anonfun.isCompleted || anonfun.denot.validFor.firstPhaseId != thisPhase.id)
948+
//println(i"updating ${mdef.tpt} to $localResType/${mdef.tpt.nuType}")
949+
else if !pt.isInstanceOf[RefinedType]
935950
&& !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially)
936951
then
937952
// If the closure is not an eta expansion and the expected type is a parametric
@@ -950,16 +965,16 @@ class CheckCaptures extends Recheck, SymTransformer:
950965
case _ =>
951966
case Nil =>
952967

953-
openClosures = (mdef.symbol, pt) :: openClosures
968+
openClosures = (anonfun, pt) :: openClosures
954969
// openClosures is needed for errors but currently makes no difference
955970
// TODO follow up on this
956971
try
957972
matchParams(mdef.paramss, pt)
958-
capt.println(i"recheck closure block $mdef: ${mdef.symbol.infoOrCompleter}")
959-
if !mdef.symbol.isCompleted then
960-
mdef.symbol.ensureCompleted() // this will recheck def
973+
capt.println(i"recheck closure block $mdef: ${anonfun.infoOrCompleter}")
974+
if !anonfun.isCompleted then
975+
anonfun.ensureCompleted() // this will recheck def
961976
else
962-
recheckDef(mdef, mdef.symbol)
977+
recheckDef(mdef, anonfun)
963978

964979
recheckClosure(expr, pt, forceDependent = true)
965980
finally
@@ -1463,7 +1478,8 @@ class CheckCaptures extends Recheck, SymTransformer:
14631478
case FunctionOrMethod(aargs, ares) =>
14641479
val saved = curEnv
14651480
curEnv = Env(
1466-
curEnv.owner, EnvKind.NestedInOwner,
1481+
curEnv.owner,
1482+
if boxed then EnvKind.Boxed else EnvKind.NestedInOwner,
14671483
CaptureSet.Var(curEnv.owner, level = ccState.currentLevel),
14681484
if boxed then null else curEnv)
14691485
try

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -165,11 +165,12 @@ abstract class Recheck extends Phase, SymTransformer:
165165
* from the current type.
166166
*/
167167
def setNuType(tpe: Type): Unit =
168-
if nuTypes.lookup(tree) == null then updNuType(tpe)
168+
if nuTypes.lookup(tree) == null && (tpe ne tree.tpe) then
169+
updNuType(tpe)
169170

170171
/** Set new type of the tree unconditionally. */
171172
def updNuType(tpe: Type): Unit =
172-
if tpe ne tree.tpe then nuTypes(tree) = tpe
173+
nuTypes(tree) = tpe
173174

174175
/** The new type of the tree, or if none was installed, the original type */
175176
def nuType(using Context): Type =

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

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:5:2 ------------------------------------------
22
5 | () => if x == null then y else y // error
33
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4-
| Found: () ->{x} C^?
4+
| Found: () ->{x} C
55
| Required: () -> C
66
| Note that capability (x : C^) is not included in capture set {}.
77
|
@@ -52,12 +52,27 @@
5252
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ----------------------------------------
5353
36 | val z2 = h[() -> Cap](() => x) // error // error
5454
| ^^^^^^^
55-
|Found: () ->{x} C^{x}
56-
|Required: () -> C^
55+
|Found: () ->? C^
56+
|Required: () -> C^²
57+
|
58+
|where: ^ refers to a root capability associated with the result type of (): C^
59+
| ^² refers to a fresh root capability created in value z2 when checking argument to parameter a of method h
60+
|
61+
|Note that capability <cap of (): C^> is not included in capture set {cap}
62+
|because <cap of (): C^> is not visible from cap in value z2.
63+
|
64+
| longer explanation available when compiling with `-explain`
65+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:37:5 -----------------------------------------
66+
37 | (() => C()) // error
67+
| ^^^^^^^^^
68+
|Found: () ->? C^
69+
|Required: () -> C^²
5770
|
58-
|where: ^ refers to a fresh root capability created in value z2 when checking argument to parameter a of method h
71+
|where: ^ refers to a root capability associated with the result type of (): C^
72+
| ^² refers to a fresh root capability created in value z2 when checking argument to parameter b of method h
5973
|
60-
|Note that capability (x : C^) is not included in capture set {}.
74+
|Note that capability <cap of (): C^> is not included in capture set {cap}
75+
|because <cap of (): C^> is not visible from cap in value z2.
6176
|
6277
| longer explanation available when compiling with `-explain`
6378
-- Error: tests/neg-custom-args/captures/capt1.scala:38:13 -------------------------------------------------------------

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ def foo() =
3434
def h[X](a: X)(b: X) = a
3535

3636
val z2 = h[() -> Cap](() => x) // error // error
37-
(() => C())
37+
(() => C()) // error
3838
val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C()) // error
3939

4040
val z1: () => Cap = f1(x)

‎tests/neg-custom-args/captures/closure-result-typing.check

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/closure-result-typing.scala:2:30 -------------------------
2+
2 | val x: () -> Object = () => c // error
3+
| ^
4+
| Found: (c : Object^)
5+
| Required: Object
6+
|
7+
| where: ^ refers to a fresh root capability in the type of parameter c
8+
|
9+
| Note that capability cap is not included in capture set {}.
10+
|
11+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/closure-result-typing.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
def test(c: Object^): Unit =
2+
val x: () -> Object = () => c // error

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

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,3 @@
66
| Note that capability (f : Proc^) is not included in capture set {}.
77
|
88
| longer explanation available when compiling with `-explain`
9-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:6:14 -------------------------------------------
10-
6 | bar( () => f ) // error
11-
| ^^^^^^^
12-
| Found: () ->{f} () ->{f} Unit
13-
| Required: () -> () ->{f} Unit
14-
| Note that capability (f : Proc^) is not included in capture set {}.
15-
|
16-
| longer explanation available when compiling with `-explain`

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@
33
def bar[A <: Proc^{f}](g: () -> A): () -> Proc^{f} =
44
g // error
55
val stowaway: () -> Proc^{f} =
6-
bar( () => f ) // error
6+
bar( () => f ) // was error now OK
77
() => { stowaway.apply().apply() }

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/filevar.scala:15:12 --------------------------------------
22
15 | withFile: f => // error with level checking, was OK under both schemes before
33
| ^
4-
|Found: (l: scala.caps.Capability^) ?->? File^? ->? Unit
5-
|Required: (l: scala.caps.Capability^) ?-> (f: File^{l}) => Unit
4+
|Found: (f: File^?) ->? Unit
5+
|Required: (f: File^{l}) => Unit
66
|
7-
|where: => refers to a root capability associated with the result type of (using l: scala.caps.Capability^): (f: File^{l}) => Unit
8-
| ^ refers to the universal root capability
7+
|where: => refers to a fresh root capability created in anonymous function of type (using l²: scala.caps.Capability): File^{l²} -> Unit when instantiating expected result type (f: File^{l}) ->{cap} Unit of function literal
98
|
109
|Note that capability l.type
1110
|cannot be included in outer capture set ? of parameter f.

0 commit comments

Comments
 (0)