Traverse types once when relating them invariantly

[coord-e]

Relating two types invariantly was expressed as subtyping in both directions:

let mut clauses = self.relate_sub_refined_type(got, expected);
clauses.extend(self.relate_sub_refined_type(expected, got));

relate_sub_refined_type walks the whole type structure, so this traverses it twice, and every owning or mutable pointer found inside relates its referent invariantly again. The number of clauses emitted for a refinement therefore doubles per pointer layer above it.

The two directions do not derive different constraints. Writing S for relate_sub_refined_type, E for relate_equal_refined_type and R for relate_sub_type:

S(A,B) = R(A.ty, B.ty) ++ [ A.ref => B.ref ]
E(A,B) = S(A,B) ++ S(B,A)
R(own X, own Y) = E(X, Y)              -- and likewise for &mut

E is symmetric by its definition, so E(own X, own Y) contains E(X,Y) and E(Y,X) — the same multiset twice. The direction only distinguishes anything at a covariant position, and every position below an owning or mutable pointer is invariant again, so the second direction just re-derives the constraints of the first.

This walks the type once, carrying the relation to derive, and emits both implications at the positions where the refinements must agree.

Effect

Measured on a &mut self trait method over Option<i32> (own (&mut (own Option<{int | p3}>, )), three such pointer layers), and on the same program with one more struct nesting:

	before	after
three pointer layers	29 clauses / 59.9 KB	14 clauses / 28.0 KB
four pointer layers	49 clauses / 115.0 KB	14 clauses / 31.6 KB

Both had 12 distinct clauses throughout. The count no longer grows with nesting depth. No change on the existing UI tests' output, which do not nest pointers above a refinement.

Two duplicates remain in that example, of the form p3 v <= ... /\ p3 v: both sides of an invariant position happen to carry the same predicate variable, so the two implications coincide. That is inherent to relating a position invariantly and is bounded by 2 regardless of depth. Dropping those would mean treating a clause whose head occurs in its own body as a nop, which needs PartialEq on Atom/Term/Formula; left out of this change.

Other changes

relate_equal_refined_type had no callers outside this module once the recursion stopped going through it, so it is dropped from the Subtyping trait.

Testing

cargo test (334 UI tests + unit and doc tests), cargo clippy -- -D warnings, cargo fmt --check.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PEtrgExrszb8aBUEGASPeE

---

Generated by Claude Code

[Copilot]

🟢 Approval recommended

The refactor preserves relation semantics while eliminating redundant recursive traversals.

Pull request overview

Optimizes invariant type relations by traversing type structures once while preserving bidirectional refinement constraints.

Changes:

• Introduces explicit Sub and Equal relation modes.
• Propagates invariance through owning and mutable pointers.
• Removes the unused equality method from Subtyping.

File summaries

File	Description
src/rty/subtyping.rs	Consolidates subtype and equality traversal to prevent duplicated clauses.

Review details

• Files reviewed: 1/1 changed files
• Comments generated: 0
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.