Three changes to typing rules #14392
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add recheck phase
A squashed version of the following commits:
Handle byname parameters
Don't force symbol completion when printing flags or annotations
Check overrides and disallow non-local inferred capture types
Handle `this` in capture sets
Print capture variable dependencies under -Ydebug-cc
Avoid spurious error message
Avoid spurious error message
"cannot be tracked since its capture set is empty".
This arose in lazyref.scala for a DependentTypeTree in an anaonymois function.
Dependent type trees map to normal TypeTrees, not InferredTypeTrees (and things
go wrong if we try to change that).
Drop TopType
Consider bounds of type variables to be boxed
More tests
Avoid multiple maps when creating symbol infos
Use a single BiTypeMap to map from inferred result and parameters
to method info.
This improves efficiency and debuggability by reducing the frequence of
multiple stacked maps capture sets.
Refactor with CompareResult#andAlso
Refactoring: use isOK on CompareResult
Reflect inferred parameter types in enclosing method type
The variables in the inferred parameter type of an anonymous function need
to also show up in the closure type itself, so that they can be constrained.
Don't interpolate parameters of anonymous functions
Here, we should wait until we get the info from the outside, which can
be arbitrarily much later.
Compute upper approximation of bimapped sets from both sides
Fail when trying to add new elements to mapped sets
It's the safe option.
Print full origin trail of derived capture sets under -Ycc-debug
Fix isEmpty condition in well-formedness check
Make printing capture sets dependent on -Ycc-debug
Recursion brake for upperApprox
Fixes to upperApprox
Make instantiteRT a BiTypeMap
Otherwise we will not be able to do upper approximations of parameters.
Interpolate only variables at negative polarity
Interpolating covariant variables risks restricting capture sets to early.
For instance, when a variable has the capture set of a called function in
its capture set. When we have indirectly recursive calls it could be that
the capture set of a called function is not yet fully formed.
Interpolate type variables when symbols are completed
Allow for possibility that variables are constant
Only recomplete symbols if their info changes
Add completions to Rechecker
Complete val and def definitions lazily on first access. Now,
recheckDefDef and recheckValDef are called the first time the
new info of the defined symbol is needed, or, if the info is
never needed, when the typer gets to the definitions. This
only applied to definitions with inferred types. The others
are handled in typer sequence, as before.
The motivation of the change is that some modifications to
inferred types of symbols can be made in subclasses without
running into ordering problems.
More fixes for subCapture
New setting -Ycc-debug for more info on capture variables
Fix subCapture in frozen state
Previously, we still OKed two empty variables to be compared with
subcapture in the frozen state. This should give an error.
Direct comparisons of dependent function types
Revert: Special treatment of dependent functions in TypeComparer
change test
Also treat explicit capturing type arguments as boxed
Print subcapturing steps in -explain traces
Don't decorate type variables with additional capture sets
Boxed CapturingTypes
Drop unsound capture suppression if expected type is boxed
If expected type is boxed, the expression still contributes to the captured
variables of its environment.
Re-infer result types of anonymous functions
Keep erased implicit args
Special treatment of dependent functions in TypeComparer
Fix addFunctionRefinements
Always print refined function types as dependent functions.
Makes it easier to see what goes on.
Make CaptureSet ++ and ** simplify more
Refine function types when reinferring so that they can be dependent
Fix avoidance problem when typing blocks
We should not pass en expected type when rechecking the expression
of a block since that can add local references to global capture set variables.
Also: tests for lists and pairs
Print empty variables with "?"
Fix printing untyped annotations
Fix printing annotations in trees
Drop redundant code
Refactor map operations on capture sets
Intoduce Bi-Mapped CaptureSets
Report an error is a simply mapped capture set gets new elements that do not come
from the original souurce. Introduce a new abstraction of bi-mapped sets that accept
new elements and propagate them to the original source.
Add map operation to SimpleIdentitySet
Restrict tracked class parameters to vals
Handle local classes and secondary constructors
Fix CapturingType precedence when printing
First stab at handling classes
Bug fixes
1. Fix canBeTracked for TermRefs
only TermRefs where prefix is NoPrefix or `this` can be tracked. The
others have to be widened.
2. Fix rule for comparing capture refs on the left
3. Be more careful where comparisons are frozen
Capture checker for functions
- Mutable variables have boxed types, so that we do not need to track them when computing capture sets of classes. - Mutable variable types cannot capture `*` in order to prevent scope extrusion.
Scope extrusion can also happen for nested types, so we need to prevent
{*} capturesets anywhere in the type of a mutable variable.
Consider the lazylists.scala test in pos-custom-args/captures:
```scala
class CC
type Cap = {*} CC
trait LazyList[+A]:
this: ({*} LazyList[A]) =>
def isEmpty: Boolean
def head: A
def tail: {this} LazyList[A]
object LazyNil extends LazyList[Nothing]:
def isEmpty: Boolean = true
def head = ???
def tail = ???
extension [A](xs: {*} LazyList[A])
def map[B](f: {*} A => B): {xs, f} LazyList[B] =
class Mapped extends LazyList[B]:
this: ({xs, f} Mapped) =>
def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f) // OK
new Mapped
```
Without this commit, the second to last line is an error since the right hand side
has capture set `{xs, f}` but the required capture set is `this`.
To fix this, we widen the expected type of the rhs `xs.tail.map(f)` from `{this}` to
`{this, f, xs}`. That is, we add the declared captures of the self type to the expected
type. The soundness argument for doing this is as follows:
Since `tail` does not have parameters, the only thing it could capture are references that the
receiver `this` captures as well. So `xs` and `f` must come via `this`. For instance, if
the receiver `xs` of `xs.tail` happens to be pure, then `xs.tail` is pure as well.
On the other hand, in the neg test `lazylists1.scala` we add the following line to `Mapped`:
```scala
def concat(other: {f} LazyList[A]): {this} LazyList[A] = ??? : ({xs, f} LazyList[A]) // error
```
Here, we cannot widen the expected type from `{this}` to `{this, xs, f}` since the result of concat
refers to `f` independently of `this`, namely through its parameter `other`. Hence, if `ys: {f} LazyList[String]`
then
```
LazyNil.concat(ys)
```
still refers to `f` even though `LazyNil` is pure. But if we would accept the definition of `concat`
above, the type of `LazyNil.concat(ys)` would be `LazyList[String]`, which is unsound.
The current implementation widens the expected type of class members if the class member does not
have tracked parameters. We could potentially refine this to say we widen with all references in
the expected type that are not subsumed by one of the parameter types.
## Changes:
### Refine rule for this widening
We now widen the expected type of the right hand side of a class member as follows:
Add all references of the declared type of this that are not subsumed by a capture set
of a parameter type.
### Do expected type widening only in final classes
Alex found a counter-example why this is required. See map5 in
neg-customargs/captures/lazylists2.scala
1. Allow `->` and `?->` and function operators, treated like `=>` and `?=>`.
2. under -Ycc treat `->` and `?->` as immutable function types, whereas `A => B`
is an alias of `{*} A -> B` and `A ?=> B` is an alias of `{*} A ?-> B`.
Closures are unaffected, we still use `=>` for all closures where they are pure or not.
Improve printing of capturing types
Avoid explicit retains annotations also outside phase cc
Generate "Impure" function aliases
For every (possibly erased and/or context) function class
XFunctionN, generate an alias ImpureXFunctionN in the Scala package defined as
type ImpureXFunctionN[...] = {*} XFunctionN[...]
Also:
- Fix a bug in TypeComparer: glb has to test subCapture in a frozen state
- Harden EventuallyCapturingType extractor to not crash on illegal capture sets
- Cleanup transformation of inferred types
- Fix rebase breakage - weaken test in TreePickler that was introduced in the meantime since the last rebase (this one needs follow up) - adapt to latest restrictions on rhs of erased definitions
Propagate capture sets to the right in curried functions. Example:
{x} A -> B -> C
is a shorthand for
{x} A -> {x} B -> C
or:
(x: {*} A) -> B -> C
is a shorthand for
(x: {*} A) -> {x} B -> C
or:
({*} A) -> B -> C
is a shorthand for
(x$0: {*} A) -> {x$0} B -> C
Also: allow empty capture sets in types
This gives a more convenient override to disable capture set propagation
in curried types than wrapping in a type alias. E.g. compare
{x} A -> {} B -> C
with
{x} A -> Protect[B -> C]
where
type Protect[X] = X
Also: refactoring to move setup code from Rechecker and CheckCaptures into a joint
class cc.Setup.
As discussed in the CC meeting on 21 Jan 2022
1. Infrastructure to deal with capturesets in byname parameters
2. Handle retainsByName annotations in ElimByName
Convert them to regular annotations on the generated function types.
This enables capture checking on by-name parameters.
3. Add a style warning for misleading by-name parameter type formatting.
By-name types should be formatted `{...}-> T`. `{...} -> T` looks too much
like a function type.
1. Make CanThrow a @capability class 2. Fix pure arrow handling in parser 3. Avoid misleading type mismatch message 4. Make map and filter conserve Const capturesets if there's no change 5. Expand $throws clauses to context function types 6. Exempt compiletime.erasedValue for "no '*'" checks 7. Capability escape checking for try
Map regular function types to impure function types when unpickling a class under -Ycc that was not itself compiled with -Ycc.
Reject root captures by considering unbox operations. This allows us to ignore root captures buried under type applications.
The following two rules replace scala#13657: 1. Exploit capture monotonicity in the apply rule, as discussed in scala#14387. 2. A rule to make typing nested classes more flexible as discussed in scala#14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
odersky
force-pushed
the
change-this-rules
branch
from
9a3f60d to
4cc8ff0
Compare
odersky
added
the
cc-experiment
Make it the formal type rather than the actual one. This avoids messing up capture annotations.
odersky
force-pushed
the
change-this-rules
branch
from
ac14dcd to
fedd8f2
Compare
Required exeption capability references are now preserved beyond typer in type ascriptions, so that they can be checked for escapes.
odersky
force-pushed
the
cc-experiment
branch
from
90fa052 to
775806b
Compare
|
This was incorporated into #14443 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The following two rules replace #13657:
There's also a bug fix where we now enforce a previously missing subcapturing relationship
between the capture set of parent of a class and the capture set of the class itself. Clearly
a class captures all variables captured by one of its parent classes.