Pr15768 #17
Open
Pr15768 #17
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.
Make it the formal type rather than the actual one. This avoids messing up capture annotations.
Required exeption capability references are now preserved beyond typer in type ascriptions, so that they can be checked for escapes.
To circumvent the restriction and to allow class refinements as inferred types we temporarily make class parameters public during phase CheckCaptures.
The self type of a class must include: - any references to capabilities outside the class - the capture sets of its retained parameters We now infer the capture set of the self type if an explicit self type is missing.
If the expected formals are pure, so should be the function parameters.
Fixes and refinements needed to compile a full collection strawman and tests with
capture checking turned on.
1. Exclude ResetPrivate symbols from overriding checks
A symbol with the ResetPrivate flag should not take part in overriding checks.
We have reset the Private just to enable refinements, but for the purpose
of overriding checks it still should be treated as a private member.
2. Refine conforms check
The previous check did not work if the whole right hand side was a tracked
variable. We now have a more robust check that works by augmenting the
expected capture set rather than filtering the actual one.
3. Keep self type around after FirstTransform
Under -Ycc we need to keep the self type declaration until CheckCaptures, so that
it can be checked for well-formedness. We can't keep the original self (which is
a ValDef) since other phases assume it is empty after FirstTransform. Instead we
copy the type `S` into a synthetic definition
private[this] type $this = S
4. Exclude some synthetic case class methods from checking, since their implementations
do not allow for capture sets. We need to get back to them eventually, and annotate the
methods in the correct way.
5. Handle function type aliases in preTypeArgs
6. Fixes for handling capture set ranges
- We now accept `C[? >: C1 T1 <: C2 T2]` even if `C` is higher-kinded.
Previously we widened the range to Nothing...Any.
- Special case for handling the subtype test `C[? >: C1 T1 <: C2 T2] <: C3 T3`
where `T1 =:= T2`: Unify capture sets C1, C2 and C3 in this case.
7. Refine inferred variable scheme
- More refined model when a type gets an inferred variable.
- Add inferred variables to pattern matching lets
8. A version of collection strawman that uses abstract types
A version of the collection strawman that uses abstract types instead of
type parameters for `Repr` and `C[_]`. This is necessary since we want to
use `this` in the capture set of some of these types.
Checking against capturing the universal capability now works also for inferred types. Also fix breakage from previous rebase
Allow references to local class parameters in capture sets of public members. These would have been classified as escaping private references before.
1. Fix nonDependentResultApprox. The previous code would unncessessarily widen covariant occurrences to `*`. 2. Add handling of cases like SingletonType <:< CapturingType. 3. Propagate element additions in a AvoidMapped variable back to source
Avoid the unsoundness in the previously used technique
Co-authored-by: Ondřej Lhoták <olhotak@uwaterloo.ca>
Synthetic apply and copy methods of case classes as well as copy default getters have inferred types that do not correctly convey capture information before phase CC. To allow for separate compilation, we have to fix the types of these methods in a denotation transformer, and then fix them back after CC. Also: Explicit type for unapply - Tighten condition on ignored definitions - Implement avoidance for return expressions
Note: using `accountsFor` criterion would be too pessimistic and therefore underapproximates elements of intersections, which means soundness would be lost. We now overapproximate with `mightAccountFor`, at a possible loss of completeness.
1. Make box insertion functional; don't rely on side effects. This
causes neg.../bounded.scala to break, which is fixed by the other
two points. (bounded.scala already was wrong before if the type
variable X was unbounded).
2. Insert boxes for function results.
3. Propagate boxed captures to the left in function types.
4. Drop CapturingKind, use a boolean for `boxed` and factor out
by-nameness in a separate mechanism.
Use either the qualifier type or the result type depending on a pre-check using a new method `mightSubcapture`.
Allow impure arguments
1. Update info of TypeDef symbols to account for boxing. Previously, the
changes were made to the tree, but were not propagated to the symbol.
2. Maintain alias types when adding boxes.
3. Don't accidentally widen in addResultBoxes. The boxmap pos test started
failing after (1), (2) before the fix (3) was added.
Fixes scala#15749
It's a necessary measure to diagnose mishandlings of boxes faster.
This required a change in `lists.scala`, where capture sets buried to the right had to be repeated on the whole type. I believe there is no desugaring yet that would do these things automatically.
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.
No description provided.