RewriteSystem::addRule() did two things before adding the rewrite rule:
- Simplify both sides. If both sides are now equal, discard the rule.
- If the last symbol on the left hand side was a superclass or concrete type
symbol, simplify the substitution terms in that symbol.
The problem is that the second step can produce a term which can be further
simplified, and in particular, one that is exactly equal to the left hand
side of some other rule.
To fix this, swap the order of the two steps. The only wrinkle is now we
have to check for a concrete type symbol at the end of _both_ the left hand
side and right hand side, since we don't orient the rule until we simplify
both sides.
I don't have a reduced test case for this one, but it was revealed by
compiler_crashers_2_fixed/0109-sr4737.swift after I introduced the trie.
protocol Q {
associatedtype T where T == Self?
}
func foo<X, Y : Q>(_: X, _: Y) {}
This generates the rewrite system
[Q:T].[concrete: Optional<τ_0_0> with <[Q]>]
τ_0_1.[Q] => τ_0_1
With this property map:
[Q:T] => { [concrete: Optional<τ_0_0> with <[Q]>] }
τ_0_1 => { [Q] }
Suppose we're resolving the concrete type τ_0_1.[Q:T]. The property map
entry is keyed by [Q:T], so the prefix τ_0_1 must be prepended to the
concrete substitutions of [concrete: Optional<τ_0_0> with <[Q]>].
However, [Q] is just the protocol Self type, and τ_0_0.[Q] is not a
valid type-like term. We could simplify the term before building the
Swift type which would apply the second rewrite rule, but it's easier
to just drop the protocol symbol in this case.
Just as with concrete types, if we find that the same suffix has two
different superclass symbols in the property map, we need to introduce
same-type requirements between their generic parameters.
The added wrinkle is that the classes might be different; in this case,
one must be a superclass of the other, and we repeatedly substitute
the generic arguments until we get the generic arguments of the
superclass before we unify.
Also, introduce the layout requirement implied by a superclass requirement
when lowering requirements, instead of when building the property map.
Right now this is functionally equivalent, but if we ever start to
test properties by checking for joinability of T with T.[p] instead of
looking at the property map entry of T, this new formulation is the
right one.
The property map stores the concrete type or superclass bound for all
terms whose suffix is equal to some key, so eg if you have
protocol P {
associatedtype T where T == U?
associatedtype U
}
Then you have this rewrite system
[P].T => [P:T]
[P].U => [P:U]
[P:T].[concrete: Optional<τ_0_0> with <[P:U]>] => [P:T]
Which creates this property map
[P:T] => { [concrete: Optional<τ_0_0> with <[P:U]>] }
Now if I start with a generic signature like
<T, U where U : P>
This produces the following rewrite system:
τ_0_1.[U] => τ_0_1
τ_0_1.T => τ_0_1.[P:T]
τ_0_1.U => τ_0_1.[P:U]
Consider the computation of the canonical type of τ_0_1.T. This term
reduces to τ_0_1.[P:T]. The suffix [P:T] has a concrete type symbol in
the property map, [concrete: Optional<τ_0_0> with <[P:U]>].
However it would not be correct to canonicalize τ_0_1.[P:T] to
Optional<τ_0_0>.subst { τ_0_0 => getTypeForTerm([P:T]) }; this
produces the type Optional<τ_0_0.T>, and not Optional<τ_0_1.T> as
expected.
The reason is that the substitution τ_0_0 => getTypeForTerm([P:T])
is "relative" to the protocol Self type of P, since domain([P:T]) = {P}.
Indeed, the right solution here is to note that τ_0_1.[P:T] has a suffix
equal to the key of the property map entry, [P:T]. If we strip off the
suffix, we get τ_0_1. If we then prepend τ_0_1 to the substitution term,
we get the term τ_0_1.[P:U], whose canonical type is τ_0_1.U.
Now, applying the substitution τ_0_0 => τ_0_1.U to Optional<τ_0_0>
produces the desired result, Optional<τ_0_1.U>.
Note that this is the same "prepend a prefix to each substitution of
a concrete type symbol" operation that is performed in checkForOverlap()
and PropertyBag::copyPropertiesFrom(), however we can simplify things
slightly by open-coding it instead of calling the utility method
prependPrefixToConcreteSubstitutions(), since the latter creates a
new symbol, which we don't actually need.
If you have
protocol P {
associatedtype T
}
class C<T> : P {}
Then substituting the type parameter T.T from the generic signature
<T where T : P> into the generic signature <T, U where T : C<U>>
is the identity operation, and also returns T.T, because subst()
isn't smart enough to replace T.T with U.
So getCanonicalTypeInContext() has to do the concrete conformance
lookup here, just like it does for the analogous situation where
you have a concrete type requirement.
This could be solved in a more principled way by better book-keeping
elsewhere, but the GSB supported the old behavior, so we can
simulate it easily enough in the RequirementMachine also.
Start treating the null {Can}GenericSignature as a regular signature
with no requirements and no parameters. This not only makes for a much
safer abstraction, but allows us to simplify a lot of the clients of
GenericSignature that would previously have to check for null before
using the abstraction.
This is just a straight port of the existing code in the GSB, with minimal changes.
It could be made more efficient in the future by trafficking in Terms rather than
Types, avoiding some intermediate conversion and canonicalization steps.
If we have something like this:
protocol P { associatedtype A : P }
class C<U> : P { typealias A = C<U> }
<T where T : P, T : C<U>>
Then we would add a rewrite T.A => T because both the concrete type
was equal to the type witness. But that is only valid if the original
requirement is a concrete type requirement, not a superclass requirement.
If two equivalence classes have the same concrete type and the
concrete type does not have any concrete substitutions, they are
essentially equivalent. Take advantage of this by introducing
same-type requirements to existing type witnesses where possible.
Intuitively, the first token of a rewrite rule determines if the rule
applies to a protocol requirement signature 'Self', or a generic
parameter in the top-level generic signature. A rewrite rule can never
take a type starting with the protocol 'Self' to a type starting with a
generic parameter, or vice versa.
Enforce this by defining the notion of a 'domain', which is the set of
protocols to which the first atom in a term applies to. This set can be
empty (if we have a generic parameter atom), or it may contain more than
one element (if we have an associated type atom for a merged associated
type).
ProtocolConformance::getTypeWitness() can return a null Type in case of
circularity. Handle this by replacing it with an ErrorType to match
the behavior of the GSB.
This more closely matches the existing behavior of the GSB, where
conflicts are diagnosed but we don't drop all concrete type
requirements on that type parameter altogether.
If an equivalence class has protocol conformance requirements together with a
superclass requirement, any protocols to which the superclass conforms might
have nested types that need to be concretized by introducing same-type
requierments between those nested types and the type witnesses in the
concrete conformances of the superclass.
When concretizing nested types, we need to be able to normalize a concrete type
containing DependentMemberTypes to our 'concrete substitution schema' form where
all type parameter structural sub-components are actually just generic parameters.
The logic for handling the abstract type witness case correctly
handles DependentMemberTypes. We want to use this for concrete
type witnesses too, since they might contain type parameters as
structural sub-components.
Store the protocol's direct associated types separately from the inherited
associated types, since in a couple of places we only need the direct
associated types.
Also, factor out a new ProtocolGraph::compute() method that does all the
steps in the right order.
We compute the canonical type by first simplifying the type term, and
then checking if it is a concrete type. If there's no concrete type,
we convert the simplified term back to an interface type and return
that; otherwise, we canonicalize any structural sub-components of
the concrete type that contain interface types, and so on.
Due to a quirk of how the existing declaration checker works, we also
need to handle "purely concrete" member types, eg if I have a
signature `<T where T == Foo>`, and we're asked to canonicalize the
type `T.[P:A]` where Foo : A.
This comes up because we can derive the signature `<T where T == Foo>`
from a generic signature like `<T where T : P>`; adding the
concrete requirement 'T == Foo' renders 'T : P' redundant. We then
want to take interface types written against the original signature
and canonicalize them with respect to the derived signature.
The problem is that `T.[P:A]` is not a valid term in the rewrite system
for `<T where T == Foo>`, since we do not have the requirement T : P.
A more principled solution would build a substitution map when
building a derived generic signature that adds new requirements;
interface types would first be substituted before being canonicalized
in the new signature.
For now, we handle this with a two-step process; we split a term up
into a longest valid prefix, which must resolve to a concrete type,
and the remaining suffix, which we use to perform a concrete
substitution using subst().
If a type parameter has a protocol conformance and a concrete type,
we want to map associated types of the conformance to their concrete
type witnesses.
This is implemented as a post-processing pass in the completion
procedure that runs after the equivalence class map has been built.
If we have an equivalence class T => { conforms_to: [ P ], concrete: Foo },
then for each associated type A of P, we generate a new rule:
T.[P:A].[concrete: Foo.A] => T.[P:A] (if Foo.A is concrete)
T.[P:A] => T.(Foo.A) (if Foo.A is abstract)
If this process introduced any new rules, we check for any new
overlaps by re-running Knuth-Bendix completion; this may in turn
introduce new concrete associated type overlaps, and so on.
The overall completion procedure now alternates between Knuth-Bendix
and rebuilding the equivalence class map; the rewrite system is
complete when neither step is able to introduce any new rules.
Protocol atoms map to the 'Self' parameter; GenericParam and Name
atoms map in the obvious way.
An associated type atom `[P1&P1&...&Pn:A]` has one or more protocols
P0...Pn and an identifier 'A'.
We map it back to a AssociatedTypeDecl as follows:
- For each protocol Pn, look for associated types A in Pn itself,
and all protocols that Pn refines.
- For each candidate associated type An in protocol Qn where
Pn refines Qn, get the associated type anchor An' defined in
protocol Qn', where Qn refines Qn'.
- Out of all the candidiate pairs (Qn', An'), pick the one where
the protocol Qn' is the lowest element according to the linear
order defined by TypeDecl::compare().
The associated type An' is then the canonical associated type
representative of the associated type atom `[P0&...&Pn:A]`.
