RequirementMachine: Improved handling of "identity conformances" [P].[P] => [P]

[slavapestov]

This is just a big yak shave to get a pathological protocol definition by @jckarter to minimize correctly:

protocol O {
   associatedtype R : O
   associatedtype C : O
     where C.C.C.C == Self,
           C.C.R.C.C.R == Self,
           R.C.R.C.R.C == Self
 }

The correct minimized signature here is

<Self where Self == Self.C.C.C.C, Self.C : O, Self.R : O, Self.C.C == Self.R.C.C.R, Self.C.R.C == Self.R.C.R>

While getting it to work, I uncovered some related issues, and fixed a few other bugs in the process.

Motivation

Consider this example:

protocol P {
  associatedtype X : P where X == Self
}

Clearly the conformance requirement X : P is redundant (and the GenericSignatureBuilder agrees), but previously nothing in the requirement machine's theory would make it so.

Here is the rewrite system:

(1) [P:X].[P] => [P:X]
(2) [P:X] => [P]

These two terms overlap on [P:X].[P]; resolving the critical pair introduces the 'identity conformance' [P].[P] => [P]. Homotopy reduction would delete this conformance, but at this point, [P:X].[P] => [P:X] would no longer be redundant, since nothing else proves that [P].[P] => [P].

Now, [P].[P] => [P] is a permanent rule, and we can handle this properly; any conformance that appears in a rewrite loop together with an identity conformance without context is completely redundant; it is equivalent to the empty generating conformance path.

The concrete type problem

However, this revealed a weakness in how completion handles concrete type substitutions. Suppose we have these rules:

(1) [P].[P] => [P]
(2) [P].[P:X] => [P:X]
(3) [P].[P:Y] => [P:Y]
(4) [P:X].[concrete: G<τ_0_0> with <[P:Y]>]

Rule (2) and (4) overlap on the following term, which has had the concrete type adjustment applied, transforming [P:Y] into [P].[P:Y] by prepending the prefix [P]:

[P].[P:X].[concrete: G<τ_0_0> with <[P].[P:Y]>]

The critical pair is obtained by applying rule (2) to both sides of the branching is

[P:X].[concrete: G<τ_0_0> with <[P].[P:Y]>] => [P:X]

Note that this is a distinct rule from (4), and again this new rule overlaps with (2), producing another rule

[P:X].[concrete: G<τ_0_0> with <[P].[P].[P:Y]>] => [P:X]

This process doesn't terminate. The root cause of this problem is the existence of rule (1).

To make this work, we need to simplify concrete substitutions when adding a new rule in completion.

The solution

We need to simplify concrete substitutions when adding a rewrite rule, so for example if X.Y => Z, we want to simplify

A.[concrete: G<τ_0_0, τ_0_1> with <X.Y, X>] => A

to

A.[concrete: G<τ_0_0, τ_0_1> with <Z, X>] => A

The requirement machine used to do this, but I took it out, because it didn't fit with the rewrite path representation. Until now, a rewrite path was a composition of rewrite steps where each step would transform a source term into a destination term.

The question then becomes, how do we represent concrete substitution simplification with such a scheme.

One approach is to rework rewrite paths to a 'nested' representation, where a new kind of rewrite step applies a sequence of rewrite paths to the concrete substitution terms. Unfortunately this would complicate memory management and require recursion when visiting the steps of a rewrite path.

Another, simpler approach that I'm going with here is to generalize a rewrite path to a stack machine program instead.

I'm adding two new kinds of rewrite steps which manipulate a pair of stacks, called 'A' and 'B':

• Decompose, which takes a term ending in a superclass or concrete type symbol, and pushes each concrete substitution on the 'A' stack.

• A>B, which pops the top of the 'A' stack and pushes it onto the 'B' stack.

Since all rewrite steps are invertible, the inverse of the two new step kinds are as follows:

• Compose, which pops a series of terms from the 'A' stack, and replaces the concrete substitutions in the term ending in a superclass or concrete type symbol underneath.

• B>A, which pops the top of the 'B' stack and pushes it onto the 'B' stack.

Both Decompose and Compose take an operand, which is the number of concrete substitutions to expect. This is encoded in the RuleID field of RewriteStep.

The two existing rewrite steps ApplyRewriteRule and AdjustConcreteType simply pop and push the term at the top of the 'A' stack.

Now, if addRule() wishes to transform

A.[concrete: G<τ_0_0, τ_0_1> with <X.Y, X>] => A

into

A.[concrete: G<τ_0_0, τ_0_1> with <Z, X>] => A

it can construct the rewrite path

Decompose(2) ⊗ A>B ⊗ <<rewrite path from X.Y to Z>> ⊗ B>A ⊗ Compose(2)

The existing 'evaluation' walks over rewrite paths that used to mutate a single MutableTerm now use a new RewritePathEvaluator type, that stores the two stacks. The definition of a rule appearing "in empty context" for homotopy reduction's purposes is now narrower; in addition to the rewrite step having empty whiskers, the evaluator at this point must also have an 'A' stack consisting of exactly one entry, and an empty 'B' stack.

[slavapestov]

@swift-ci Please smoke test

[slavapestov]

@swift-ci Please smoke test