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]`.
We used to assert that the merged protocol set was larger than or
equal to in size to both the left hand side and the right hand
side.
However, there is a counter-example:
protocol P {}
protocol Q {}
protocol R : P, Q {}
LHS = [P&Q:T], RHS = [R:T]
The merged atom is `[R:T]` which has fewer protocols than the
left hand side.
If you have a same-type requirement like 'Self.Foo == Self' inside a
protocol P, we add a rewrite rule:
[P].Foo => [P]
Simplification turns this into
[P:Foo] => [P]
Previously, the order was backwards so we would end up with
[P] => [P:Foo]
Which would mess up the conformance information in the equivalence class map.
The `if (other.size() > size())` check was bogus; we can still have an
overlap of the second kind if the other term is longer than this term.
Remove this check, and rewrite the algorithm to be clearer in general.
Also move a all headers other than RequirementMachine.h there, since
I don't expect they will be used outside of the rewrite system
implementation itself.
