Add experimental capture checking #15877
Merged
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
|
@Linyxus I put you down as a reviewer since it might be a good way to get started to work on further improvements, which would come in follow-on PRs. Don't worry if there are things which are unclear for now. But if you spot mistakes and possible improvements please report them in the review. The review is best done by comparing the diffs for all commits together. With 97 commits, it would be hard to review them one-by-one, in particular since later commits often change what was added in earlier commits. If you can only do part of it, that's fine as well. I realize it's a big chunk of work to review more than 8000 lines of code. If others want to chip in, please go ahead! |
Linyxus
reviewed
Aug 26, 2022
| if tp.isBoxed then refs ++ pcs else pcs | ||
| case tp: TypeRef if tp.symbol.isAbstractType => CaptureSet.empty | ||
| case tp: TypeProxy => getBoxed(tp.superType) | ||
| case tp: AndType => getBoxed(tp.tp1) ++ getBoxed(tp.tp2) |
There was a problem hiding this comment.
I am not sure whether this is correct. Should we use ++ for unions and ** for intersections?
There was a problem hiding this comment.
You are right, the two operators must be swapped.
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.
- comments - some refactorings - enable rechecking tests
Rely on auto-boxing when accessing the arguments instead
|
Going to merge now, so that it becomes easier to deal with new issues. |
tgodzik
added a commit
to tgodzik/metals
that referenced
this pull request
Aug 30, 2022
The issues caused by scala/scala3#15877
tgodzik
added a commit
to tgodzik/metals
that referenced
this pull request
Aug 31, 2022
The issues caused by scala/scala3#15877
tgodzik
added a commit
to scalameta/metals
that referenced
this pull request
Aug 31, 2022
The issues caused by scala/scala3#15877
dos65
pushed a commit
to scalameta/metals
that referenced
this pull request
Sep 5, 2022
The issues caused by scala/scala3#15877
tgodzik
reviewed
Sep 13, 2022
| @@ -359,7 +359,6 @@ Text => empty | |||
| Language => Scala | |||
| Symbols => 14 entries | |||
| Occurrences => 30 entries | |||
| Synthetics => 2 entries | |||
There was a problem hiding this comment.
@odersky Why were all those entries removed? Could we revert the changes?
tanishiking
added a commit
to tanishiking/scala3
that referenced
this pull request
Sep 13, 2022
Most of the type apply synthetics have disappeared in scala#15877 because, previously we relies on the `Scala2` flag for filtering out TypeApply synthetics. However, it was hacky, and the capture checking PR makes change on how the compiler put the flags to symbols. As a result, most TypeApply synthetics have disappeared. this commit revives those disappeared type apply synthetics.
bishabosha
added a commit
that referenced
this pull request
Sep 13, 2022
This PR fixes the regressions in SemanticDB's TypeApply synthetics introduced by #15877 - e835dc0 - 097b179 - 097b179 Previously, we relies on `Scala2` flag for filtering out some synthetics, which isn't reliable for SemanticDB (that's why the capture checking made a change in how the compiler put flags to symbols and the regression occurred). This PR fixes the regression by re-implements TypeApply synthetics without using `Scala2` flag. (also fix scalameta/metals#4372) Probably, it makes more sense to compare the `metac.expect`'s diff from 53e1adc which was something before the regression. <details> <summary>diff from 53e1adc</summary> `git diff 53e1adc HEAD tests/semanticdb/metac.expect` ```diff diff --git a/tests/semanticdb/metac.expect b/tests/semanticdb/metac.expect index 5e20650513..2c7f720937 100644 --- a/tests/semanticdb/metac.expect +++ b/tests/semanticdb/metac.expect @@ -50,7 +50,7 @@ Text => empty Language => Scala Symbols => 60 entries Occurrences => 132 entries -Synthetics => 4 entries +Synthetics => 3 entries Symbols: advanced/C# => class C [typeparam T ] extends Object { self: C[T] => +3 decls } @@ -252,7 +252,6 @@ Synthetics: [27:12..27:16):s.s1 => reflectiveSelectable(*) [29:12..29:16):s.s2 => reflectiveSelectable(*) [31:12..31:16):s.s3 => reflectiveSelectable(*) -[47:19..47:24):foo.a => *[foo.A] expect/Annotations.scala ------------------------ @@ -264,7 +263,6 @@ Text => empty Language => Scala Symbols => 23 entries Occurrences => 52 entries -Synthetics => 2 entries Symbols: annot/Alias. => final object Alias extends Object { self: Alias.type => +2 decls } @@ -345,10 +343,6 @@ Occurrences: [39:11..39:26): ClassAnnotation -> com/javacp/annot/ClassAnnotation# [39:28..39:33): param -> scala/annotation/meta/param# -Synthetics: -[25:2..25:20):@throws[Exception] => *[Exception] -[25:2..25:20):@throws[Exception] => *[Exception] - expect/Anonymous.scala ---------------------- @@ -896,7 +890,7 @@ Text => empty Language => Scala Symbols => 181 entries Occurrences => 148 entries -Synthetics => 10 entries +Synthetics => 6 entries Symbols: _empty_/Enums. => final object Enums extends Object { self: Enums.type => +30 decls } @@ -1232,16 +1226,12 @@ Occurrences: [68:25..68:31): Planet -> _empty_/Enums.Planet# Synthetics: -[46:28..46:35):C <:< C => *[C, C] -[49:27..49:31):Refl => *.apply[T] [52:9..52:13):Refl => *.unapply[Option[B]] -[52:19..52:30):opt.flatMap => *[B] [52:31..52:50):identity[Option[B]] => *[Function1[A, Option[B]]] [54:14..54:18):Some => *.apply[Some[Int]] [54:14..54:34):Some(Some(1)).unwrap => *(given_<:<_T_T[Option[Int]]) [54:19..54:23):Some => *.apply[Int] [54:28..54:34):unwrap => *[Some[Int], Int] -[56:52..56:64):Enum[Planet] => *[Planet] expect/EtaExpansion.scala ------------------------- @@ -3165,7 +3155,7 @@ Text => empty Language => Scala Symbols => 52 entries Occurrences => 132 entries -Synthetics => 36 entries +Synthetics => 39 entries Symbols: example/Synthetic# => class Synthetic extends Object { self: Synthetic => +23 decls } @@ -3361,12 +3351,15 @@ Synthetics: [6:2..6:18):Array.empty[Int] => intArrayOps(*) [7:2..7:8):"fooo" => augmentString(*) [10:13..10:24):"name:(.*)" => augmentString(*) +[11:8..11:11):#:: => *.unapply[Int] [11:17..11:25):LazyList => *.apply[Int] [13:4..13:28):#:: 2 #:: LazyList.empty => *[Int] [13:8..13:28):2 #:: LazyList.empty => toDeferrer[Int](*) [13:10..13:28):#:: LazyList.empty => *[Int] [13:14..13:28):LazyList.empty => toDeferrer[Nothing](*) [13:14..13:28):LazyList.empty => *[Nothing] +[15:9..15:12):#:: => *.unapply[Int] +[15:16..15:19):#:: => *.unapply[Int] [15:25..15:33):LazyList => *.apply[Int] [17:14..17:38):#:: 2 #:: LazyList.empty => *[Int] [17:18..17:38):2 #:: LazyList.empty => toDeferrer[Int](*) @@ -3471,7 +3464,7 @@ Text => empty Language => Scala Symbols => 22 entries Occurrences => 46 entries -Synthetics => 7 entries +Synthetics => 11 entries Symbols: example/ValPattern# => class ValPattern extends Object { self: ValPattern => +14 decls } @@ -3546,12 +3539,16 @@ Occurrences: [40:10..40:18): rightVar -> local4 Synthetics: +[5:6..5:10):Some => *.unapply[Int] [6:4..6:8):Some => *.apply[Int] [8:6..8:10):List => *.unapplySeq[Nothing] [8:11..8:15):Some => *.unapply[Nothing] +[11:6..11:10):Some => *.unapply[Int] [12:4..12:8):Some => *.apply[Int] [25:4..25:11):locally => *[Unit] +[27:10..27:14):Some => *.unapply[Int] [28:8..28:12):Some => *.apply[Int] +[31:10..31:14):Some => *.unapply[Int] [32:8..32:12):Some => *.apply[Int] expect/Vals.scala @@ -4264,7 +4261,6 @@ Text => empty Language => Scala Symbols => 36 entries Occurrences => 46 entries -Synthetics => 3 entries Symbols: local0 => type N$1 <: Nat @@ -4352,11 +4348,6 @@ Occurrences: [23:35..23:39): Zero -> recursion/Nats.Zero. [23:40..23:42): ++ -> recursion/Nats.Nat#`++`(). -Synthetics: -[5:50..5:54):Succ => *.apply[Nat.this.type] -[10:13..10:17):Succ => *.unapply[N$1] -[20:11..20:15):Succ => *.unapply[N$2] - expect/semanticdb-Definitions.scala ----------------------------------- ``` </details>
mpollmeier
pushed a commit
to mpollmeier/dotty
that referenced
this pull request
Oct 16, 2022
Most of the type apply synthetics have disappeared in scala#15877 because, previously we relies on the `Scala2` flag for filtering out TypeApply synthetics. However, it was hacky, and the capture checking PR makes change on how the compiler put the flags to symbols. As a result, most TypeApply synthetics have disappeared. this commit revives those disappeared type apply synthetics.
smarter
added a commit
to dotty-staging/dotty
that referenced
this pull request
Jul 14, 2023
The isSubInfo for capture-checking introduced in scala#15877 had the following TODO: // A relaxed version of subtyping for dependent functions where method types // are treated as contravariant. // TODO: Merge with isSubInfo in hasMatchingMember. Currently, we can't since // the isSubinfo of hasMatchingMember has problems dealing with PolyTypes // (---> orphan params during pickling) The orphan params error was due to the recursion on the result of the PolyTypes being done without first calling `compareTypeLambda`. After fixing this we can safely merge the two versions while keeping the new behavior for dependent and polymorphic function types hidden under the `captureChecking` feature since they're language changes. I'll open a separate PR to create a `relaxedSubtyping` feature for these improvements since their usefulness is independent of capture checking. The isSubInfo for capture-checking got two additional cases involving CapturingTypes in 3e690a8, I don't know what they're supposed to do, but moving those to the regular isSubInfo breaks various capture-checking tests: -- [E007] Type Mismatch Error: tests/pos-custom-args/captures/classes.scala:11:32 -------------------------------------- 11 | val c1: C{val n: B^{x}}^{x} = c0 | ^^ | Found: (c0 : C{val n: B^}^{x}) | Required: C{val n: B^{x}}^{x} So this commit breaks capture-checking and I don't know enough about what this code is supposed to do to fix it.
Linyxus
pushed a commit
to dotty-staging/dotty
that referenced
this pull request
Jul 18, 2023
The isSubInfo for capture-checking introduced in scala#15877 had the following TODO: // A relaxed version of subtyping for dependent functions where method types // are treated as contravariant. // TODO: Merge with isSubInfo in hasMatchingMember. Currently, we can't since // the isSubinfo of hasMatchingMember has problems dealing with PolyTypes // (---> orphan params during pickling) The orphan params error was due to the recursion on the result of the PolyTypes being done without first calling `compareTypeLambda`. After fixing this we can safely merge the two versions while keeping the new behavior for dependent and polymorphic function types hidden under the `captureChecking` feature since they're language changes. I'll open a separate PR to create a `relaxedSubtyping` feature for these improvements since their usefulness is independent of capture checking. The isSubInfo for capture-checking got two additional cases involving CapturingTypes in 3e690a8, I don't know what they're supposed to do, but moving those to the regular isSubInfo breaks various capture-checking tests: -- [E007] Type Mismatch Error: tests/pos-custom-args/captures/classes.scala:11:32 -------------------------------------- 11 | val c1: C{val n: B^{x}}^{x} = c0 | ^^ | Found: (c0 : C{val n: B^}^{x}) | Required: C{val n: B^{x}}^{x} So this commit breaks capture-checking and I don't know enough about what this code is supposed to do to fix it.
Linyxus
pushed a commit
to dotty-staging/dotty
that referenced
this pull request
Jul 18, 2023
The isSubInfo for capture-checking introduced in scala#15877 had the following TODO: // A relaxed version of subtyping for dependent functions where method types // are treated as contravariant. // TODO: Merge with isSubInfo in hasMatchingMember. Currently, we can't since // the isSubinfo of hasMatchingMember has problems dealing with PolyTypes // (---> orphan params during pickling) The orphan params error was due to the recursion on the result of the PolyTypes being done without first calling `compareTypeLambda`. After fixing this we can safely merge the two versions while keeping the new behavior for dependent and polymorphic function types hidden under the `captureChecking` feature since they're language changes. I'll open a separate PR to create a `relaxedSubtyping` feature for these improvements since their usefulness is independent of capture checking. The isSubInfo for capture-checking got two additional cases involving CapturingTypes in 3e690a8, I don't know what they're supposed to do, but moving those to the regular isSubInfo breaks various capture-checking tests: -- [E007] Type Mismatch Error: tests/pos-custom-args/captures/classes.scala:11:32 -------------------------------------- 11 | val c1: C{val n: B^{x}}^{x} = c0 | ^^ | Found: (c0 : C{val n: B^}^{x}) | Required: C{val n: B^{x}}^{x} So this commit breaks capture-checking and I don't know enough about what this code is supposed to do to fix it.
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.
This PR merges branch cc-experiment into main. The capture checking language extensions are all under a -Ycc flag. At the present stage, they should be considered highly experimental and unstable.
Nevertheless, I think it makes sense to have capture checking as part of the main branch. It will encourage more experiments and will make it easier to incorporate improvements in a stable manner. Since we will have several new people working on capture checking starting next month, it's a good time to merge now.