The implementation of Knuth-Bendix completion has had a subtle
bookkeeping bug since I first wrote the code in 2021.
It is possible for two rules to overlap in more than one position,
but the ResolvedOverlaps set was a set of pairs (i, j), where
i and j are the index of the two rules. So overlaps other than
the first were not considered. Fix this by changing ResolvedOverlaps
to a set of triples (i, j, k), where k is the position in the
left-hand side of the first rule.
The end result is that we would incorrectly accept the protocol M3
shown in the test case. I'm pretty sure the monoid that M3 encodes
does not have a complete presentation over any alphabet, so of
course it should not be accepted here.
The concrete nesting limit, which defaults to 30, catches
things like A == G<A>. However, with something like
A == (A, A), you end up with an exponential problem size
before you hit the limit.
Add two new limits.
The first is the total size of the concrete type, counting
all leaves, which defaults to 4000. It can be set with the
-requirement-machine-max-concrete-size= frontend flag.
The second avoids an assertion in addTypeDifference() which
can be hit if a certain counter overflows before any other
limit is breached. This also defaults to 4000 and can be set
with the -requirement-machine-max-type-differences= frontend flag.
This basically undoes 3da6fe9c0d, which in hindsight was wrong.
There were no other usages of TypeArrayView anywhere else except for
GenericSignature::getGenericParams(), and it was almost never what
you want, so callers had to convert back and forth to an ArrayRef.
Remove it.
Reformatting everything now that we have `llvm` namespaces. I've
separated this from the main commit to help manage merge-conflicts and
for making it a bit easier to read the mega-patch.
This is phase-1 of switching from llvm::Optional to std::optional in the
next rebranch. llvm::Optional was removed from upstream LLVM, so we need
to migrate off rather soon. On Darwin, std::optional, and llvm::Optional
have the same layout, so we don't need to be as concerned about ABI
beyond the name mangling. `llvm::Optional` is only returned from one
function in
```
getStandardTypeSubst(StringRef TypeName,
bool allowConcurrencyManglings);
```
It's the return value, so it should not impact the mangling of the
function, and the layout is the same as `std::optional`, so it should be
mostly okay. This function doesn't appear to have users, and the ABI was
already broken 2 years ago for concurrency and no one seemed to notice
so this should be "okay".
I'm doing the migration incrementally so that folks working on main can
cherry-pick back to the release/5.9 branch. Once 5.9 is done and locked
away, then we can go through and finish the replacement. Since `None`
and `Optional` show up in contexts where they are not `llvm::None` and
`llvm::Optional`, I'm preparing the work now by going through and
removing the namespace unwrapping and making the `llvm` namespace
explicit. This should make it fairly mechanical to go through and
replace llvm::Optional with std::optional, and llvm::None with
std::nullopt. It's also a change that can be brought onto the
release/5.9 with minimal impact. This should be an NFC change.
Note the test cases in abstract_type_witnesses used to pass but are now
rejected. This is fine, because doing anything more complicated used to
crash, and the GSB would crash or misbehave with these examples.
Preserves concrete type rules on associated types that were derived
from rules indirectly formed from protocol typealias rules.
That is, if you have a pair of rules in another minimization domain:
[P].A.[concrete: C] => [P].A
[Q:T].[P] => [Q:T]
Then completion will introduce a new rule:
[Q:T].A.[concrete: C] => [Q:T].A
Since this rule is outside of our minimization domain, we don't record
a rewrite loop for it, and it will never become redundant.
Now if we have a rule in our own minimization domain:
T.[Q:T].A => T.[Q:U]
Then we get a new rule:
T.[Q:U].[concrete: C] => T.[Q:U]
Make sure we keep this rule around on account of it being derived from
([Q:T].A.[concrete: C] => [Q:T].A).
initialization of the rewrite system.
Instead, the rewrite system can determine trivially redundant requirements
by finding structural requirements with no associated rewrite rules.
rules in a separate pass after homotopy reduction.
RewriteSystem::propagateExplicitBits was too eager in propagating
IDs from explicit rules within rewrite loops, which resulted in bogus
redundancy warnings when the canonical form of an explicit rule was
given a different requirement ID. Instead, propagate requirement IDs
after homotopy reduction when redundant rules are computed and rewrite
loops are simplified.
rewrite system.
This ID can be used to index into the WrittenRequirements array in the
rewrite system to retrieve the structural requirement, e.g. for the
purpose of diagnostics.
Consider this example:
protocol P : C {}
class C : P {}
<T where T : P>
The GenericSignatureBuilder thinks the minimized signature is
<T where T : P>. The RequirementMachine would minimize it down to
<T where T : C>. The latter is more correct, since the conformance
here is concrete and no witness table needs to be passed in at
runtime, however for strict binary compatibility we need to produce
the same signature as the GenericSignatureBuilder.
Accomplish this by changing the minimal conformances algorithm to
detect "circular concrete conformance rules", which take the form
[P].[concrete: C : Q]
Where Q : P. These rules are given special handling. Ordinarily a
protocol conformance rule is eliminated before a concrete conformance
rule; however concrete conformances derived from circular
conformances are considered to be redundant from the get-go,
preventing protocol conformances that can be written in terms of
such concrete conformances from themselves becoming redundant.
Fixes rdar://problem/89633532.
We want to prefer explicit rules when an explicit rule and non-explicit
rule conflict. Since the explicit bit hasn't been computed yet when
building the property map, save conflicting rule pairs in a side table,
and then process them later in homotopy reduction.
The side table will also be useful for diagnostics later.
Now that the PropertyMap to the concrete simplification version is optional,
we can just pass nullptr here to get the old behavior where type terms are
simplified to canonical anchors and no concrete simplification is performed.
Now that we can detect protocol typealias rules, collect and keep
track of them so that they can be recorded in protocol requirement
signatures.
For now, this is all NFC since nothing introduces such rules into
the rewrite system, except for invalid requirements which are
diagnosed anyway.
There are two kinds of protocol typealiases:
1) The underlying type is a type parameter. These rules look like
[P].A => X where X is the underlying type.
2) The underlying type is a concrete type. These rules look like
[P].A.[concrete: C] => [P].A.
The isProtocolTypeAliasRule() predicate detects both cases and
returns the type alias name ('A', in the above examples). For now
it's not used anywhere, since we don't actually introduce these
rules for any reason.
