RequirementMachine: Preliminary support for superclass and concrete type requirements #37962
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
slavapestov
force-pushed
the
requirement-machine-concrete-types
branch
from
d8e0665 to
aa6e614
Compare
|
@swift-ci Please smoke test |
|
@swift-ci Please test source compatibility |
3 similar comments
|
@swift-ci Please test source compatibility |
|
@swift-ci Please test source compatibility |
|
@swift-ci Please test source compatibility |
…an assert When a protocol's requirement signature is being computed by GenericSignatureBuilder::computeGenericSignature(), we call checkGenericSignature(), which contains various assertions that call GenericSignature::isCanonicalTypeInContext(). One of these assertions forgot to pass the GSB instance down as the 'builder' parameter. The end result is that we would create a new GSB from the protocol's requirement signature, which is generally not well-formed since it does not have a conformance requirement on 'Self'. It seems this was harmless, other than the wasted CPU cycles, but it was caught by some RequirementMachine assertions.
…nside the request type
If we delete a rule because it's left hand side can be reduced using a newly-added rule, we still have to check for overlap between the deleted rule and all other rules. Remove the "is deleted" checks when removing a rule pair from the worklist, and instead, perform the check when adding the potential overlaps from a new rule to the worklist. Also, add some print debugging statements to the completion procedure, enabled when RewriteSystem::DebugCompletion is set to true (which for now at least, requires a recompilation).
The 'associated type merging' hack is a more general form of this.
MutableTerm will be used for temporaries; I'm going to add a new Term type for uniqued permanently-allocated terms shortly.
Unlike Atoms, this a new type that exists alongside MutableTerm (what used to be just Term). For now, nothing uses Term yet.
Previously if the left hand side of two rules overlapped, we would compute the overlapped term and apply both rules to obtain a critical pair. But it is actually possible to compute the critical pair directly. For now this has no effect other than possibly being more efficient, but for concrete type terms we will need this formulation for the completion procedure to work.
slavapestov
force-pushed
the
requirement-machine-concrete-types
branch
from
aa6e614 to
336fa00
Compare
|
@swift-ci Please smoke test |
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.
Add new kinds of atoms representing superclass and concrete type requirements, and generate rewrite rules from these requirements when they appear in a generic signature.
Conceptually, we want to represent a concrete type requirement
T == Foo<Int, Y.Z>as a rewrite rule:What we really want is for the arguments to the type constructor
Foo<>to be a mix of other concrete types or rewriting terms (in this case,Int' andY.Z), but we can't squeeze that into the representation ofType`, and defining a parallel set of type constructors for all parametrizable types would not be feasible (not only do we have bound generic types, but also function types with varying levels of complexity, metatypes, tuples, ...).The solution I came up with is to replace each subterm with a fresh generic parameter. All of these generic parameters have a depth of 0 and an index into a "substitution list" which is an array of terms. So in reality,
[concrete: Foo<Int, Y.Z>]is stored as follows:This PR adds some support for these atoms in the completion procedure. Namely, when computing an overlap, if we have two rules
TU -> XandUV -> YandVends with a superclass or concrete type atom, we prependTto the concrete substitutions in the atom.However, there is another missing step that is coming in the next PR: unification of type constructor arguments when the same type is subject to multiple superclass or concrete type requirements.