Rewrite constraint resolution fixed-point search can be exponential

[danakj]

Rewrite constraint resolution is described here: https://docs.carbon-lang.dev/docs/design/generics/appendix-rewrite-constraints.html#rewrite-constraint-resolution

To find a fixed point, we can perform rewrites on other rewrites, cycling between them until they don’t change or until a rewrite would apply to itself. In the latter case, we have found a cycle and can reject the constraint. Note that it’s not sufficient to expand only a single rewrite until we hit this condition: ...

After constraint resolution, no references to rewritten associated constants remain in the constraints on T.

Given a cycle of rewrite rules that use a tuple, it's trivial to create a cycle that generates exponentially larger types through substitution, such that finding the cycle takes ~infinite time.

A small example, which takes ~9 seconds to complete thanks to only using 6 steps in the cycle, and 2 elements in each tuple:

interface Z {
  let T2:! type;
  let T3:! type;
  let T4:! type;
  let T5:! type;
  let T6:! type;
  let T7:! type;
}


fn F(
    M:! Z where
      .T2 = (.T3, .T3) and
      .T3 = (.T4, .T4) and
      .T4 = (.T5, .T5) and
      .T5 = (.T6, .T6) and
      .T6 = (.T7, .T7) and
      .T7 = (.T2, .T2)
    );

The substitution looks like:

.T2 = (.T3, .T3) -> .T2 = ((.T4, .T4), (.T4, .T4))
.T3 = (.T4, .T4) -> .T3 = ((.T5, .T5), (.T5, .T5))
.T4 = (.T5, .T5) -> .T4 = ((.T6, .T6), (.T6, .T6))
.T5 = (.T6, .T6) -> .T5 = ((.T7, .T7), (.T7, .T7))
.T6 = (.T7, .T7) -> .T6 = ((.T2, .T2), (.T2, .T2))
.T7 = (.T2, .T2) -> .T7 = (((.T4, .T4), (.T4, .T4)), ((.T4, .T4), (.T4, .T4)))

.T2 = ((.T4, .T4), (.T4, .T4)) -> .T2 = ((((.T6, .T6), (.T6, .T6)), ((.T6, .T6), (.T6, .T6))), (((.T6, .T6), (.T6, .T6)), ((.T6, .T6), (.T6, .T6))))
... etc ...

Each time through the rewrite constraints is growing the number of elements in the RHS tuples exponentially. Until it finally writes a reference to the same LHS into a RHS and finds the cycle.

If I take one step out of the cycle, the test completes in about a second, adding another step would take minutes.

(This was found by a fuzzer.)

[danakj]

For this example, limiting the substitutions per rewrite constraint to one on each pass through the rewrite constaints makes this run quickly, as it just replaces one T3, one T4, one T5, one T6, one T7, one T2, one T3, one T4... etc until it finds the cycle.

I am not sure if this is a rigorous solution, but it is effective at not growing the types exponentially here. Maybe we can come up with a counterexample.