Skip to content

Commit

Permalink
Revise inferred type checking
Browse files Browse the repository at this point in the history 
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).
  • Loading branch information
@odersky
odersky committed Sep 20, 2023
1 parent 66546df commit 890a2ba
Show file tree
Hide file tree
Showing 5 changed files with 134 additions and 85 deletions.
10 changes: 10 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,16 @@ extension (tp: Type)
case _: TypeRef | _: AppliedType => tp.typeSymbol.hasAnnotation(defn.CapabilityAnnot)
case _ => false

/** Drop @retains annotations everywhere */
def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
val tm = new TypeMap:
def apply(t: Type) = t match
case AnnotatedType(parent, annot) if annot.symbol == defn.RetainsAnnot =>
apply(parent)
case _ =>
mapOver(t)
tm(tp)

extension (cls: Symbol)

def pureBaseClass(using Context): Option[Symbol] =
Expand Down
77 changes: 37 additions & 40 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -573,7 +573,7 @@ class CheckCaptures extends Recheck, SymTransformer:
override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
try
if sym.is(Module) then sym.info // Modules are checked by checking the module class
else super.recheckValDef(tree, sym)
else checkInferredResult(super.recheckValDef(tree, sym), tree)
finally
if !sym.is(Param) then
// Parameters with inferred types belong to anonymous methods. We need to wait
Expand All @@ -589,11 +589,46 @@ class CheckCaptures extends Recheck, SymTransformer:
val localSet = capturedVars(sym)
if !localSet.isAlwaysEmpty then
curEnv = Env(sym, EnvKind.Regular, localSet, curEnv)
try super.recheckDefDef(tree, sym)
try checkInferredResult(super.recheckDefDef(tree, sym), tree)
finally
interpolateVarsIn(tree.tpt)
curEnv = saved

def checkInferredResult(tp: Type, tree: ValOrDefDef)(using Context): Type =
val sym = tree.symbol

def isLocal =
sym.owner.ownersIterator.exists(_.isTerm)
|| sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)

def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
sym.is(Private) // private symbols can always have inferred types
|| sym.name.is(DefaultGetterName) // default getters are exempted since otherwise it would be
// too annoying. This is a hole since a defualt getter's result type
// might leak into a type variable.
|| // non-local symbols cannot have inferred types since external capture types are not inferred
isLocal // local symbols still need explicit types if
&& !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference

def addenda(expected: Type) = new Addenda:
override def toAdd(using Context) =
def result = if tree.isInstanceOf[ValDef] then"" else " result"
i"""
|
|Note that the expected type $expected
|is the previously inferred$result type of $sym
|which is also the type seen in separately compiled sources.
|The new inferred type $tp
|must conform to this type.""" :: Nil

tree.tpt match
case tpt: InferredTypeTree if !canUseInferred =>
val expected = tpt.tpe.dropAllRetains
checkConformsExpr(tp, expected, tree.rhs, addenda(expected))
case _ =>
tp
end checkInferredResult

/** Class-specific capture set relations:
* 1. The capture set of a class includes the capture sets of its parents.
* 2. The capture set of the self type of a class includes the capture set of the class.
Expand Down Expand Up @@ -1148,9 +1183,6 @@ class CheckCaptures extends Recheck, SymTransformer:

/** Perform the following kinds of checks
* - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
* - Check that externally visible `val`s or `def`s have empty capture sets. If not,
* suggest an explicit type. This is so that separate compilation (where external
* symbols have empty capture sets) gives the same results as joint compilation.
* - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
* - Heal ill-formed capture sets of type parameters. See `healTypeParam`.
*/
Expand All @@ -1169,41 +1201,6 @@ class CheckCaptures extends Recheck, SymTransformer:
case AnnotatedType(parent, annot) if annot.symbol == defn.RetainsAnnot =>
checkWellformedPost(parent, annot.tree, tree)
case _ =>
case t: ValOrDefDef
if t.tpt.isInstanceOf[InferredTypeTree] && !Synthetics.isExcluded(t.symbol) =>
val sym = t.symbol
val isLocal =
sym.owner.ownersIterator.exists(_.isTerm)
|| sym.accessBoundary(defn.RootClass).isContainedIn(sym.topLevelClass)
def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly
sym.is(Private) // Private symbols can always have inferred types
|| sym.name.is(DefaultGetterName) // Default getters are exempted since otherwise it would be
// too annoying. This is a hole since a defualt getter's result type
// might leak into a type variable.
|| // non-local symbols cannot have inferred types since external capture types are not inferred
isLocal // local symbols still need explicit types if
&& !sym.owner.is(Trait) // they are defined in a trait, since we do OverridingPairs checking before capture inference
|| // If there are overridden symbols, their types form an upper bound
sym.allOverriddenSymbols.nonEmpty // for the inferred type. In this case, separate compilation would
// not be a soundness issue.
def isNotPureThis(ref: CaptureRef) = ref match {
case ref: ThisType => !ref.cls.isPureClass
case _ => true
}
if !canUseInferred then
val inferred = t.tpt.knownType
def checkPure(tp: Type) = tp match
case CapturingType(_, refs: CaptureSet.Var)
if !refs.elems.filter(isNotPureThis).isEmpty =>
val resultStr = if t.isInstanceOf[DefDef] then " result" else ""
report.error(
em"""Non-local $sym cannot have an inferred$resultStr type
|$inferred
|with non-empty capture set $refs.
|The type needs to be declared explicitly.""".withoutDisambiguation(),
t.srcPos)
case _ =>
inferred.foreachPart(checkPure, StopAt.Static)
case t @ TypeApply(fun, args) =>
fun.knownType.widen match
case tl: PolyType =>
Expand Down
18 changes: 5 additions & 13 deletions compiler/src/dotty/tools/dotc/cc/Setup.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
val newInfo =
if needsInfoTransform then
atPhase(thisPhase.next)(symd.maybeOwner.info) // ensure owner is completed
transformExplicitType(sym.info, rootTarget = if newScheme then sym else NoSymbol)
transformExplicitType(sym.info, rootTarget = if newScheme && false then sym else NoSymbol)
else sym.info

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

/** Drop @retains annotations everywhere */
object cleanup extends TypeMap:
def apply(t: Type) = t match
case AnnotatedType(parent, annot) if annot.symbol == defn.RetainsAnnot =>
apply(parent)
case _ =>
mapOver(t)

/** Refine a possibly applied class type C where the class has tracked parameters
* x_1: T_1, ..., x_n: T_n to C { val x_1: CV_1 T_1, ..., val x_n: CV_n T_n }
* where CV_1, ..., CV_n are fresh capture sets.
Expand Down Expand Up @@ -265,7 +257,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
// Don't recurse into parameter bounds, just cleanup any stray retains annotations
// !!! TODO we should also map roots to rootvars here
tp.derivedLambdaType(
paramInfos = tp.paramInfos.mapConserve(cleanup(_).bounds),
paramInfos = tp.paramInfos.mapConserve(_.dropAllRetains.bounds),
resType = this(tp.resType))
case Box(tp1) =>
box(this(tp1))
Expand Down Expand Up @@ -480,14 +472,14 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
tree.rhs match
case possiblyTypedClosureDef(ddef) if !mentionsCap(rhsOfEtaExpansion(ddef)) =>
//ddef.symbol.setNestingLevel(ctx.owner.nestingLevel + 1)
if newScheme then ccState.isLevelOwner(sym) = true
if newScheme && false then ccState.isLevelOwner(sym) = true
ccState.isLevelOwner(ddef.symbol) = true
// Toplevel closures bound to vals count as level owners
// unless the closure is an implicit eta expansion over a type application
// that mentions `cap`. In that case we prefer not to silently rebind
// the `cap` to a local root of an invisible closure. See
// pos-custom-args/captures/eta-expansions.scala for examples of both cases.
newScheme || !tpt.isInstanceOf[InferredTypeTree]
(newScheme && false) || !tpt.isInstanceOf[InferredTypeTree]
// in this case roots in inferred val type count as polymorphic
case _ =>
true
Expand Down Expand Up @@ -564,7 +556,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
prevLambdas: List[LambdaType] // the outer method and polytypes generated previously in reverse order
): Type =
val mapr =
if !newScheme && sym.isLevelOwner
if !(newScheme && false) && sym.isLevelOwner
then mapRoots(sym.localRoot.termRef, defn.captureRoot.termRef)
else identity[Type]
info match
Expand Down
80 changes: 56 additions & 24 deletions tests/neg-custom-args/captures/i15116.check
View file
Original file line number Diff line number Diff line change
@@ -1,28 +1,60 @@
-- Error: tests/neg-custom-args/captures/i15116.scala:3:6 --------------------------------------------------------------
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:3:13 ----------------------------------------
3 | val x = Foo(m) // error
| ^^^^^^^^^^^^^^
| Non-local value x cannot have an inferred type
| Foo{val m: String^{Bar.this.m}}^{Bar.this.m}
| with non-empty capture set {Bar.this.m}.
| The type needs to be declared explicitly.
-- Error: tests/neg-custom-args/captures/i15116.scala:5:6 --------------------------------------------------------------
| ^^^^^^
| Found: Foo{val m²: (Bar.this.m : String^{cap[Bar]})}^{Bar.this.m}
| Required: Foo
|
| where: m is a value in class Bar
| m² is a value in class Foo
|
|
| Note that the expected type Foo
| is the previously inferred type of value x
| which is also the type seen in separately compiled sources.
| The new inferred type Foo{val m: (Bar.this.m : String^{cap[Bar]})}^{Bar.this.m}
| must conform to this type.
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:5:13 ----------------------------------------
5 | val x = Foo(m) // error
| ^^^^^^^^^^^^^^
| Non-local value x cannot have an inferred type
| Foo{val m: String^{Baz.this}}^{Baz.this}
| with non-empty capture set {Baz.this}.
| The type needs to be declared explicitly.
-- Error: tests/neg-custom-args/captures/i15116.scala:7:6 --------------------------------------------------------------
| ^^^^^^
| Found: Foo{val m: String^{Baz.this}}^{Baz.this}
| Required: Foo
|
| Note that the expected type Foo
| is the previously inferred type of value x
| which is also the type seen in separately compiled sources.
| The new inferred type Foo{val m: String^{Baz.this}}^{Baz.this}
| must conform to this type.
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:7:13 ----------------------------------------
7 | val x = Foo(m) // error
| ^^^^^^^^^^^^^^
| Non-local value x cannot have an inferred type
| Foo{val m: String^{Bar1.this.m}}^{Bar1.this.m}
| with non-empty capture set {Bar1.this.m}.
| The type needs to be declared explicitly.
-- Error: tests/neg-custom-args/captures/i15116.scala:9:6 --------------------------------------------------------------
| ^^^^^^
| Found: Foo{val m²: (Bar1.this.m : String^{cap[Bar1]})}^{Bar1.this.m}
| Required: Foo
|
| where: m is a value in class Bar1
| m² is a value in class Foo
|
|
| Note that the expected type Foo
| is the previously inferred type of value x
| which is also the type seen in separately compiled sources.
| The new inferred type Foo{val m: (Bar1.this.m : String^{cap[Bar1]})}^{Bar1.this.m}
| must conform to this type.
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15116.scala:9:13 ----------------------------------------
9 | val x = Foo(m) // error
| ^^^^^^^^^^^^^^
| Non-local value x cannot have an inferred type
| Foo{val m: String^{Baz2.this}}^{Baz2.this}
| with non-empty capture set {Baz2.this}.
| The type needs to be declared explicitly.
| ^^^^^^
| Found: Foo{val m: String^{Baz2.this}}^{Baz2.this}
| Required: Foo
|
| Note that the expected type Foo
| is the previously inferred type of value x
| which is also the type seen in separately compiled sources.
| The new inferred type Foo{val m: String^{Baz2.this}}^{Baz2.this}
| must conform to this type.
|
| longer explanation available when compiling with `-explain`
34 changes: 26 additions & 8 deletions tests/neg-custom-args/captures/usingLogFile.check
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,16 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:23:27 ---------------------------------
23 | val later = usingLogFile { f => () => f.write(0) } // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: () ->{x$0, local} Unit
| Required: () -> Unit
|
| Note that the expected type () -> Unit
| is the previously inferred type of value later
| which is also the type seen in separately compiled sources.
| The new inferred type box () ->{x$0, local} Unit
| must conform to this type.
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:32:37 ------------------------------------------------------
32 | usingLogFile { f => later3 = () => f.write(0) } // error
| ^
Expand All @@ -10,18 +23,23 @@
| Required: Test2.Cell[box () ->{cap[<root>]} Unit]
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:14 ------------------------------------------------------
23 | val later = usingLogFile { f => () => f.write(0) } // error
| ^^^^^^^^^^^^
| escaping local reference local.type
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:47:27 ---------------------------------
47 | val later = usingLogFile { f => () => f.write(0) } // error
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| Found: () ->{x$0, local} Unit
| Required: () -> Unit
|
| Note that the expected type () -> Unit
| is the previously inferred type of value later
| which is also the type seen in separately compiled sources.
| The new inferred type box (() ->{x$0, local} Unit)^?
| must conform to this type.
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:28:23 ------------------------------------------------------
28 | private val later2 = usingLogFile { f => Cell(() => f.write(0)) } // error
| ^^^^^^^^^^^^
| escaping local reference local.type
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:14 ------------------------------------------------------
47 | val later = usingLogFile { f => () => f.write(0) } // error
| ^^^^^^^^^^^^
| escaping local reference local.type
-- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:16 ------------------------------------------------------
62 | val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
| ^^^^^^^^^
Expand Down

0 comments on commit 890a2ba

Please sign in to comment.