Upcasts for access-permissions on strict supertypes#106
Draft
pawinkler wants to merge 2 commits intopaul/interface-permissionsfrom
Draft
Upcasts for access-permissions on strict supertypes#106pawinkler wants to merge 2 commits intopaul/interface-permissionsfrom
pawinkler wants to merge 2 commits intopaul/interface-permissionsfrom
Conversation
Add an `Upcast` expression embedding (TypeOp.kt) that, when linearized, unfolds the shared-predicate hierarchy between a concrete subtype and an expected supertype. Replace the old `withType` calls at return/branch sites in `Linearizer` with `withUpcast`, and implement `applyUnfolding` on `LinearizationContext` (with specialized overrides in `Linearizer`, `PureFunBodyLinearizer`, and a throwing override in `PureExpLinearizer`). `NonInlineNamedFunction.insertCall` wraps each argument with `withUpcast` before the call. Add tests: `conditional_subtype_passing` (verification/classes) and `pure_upcast` (verification/pure_functions). Co-Authored-By: Claude Sonnet 4.6 (1M context) <noreply@anthropic.com>
…which is an open problem
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
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.
Summary
This PR was extracted from #92 and is based on #105. It concerns the implementation of a new
Upcastembedding. It allows us to detect an implicit upcast from a subtype to a strict supertype at the conversion level. The upcasts can then be used in the linearizers to unfold the access-permissions accordingly, so that the the supertype and its fields can be accessed. This is necessary in certain situations, such as when a functions expects a strict supertype of an argument's type. Without the additional unfolds, the held permissions would only include the subtype, not the supertype. Creating a new embedding allows us to split concerns nicely between the conversion and the encoding layer.Changes
Upcastexpression embedding (TypeOp.kt) that, when linearized, unfoldsthe shared-predicate hierarchy between a concrete subtype and an expected supertype.
unfoldstatements (previously injected at method/functioncall sites and assignments) with a uniform expression-level mechanism driven by
withUpcast.applyUnfoldingtoLinearizationContextwith specialized implementations inLinearizer(emitsStmt.Unfold) andPureFunBodyLinearizer(registers predicates on anSSA variable for
SsaConverter);PureExpLinearizerthrows since SSA is required.Special Considerations
Nullability
Stmt.If/ ternary)Type cast operators
as) — produces aCastembedding; type is already the target, no upcast neededas?) — the then-branch stores the receiver (supertype) into the cast result(subtype), which is the wrong direction for
Upcast; unfolding is missingSpecification contexts
@Purefunction preconditions / postconditions —PureExpLinearizer.applyUnfoldingthrows; requires SSA support that this linearizer does not have