[coord-e]

Fixes #178. Also fixes #341.

Env::dropping_formula_for_term only cut recursion at a variant field that is directly a pointer to an enum with the same symbol. That caused two problems:

• Stack overflow. A recursive enum whose cycle goes any other way recursed forever: through a tuple field (Cons((i64, Box<L>)), Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178), through another enum (Node(i64, Option<Box<Node>>), the usual optional-child shape), or through a mutually recursive enum (A::Wrap(Box<B>), B::Back(Box<A>)). Details are in this comment on #178.
• Unresolved &mut. The check looked at the symbol only, so it also skipped a pointer to a different instantiation of the same generic enum. That left the &mut in Option<&mut Option<i64>> unresolved (Incompleteness: dropping a generic enum skips any field pointing to another instantiation of the same enum as "recursive", so the &mut in Option<&mut Option<T>> / Option<Box<Option<&mut T>>> is never resolved and the owner is havoc'd #341).

This PR passes a stack of the sorts of the enums whose drop formula is being built. An enum is skipped only when its sort is already on that stack. The direct Box<Self> case is skipped the same way it was before, now by the guard. Every other path back to an enclosing enum is cut too, and a different instantiation is recursed into. Skipping still only leaves a prophecy unresolved, so it stays sound, as the existing skip was.

This overlaps with #342, which fixes #341 by comparing the pointee's sort. It doesn't help the overflow cases, because there the field that leads back is not a pointer to the enum being dropped.

Tests

• Added tests/ui/{pass,fail}/enum_recursive_through_option.rs (Link(i64, Option<Box<Chain>>)). The pass file overflows the stack on main.
• Checked by hand: the reproducers from Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 and Incompleteness: dropping a generic enum skips any field pointing to another instantiation of the same enum as "recursive", so the &mut in Option<&mut Option<T>> / Option<Box<Option<&mut T>>> is never resolved and the owner is havoc'd #341 and the mutually recursive pair now verify as safe.
• cargo test passes locally: 402 UI tests, with Z3 5.0.0 and the pinned PCSat. cargo fmt --check and cargo clippy -- -D warnings are clean.

---

Generated by Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-27T21:44:50.211258Z	ccef9c8	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.