Skip to content

Commit 890a2ba

Browse files
oderskyodersky
committed
Revise inferred type checking
The new check is that a publicly visible inferred type after capture checking must conform to the type before capture checking (which is also the type seen by other separately compiled units).
1 parent 66546df commit 890a2ba

File tree

5 files changed

+134
-85
lines changed

5 files changed

+134
-85
lines changed

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -272,6 +272,16 @@ extension (tp: Type)
272272
case _: TypeRef | _: AppliedType => tp.typeSymbol.hasAnnotation(defn.CapabilityAnnot)
273273
case _ => false
274274

275+
/** Drop @retains annotations everywhere */
276+
def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
277+
val tm = new TypeMap:
278+
def apply(t: Type) = t match
279+
case AnnotatedType(parent, annot) if annot.symbol == defn.RetainsAnnot =>
280+
apply(parent)
281+
case _ =>
282+
mapOver(t)
283+
tm(tp)
284+
275285
extension (cls: Symbol)
276286

277287
def pureBaseClass(using Context): Option[Symbol] =

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

Lines changed: 37 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -573,7 +573,7 @@ class CheckCaptures extends Recheck, SymTransformer:
573573
override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
574574
try
575575
if sym.is(Module) then sym.info // Modules are checked by checking the module class
576-
else super.recheckValDef(tree, sym)
576+
else checkInferredResult(super.recheckValDef(tree, sym), tree)
577577
finally
578578
if !sym.is(Param) then
579579
// Parameters with inferred types belong to anonymous methods. We need to wait
@@ -589,11 +589,46 @@ class CheckCaptures extends Recheck, SymTransformer:
589589
val localSet = capturedVars(sym)
590590
if !localSet.isAlwaysEmpty then
591591
curEnv = Env(sym, EnvKind.Regular, localSet, curEnv)
592-
try super.recheckDefDef(tree, sym)
592+
try checkInferredResult(super.recheckDefDef(tree, sym), tree)
593593
finally
594594
interpolateVarsIn(tree.tpt)
595595
curEnv = saved
596596

597+
def checkInferredResult(tp: Type, tree: ValOrDefDef)(using Context): Type =
598+
val sym = tree.symbol
599+
600+
def isLocal =
601+
sym.owner.ownersIterator.exists(_.isTerm)
602+
|| sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
603+
604+
def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
605+
sym.is(Private) // private symbols can always have inferred types
606+
|| sym.name.is(DefaultGetterName) // default getters are exempted since otherwise it would be
607+
// too annoying. This is a hole since a defualt getter's result type
608+
// might leak into a type variable.
609+
|| // non-local symbols cannot have inferred types since external capture types are not inferred
610+
isLocal // local symbols still need explicit types if
611+
&& !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
612+
613+
def addenda(expected: Type) = new Addenda:
614+
override def toAdd(using Context) =
615+
def result = if tree.isInstanceOf[ValDef] then"" else " result"
616+
i"""
617+
|
618+
|Note that the expected type $expected
619+
|is the previously inferred$result type of $sym
620+
|which is also the type seen in separately compiled sources.
621+
|The new inferred type $tp
622+
|must conform to this type.""" :: Nil
623+
624+
tree.tpt match
625+
case tpt: InferredTypeTree if !canUseInferred =>
626+
val expected = tpt.tpe.dropAllRetains
627+
checkConformsExpr(tp, expected, tree.rhs, addenda(expected))
628+
case _ =>
629+
tp
630+
end checkInferredResult
631+
597632
/** Class-specific capture set relations:
598633
* 1. The capture set of a class includes the capture sets of its parents.
599634
* 2. The capture set of the self type of a class includes the capture set of the class.
@@ -1148,9 +1183,6 @@ class CheckCaptures extends Recheck, SymTransformer:
11481183

11491184
/** Perform the following kinds of checks
11501185
* - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
1151-
* - Check that externally visible `val`s or `def`s have empty capture sets. If not,
1152-
* suggest an explicit type. This is so that separate compilation (where external
1153-
* symbols have empty capture sets) gives the same results as joint compilation.
11541186
* - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
11551187
* - Heal ill-formed capture sets of type parameters. See `healTypeParam`.
11561188
*/
@@ -1169,41 +1201,6 @@ class CheckCaptures extends Recheck, SymTransformer:
11691201
case AnnotatedType(parent, annot) if annot.symbol == defn.RetainsAnnot =>
11701202
checkWellformedPost(parent, annot.tree, tree)
11711203
case _ =>
1172-
case t: ValOrDefDef
1173-
if t.tpt.isInstanceOf[InferredTypeTree] && !Synthetics.isExcluded(t.symbol) =>
1174-
val sym = t.symbol
1175-
val isLocal =
1176-
sym.owner.ownersIterator.exists(_.isTerm)
1177-
|| sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
1178-
def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
1179-
sym.is(Private) // Private symbols can always have inferred types
1180-
|| sym.name.is(DefaultGetterName) // Default getters are exempted since otherwise it would be
1181-
// too annoying. This is a hole since a defualt getter's result type
1182-
// might leak into a type variable.
1183-
|| // non-local symbols cannot have inferred types since external capture types are not inferred
1184-
isLocal // local symbols still need explicit types if
1185-
&& !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
1186-
|| // If there are overridden symbols, their types form an upper bound
1187-
sym.allOverriddenSymbols.nonEmpty // for the inferred type. In this case, separate compilation would
1188-
// not be a soundness issue.
1189-
def isNotPureThis(ref: CaptureRef) = ref match {
1190-
case ref: ThisType => !ref.cls.isPureClass
1191-
case _ => true
1192-
}
1193-
if !canUseInferred then
1194-
val inferred = t.tpt.knownType
1195-
def checkPure(tp: Type) = tp match
1196-
case CapturingType(_, refs: CaptureSet.Var)
1197-
if !refs.elems.filter(isNotPureThis).isEmpty =>
1198-
val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
1199-
report.error(
1200-
em"""Non-local $sym cannot have an inferred$resultStr type
1201-
|$inferred
1202-
|with non-empty capture set $refs.
1203-
|The type needs to be declared explicitly.""".withoutDisambiguation(),
1204-
t.srcPos)
1205-
case _ =>
1206-
inferred.foreachPart(checkPure, StopAt.Static)
12071204
case t @ TypeApply(fun, args) =>
12081205
fun.knownType.widen match
12091206
case tl: PolyType =>

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

Lines changed: 5 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
127127
val newInfo =
128128
if needsInfoTransform then
129129
atPhase(thisPhase.next)(symd.maybeOwner.info) // ensure owner is completed
130-
transformExplicitType(sym.info, rootTarget = if newScheme then sym else NoSymbol)
130+
transformExplicitType(sym.info, rootTarget = if newScheme && false then sym else NoSymbol)
131131
else sym.info
132132

133133
if newFlags != symd.flags || (newInfo ne sym.info)
@@ -189,14 +189,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
189189
private def mapInferred(rootTarget: Symbol)(using Context) = new TypeMap:
190190
override def toString = "map inferred"
191191

192-
/** Drop @retains annotations everywhere */
193-
object cleanup extends TypeMap:
194-
def apply(t: Type) = t match
195-
case AnnotatedType(parent, annot) if annot.symbol == defn.RetainsAnnot =>
196-
apply(parent)
197-
case _ =>
198-
mapOver(t)
199-
200192
/** Refine a possibly applied class type C where the class has tracked parameters
201193
* x_1: T_1, ..., x_n: T_n to C { val x_1: CV_1 T_1, ..., val x_n: CV_n T_n }
202194
* where CV_1, ..., CV_n are fresh capture sets.
@@ -265,7 +257,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
265257
// Don't recurse into parameter bounds, just cleanup any stray retains annotations
266258
// !!! TODO we should also map roots to rootvars here
267259
tp.derivedLambdaType(
268-
paramInfos = tp.paramInfos.mapConserve(cleanup(_).bounds),
260+
paramInfos = tp.paramInfos.mapConserve(_.dropAllRetains.bounds),
269261
resType = this(tp.resType))
270262
case Box(tp1) =>
271263
box(this(tp1))
@@ -480,14 +472,14 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
480472
tree.rhs match
481473
case possiblyTypedClosureDef(ddef) if !mentionsCap(rhsOfEtaExpansion(ddef)) =>
482474
//ddef.symbol.setNestingLevel(ctx.owner.nestingLevel + 1)
483-
if newScheme then ccState.isLevelOwner(sym) = true
475+
if newScheme && false then ccState.isLevelOwner(sym) = true
484476
ccState.isLevelOwner(ddef.symbol) = true
485477
// Toplevel closures bound to vals count as level owners
486478
// unless the closure is an implicit eta expansion over a type application
487479
// that mentions `cap`. In that case we prefer not to silently rebind
488480
// the `cap` to a local root of an invisible closure. See
489481
// pos-custom-args/captures/eta-expansions.scala for examples of both cases.
490-
newScheme || !tpt.isInstanceOf[InferredTypeTree]
482+
(newScheme && false) || !tpt.isInstanceOf[InferredTypeTree]
491483
// in this case roots in inferred val type count as polymorphic
492484
case _ =>
493485
true
@@ -564,7 +556,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
564556
prevLambdas: List[LambdaType] // the outer method and polytypes generated previously in reverse order
565557
): Type =
566558
val mapr =
567-
if !newScheme && sym.isLevelOwner
559+
if !(newScheme && false) && sym.isLevelOwner
568560
then mapRoots(sym.localRoot.termRef, defn.captureRoot.termRef)
569561
else identity[Type]
570562
info match

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

Lines changed: 56 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,60 @@
1-
-- Error: tests/neg-custom-args/captures/i15116.scala:3:6 --------------------------------------------------------------
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:3:13 ----------------------------------------
22
3 | val x = Foo(m) // error
3-
| ^^^^^^^^^^^^^^
4-
| Non-local value x cannot have an inferred type
5-
| Foo{val m: String^{Bar.this.m}}^{Bar.this.m}
6-
| with non-empty capture set {Bar.this.m}.
7-
| The type needs to be declared explicitly.
8-
-- Error: tests/neg-custom-args/captures/i15116.scala:5:6 --------------------------------------------------------------
3+
| ^^^^^^
4+
| Found: Foo{val m²: (Bar.this.m : String^{cap[Bar]})}^{Bar.this.m}
5+
| Required: Foo
6+
|
7+
| where: m is a value in class Bar
8+
| m² is a value in class Foo
9+
|
10+
|
11+
| Note that the expected type Foo
12+
| is the previously inferred type of value x
13+
| which is also the type seen in separately compiled sources.
14+
| The new inferred type Foo{val m: (Bar.this.m : String^{cap[Bar]})}^{Bar.this.m}
15+
| must conform to this type.
16+
|
17+
| longer explanation available when compiling with `-explain`
18+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:5:13 ----------------------------------------
919
5 | val x = Foo(m) // error
10-
| ^^^^^^^^^^^^^^
11-
| Non-local value x cannot have an inferred type
12-
| Foo{val m: String^{Baz.this}}^{Baz.this}
13-
| with non-empty capture set {Baz.this}.
14-
| The type needs to be declared explicitly.
15-
-- Error: tests/neg-custom-args/captures/i15116.scala:7:6 --------------------------------------------------------------
20+
| ^^^^^^
21+
| Found: Foo{val m: String^{Baz.this}}^{Baz.this}
22+
| Required: Foo
23+
|
24+
| Note that the expected type Foo
25+
| is the previously inferred type of value x
26+
| which is also the type seen in separately compiled sources.
27+
| The new inferred type Foo{val m: String^{Baz.this}}^{Baz.this}
28+
| must conform to this type.
29+
|
30+
| longer explanation available when compiling with `-explain`
31+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:7:13 ----------------------------------------
1632
7 | val x = Foo(m) // error
17-
| ^^^^^^^^^^^^^^
18-
| Non-local value x cannot have an inferred type
19-
| Foo{val m: String^{Bar1.this.m}}^{Bar1.this.m}
20-
| with non-empty capture set {Bar1.this.m}.
21-
| The type needs to be declared explicitly.
22-
-- Error: tests/neg-custom-args/captures/i15116.scala:9:6 --------------------------------------------------------------
33+
| ^^^^^^
34+
| Found: Foo{val m²: (Bar1.this.m : String^{cap[Bar1]})}^{Bar1.this.m}
35+
| Required: Foo
36+
|
37+
| where: m is a value in class Bar1
38+
| m² is a value in class Foo
39+
|
40+
|
41+
| Note that the expected type Foo
42+
| is the previously inferred type of value x
43+
| which is also the type seen in separately compiled sources.
44+
| The new inferred type Foo{val m: (Bar1.this.m : String^{cap[Bar1]})}^{Bar1.this.m}
45+
| must conform to this type.
46+
|
47+
| longer explanation available when compiling with `-explain`
48+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:9:13 ----------------------------------------
2349
9 | val x = Foo(m) // error
24-
| ^^^^^^^^^^^^^^
25-
| Non-local value x cannot have an inferred type
26-
| Foo{val m: String^{Baz2.this}}^{Baz2.this}
27-
| with non-empty capture set {Baz2.this}.
28-
| The type needs to be declared explicitly.
50+
| ^^^^^^
51+
| Found: Foo{val m: String^{Baz2.this}}^{Baz2.this}
52+
| Required: Foo
53+
|
54+
| Note that the expected type Foo
55+
| is the previously inferred type of value x
56+
| which is also the type seen in separately compiled sources.
57+
| The new inferred type Foo{val m: String^{Baz2.this}}^{Baz2.this}
58+
| must conform to this type.
59+
|
60+
| longer explanation available when compiling with `-explain`

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

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,16 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:23:27 ---------------------------------
2+
23 | val later = usingLogFile { f => () => f.write(0) } // error
3+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
| Found: () ->{x$0, local} Unit
5+
| Required: () -> Unit
6+
|
7+
| Note that the expected type () -> Unit
8+
| is the previously inferred type of value later
9+
| which is also the type seen in separately compiled sources.
10+
| The new inferred type box () ->{x$0, local} Unit
11+
| must conform to this type.
12+
|
13+
| longer explanation available when compiling with `-explain`
114
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:32:37 ------------------------------------------------------
215
32 | usingLogFile { f => later3 = () => f.write(0) } // error
316
| ^
@@ -10,18 +23,23 @@
1023
| Required: Test2.Cell[box () ->{cap[<root>]} Unit]
1124
|
1225
| longer explanation available when compiling with `-explain`
13-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:14 ------------------------------------------------------
14-
23 | val later = usingLogFile { f => () => f.write(0) } // error
15-
| ^^^^^^^^^^^^
16-
| escaping local reference local.type
26+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:47:27 ---------------------------------
27+
47 | val later = usingLogFile { f => () => f.write(0) } // error
28+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
29+
| Found: () ->{x$0, local} Unit
30+
| Required: () -> Unit
31+
|
32+
| Note that the expected type () -> Unit
33+
| is the previously inferred type of value later
34+
| which is also the type seen in separately compiled sources.
35+
| The new inferred type box (() ->{x$0, local} Unit)^?
36+
| must conform to this type.
37+
|
38+
| longer explanation available when compiling with `-explain`
1739
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:28:23 ------------------------------------------------------
1840
28 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
1941
| ^^^^^^^^^^^^
2042
| escaping local reference local.type
21-
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:14 ------------------------------------------------------
22-
47 | val later = usingLogFile { f => () => f.write(0) } // error
23-
| ^^^^^^^^^^^^
24-
| escaping local reference local.type
2543
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:16 ------------------------------------------------------
2644
62 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
2745
| ^^^^^^^^^

0 commit comments

Comments
 (0)