[Rigidity]

Closes #170

Problem

compare cached almost nothing inside recursive types. Memo only reuses a result that didn't rely on a comparison still in progress, and inside a cycle nearly every result does. It also turned caching off entirely while a generic function's generics were being instantiated (#140). So the G program from the issue never finished, and intersect's repeated comparisons of the N0/N1 types took most of a second.

What changed

Of the issue's two directions, this takes the first. It keys the cycle check on everything a result depends on, and makes the relaxed reuse rule exact. A "top-level comparison" below means one that starts from an empty stack, which is every call from compare, check, intersect and subtract. Each top-level comparison now runs in one of two modes.

• Fixpoint mode (new FixpointMemo in memo.rs). It applies when all of these hold, which ComparisonContext::is_monotone checks with one walk per side:

  • there's no inference;
  • no binders are in scope;
  • every type reachable from either side is contractive;
  • every generic function type's parameters and return type either are one of its generics or don't reference them.

  Here a result is cached even if it relied on comparisons in progress, together with those comparisons. It's reused while they're all still on the stack. This is what makes G fast.

• Exact mode. Otherwise the existing Memo is used unchanged. It now also caches comparisons that happen while a generic function is being instantiated, as long as the comparison's own key doesn't refer to a generic being instantiated. Before, nothing was cached in that case.

• The cycle check's stack key now includes the semantics passed down (it already included the binder pattern), so a comparison is only assumed to hold when it's revisited exactly. The stack key is now the same as the memo key.

• The instantiating counter is gone, since nothing reads it any more.

Why fixpoint mode is exact

In fixpoint mode, the result of every comparison is a fixed equation over the comparisons it reaches, built from max, min and constants over the chain Assign < Cast < Invalid.

• The conditional fallbacks ((Generic, Union) and the struct fallback in (_, Union)) are mins whose value doesn't depend on the fallback when it isn't compared.
• Contractiveness means every revisit passes through a pair or function. So returning early at a comparison in progress always gives Assign, the least value.
• Instances only ever collect bounds directly (compare(U, X) or compare(X, U)). Those never recurse, so they're never revisited or merged, and the bounds checked when the function finishes are the same every time the function is compared.
• Inference collects candidates as a side effect, so fixpoint mode is off under inference.

Write μ for the least fixed point, and μ[D] for the least fixed point with the comparisons in D fixed to Assign. Then:

1. Every value computed or reused is at most μ. Early returns give the least value, and reused values are at most μ by induction. The equations are monotone and μ is their fixed point.
2. Each value is at least μ[D], where D is the set of in-progress comparisons below it that it relied on.
   • The inputs to its equation are at least μ[D ∪ {itself}].
   • Fixing only itself gives a one-variable function h built from max, min and constants. Such a function satisfies h(y) = h(⊥) ∨ (y ∧ h(⊤)), so h(h(⊥)) = h(⊥).
   • So h(⊥) is the least fixed point of h, which is μ[D].
3. A cached result is only reused while its D is on the stack S. Computing it again there would give μ[S] ≤ μ[D], since fixing more comparisons to Assign can only lower the fixed point.

A top-level comparison has an empty D, so its result is exactly μ with or without reuse. Results inside a cycle can differ between memo on and off, but callers only ever see top-level results.

The doc comments on FixpointMemo and is_monotone have the full argument. Two conditions are there because the proof needs them, not because of a known counterexample: instantiates_directly (a unit test pins which function types it accepts) and no fixpoint mode under inference. Dropping the contractiveness check, on the other hand, gives a real mismatch, which the differential test now catches (seed 4706).

I didn't compute per strongly connected component. With instance bounds and merges in the mix, that would have meant rewriting compare_impl, and the change would no longer be a memo over the existing algorithm.

Tests

• crates/rue-types/tests/memo.rs, differential. Random modules of up to three mutually recursive aliases, with:

  • generic parameters and applications;
  • generic function types (usually instantiated directly, sometimes nested, so both modes run);
  • structs, unions and pairs.

  For each module, every case compares compare both ways, compare_with_inference and its candidates, check and intersect with the memo on and off (without_compare_memo). Generic ids are renumbered first.

  Exponential cases give up after a fixed number of steps (with_step_limit). The test asserts that a case never gives up only with the memo on (it's 0 now).

  The CI run is 400 seeds plus seeds 1978 and 4706. Those two catch a broken exact-mode gate and a missing contractiveness check, which I confirmed by mutating the code. It takes 1.6s in release and about 33s in debug.

  The large run is #[ignore]d; run it with cargo test --release -p rue-types --test memo -- --ignored: 20,000 seeds × 8 queries gave 129,180 identical cases and 0 that gave up only with the memo on (5.5 minutes in release).

• Regression tests with step bounds rather than timings, so they don't flake. Both fail within seconds on main, since a step limit makes them panic:

  • test_rotating_generic_function (the G program): about 97,000 steps, bound 300,000. It never finishes on main.
  • test_mutually_recursive_intersection (the N0/N1 program): intersect 1,080,000 steps on main → 3,600; compare 89,000 → 1,700. Bound 20,000 each.

• Snapshot tests/types/recursive_intersection_errors.rue covers the second program end to end.

  • There's no snapshot for G. Comparing it recurses deeper than the snapshot test's 2 MiB thread allows in debug builds, though it's fine in release and in the CLI. The unit test runs it on a larger stack.

• No existing snapshot changed.

Timings (release, M-series Mac)

	main	this PR
G program	killed at 60s	0.26s
N0/N1 program	0.35s	0.01s (same error)
Fuzz corpus of 2,500 programs, 10s timeout	75 time out	39 time out (36 fixed, none new)

I couldn't reproduce the issue's corpus (#160's /tmp files aren't available), so I wrote a similar generator for Rue source. It makes two or three recursive aliases with generic parameters, generic function types, pairs and unions, followed by an assignment or an is check. Its programs are more aggressive than the issue's (75 of 2,500 time out on main, against 21 there). The counts come from running, one at a time, every program that timed out on either binary in a first parallel pass.

The programs that still time out also time out on main. They're generic functions whose generic appears nested inside a recursive type, such as fn<U>(...) -> U | N0<...>, so they run in exact mode. Compile time of the examples is unchanged (for example examples/json.rue takes 0.27s against 0.49s on main).

Found along the way (not fixed here)

• The second program's Recursion depth exceeded is a separate issue in check, not this bug.
  • The same check, (nil, N1) | N0 | Bytes | N1 | nil against N0 | Bytes | N0 and then against N1, recurs on its own path every two levels. So no finite runtime check exists, and the error is check_each's designed limit.
  • It happens on main too, and is now reached in 0.01s.
  • It may deserve a clearer error, or recursive checks.
• is_non_contractive misses a cycle through another alias's generic application: type T0 = T1<Int>; type T1<A> = A | (nil, A) | T0; isn't rejected. let _y: T0 = x with x: T0 then fails with "Cannot assign T0 to T0" (on main too). Fixpoint mode isn't affected, since it checks contractiveness with reaches_non_contractive_cycle.
• Exact mode is still exponential for generic functions whose generics appear nested inside recursive types (the remaining fuzz timeouts). Instances there can be merged when a comparison is revisited, which this argument doesn't cover.

Decisions for you (provisional)

• Test hooks. without_compare_memo and with_step_limit are behind the existing step-counter feature, rather than a new one. Splitting them out means adding a feature to rue-types/Cargo.toml and to its dev-dependency.
• Scope of fixpoint mode. It only applies when generic functions instantiate their generics directly. Everything else stays on the exact memo. Extending it would need a proof that merges preserve the fixed point, so I'd make that a follow-up.
• Semantics in the cycle key. With the current order of the match arms, the semantics passed down never reach an arm that reads them, so adding them changes no result. I kept them so the key stays complete if that changes (main's memo key already included them). The alternative is to drop them from both keys.
• No G snapshot because of the debug stack depth. The alternative is to run the snapshot test thread on a larger stack.