A first, incomplete implementation of polyadic capture calculus #18566
Conversation
This file contains hidden or 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
odersky force-pushed the change-root-levels branch from 890a2ba to 0534202 Compare 
This is needed if we want to do setup transforms as part of denotation transformers.
1. Update symbols owner before recursing to children, so that new owners taking account of try block owners are installed. 2. Query owner chaines at phase checkCpatures when computing enclosing level owners.
I tried several other strategies, but nothing worked. - update after Setup: This means we cannot to levelOwner during setup. - running levelOwner after Setup causes CyclicErrors when transforming symbols in Setup - having a seperate notion of ccOwner maintained in a CCState table does not work since there are too many hidden uses of owner everywhere that would ignore that table.
(except if they are updated). This is the first step towards converting to capturing types in SymTransformer, where we have the context.
Need to copy the denotation, since denotations come with next pointers which would get scrambled otherwise.
Makes things more regular and allows for a non-identity mapping between declared types and infos of vals.
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).
Widen singleton types when instantiating local roots in checkConforms
Don't force info when checking whether something is a root capability while printing
Refactor everything so that now vals as well as defs can be level owners
Innstead of traversing old types at postCheck, note what needs to be done when these types are first transformed at Setup.
With the new way to construct capturing types at Setup, we can add the correct boxing annotations there, so the previous unmodular hack can be dropped.
Break out operation to add a single element. This makes widenCaptures redundant.
Avoid the mutable state in CapturSet.Var
# Conflicts: # compiler/src/dotty/tools/dotc/cc/Setup.scala
(Configurable)
odersky force-pushed the change-root-levels branch from e1858db to 2d07bd5 Compare The problem arises if we have a class like the one in pos-custom-args/captures/refs.scala: ```scala class MonoRef(init: Proc): type MonoProc = Proc var x: MonoProc = init def getX: MonoProc = x def setX(x: MonoProc): Unit = this.x = x ``` The type of `getX` and `setX` refer to the local root capability of class `MonoRef`. When we call `m.getX` or `m.setX` in `m: MonoRef`, these occurrences have to be adapted to capture roots in the scope of the selection. We determine these roots by inspecting the capture set of `m` and picking a root that corresponds to it.
odersky changed the title - Drop valsCanBeLevelOwners and levelOwnersNeedCapParam config settings - Drop !isCaseClassSynthetic condition in isLevelOwner - Drop handling of anonymous functions in levelOwnerNamed Neither are needed anymore with the the conflg flags gone.
When comparing refined types C{x: T}^cs <:< C{x: T'}^cs' we need to remember the capture set `cs` on the left hand side when we get to ask whether the refined type has a member `x: T'`, so that we can correctly instantiate any local root `cap[C]` in the member type of `x`. Same if the LHS is simply `C^cs`. In both cases we strip the capture set before we get to take the compute `x`, so we have to re-add it at the point of that member computation. Without that step, class refinements can contain references to the generic root `cap`.
Check that instantiated root variable of a method inside a class is nested in the instance variable of the class. For the moment I was not able to construct a counter example where this makes a difference.
odersky force-pushed the change-root-levels branch from 2e1ed26 to b7d8047 Compare We need to do it for compiled as well as imported types. We only keep adding variables to selftypes of local classes in postProcess. This allows us to drop one occurrence of LooseRootChecking
That's needed since a subclass might be a level owner.
Also: Print local roots with id of owner under -uniqid
The only time a nested object class could have a self type with a non-empty capture set is when it declared in the current compilation unit. Then that capture set is a Var that gets installed via an updateInfo. But then we do also an updateInfo of the module val, so no need to do the same thing in transformSym.
| In the end, after getting everything to compile again, I conclude that the scheme is too complicated to be seriously considered. Mapping So I decided to put this on hold in favor of #18699, which is overall simpler and hopefully more robust. |
odersky added a commit that referenced this pull request Oct 23, 2023
- Start with `sealed` type parameters, extended so that class parameters can also be `sealed`. - Tighten the rules so that type parameter arguments for `sealed` type parameters must themselves be `sealed`, except if the argument is from some outer scope. - Introduce a coercion that maps a universal capture set to a local root that is enclosed by the owners of all free variables of the coerced expression. Supersedes #18566
| Withdrawn in favor of #18699 |
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
1 participant
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.
it's been a big revamp. Most things are in place now.
The major omission is that we currently don't check for level inversion, so there are soundness holes. We know how to do it in principle, but it will be some work to push an implementation through.