Stack overflow (non-termination) in `TypeBuilder::build`: a struct is always expanded structurally with no cycle cut, so any struct that reaches itself (`struct Node { next: Option<Box<Node>> }`, `struct Tree { kids: Vec<Tree> }`) aborts the compiler

[coord-e]

Summary

refine::template::TypeBuilder::build (src/refine/template.rs:206, and the Scoped copy at src/refine/template.rs:392) gives an enum a nominal representation — rty::EnumType::new(sym, args), which names the datatype and never looks at its variants — but expands a struct structurally, into a tuple of the refinement types of all of its fields:

if def.is_enum() {
    let sym = refine::datatype_symbol(self.tcx, def.did());
    let args: IndexVec<_, _> = params.types().map(|ty| ...self.build(ty)...).collect();
    rty::EnumType::new(sym, args).into()          // nominal: variants are NOT visited
} else if def.is_struct() {                       // src/refine/template.rs:247 / :426
    let elem_tys = def
        .all_fields()
        .map(|field| {
            let ty = field.ty(self.tcx, params);
            // elaboration: all fields are boxed
            rty::PointerType::own(self.build(ty)).into()   // <- unconditional descent
        })
        .collect();
    rty::TupleType::new(elem_tys).into()
}

An enum therefore breaks any type-level cycle at its own name. A struct has no name in rty at all (rty.rs:585: "the current implementation uses tuples to represent structs … It is our TODO to improve the struct representation"), so there is nothing to break the cycle on, and there is no memo table or depth cutoff either. Any struct that can reach itself through its fields makes build recurse forever.

The recursion does not even have to be direct: it is enough that some field's type mentions the struct again, and build descends into an enum's generic arguments and into Box/Seq/Array model payloads. That covers the two most common recursive data structures in Rust:

struct Node { v: i32, next: Option<Box<Node>> }   // singly-linked list
struct Tree { v: i32, kids: Vec<Tree> }           // n-ary tree

The result is a hard fatal runtime error: stack overflow (exit 134) with no diagnostic — the CHC system is never built and the solver is never invoked.

Minimal reproduction

struct S { b: Box<S> } is the smallest form; Option<Box<..>> and Vec<..> are the ones that actually show up in code.

// min.rs
struct S { b: Box<S> }
impl thrust_models::Model for S { type Ty = Self; }

#[thrust::trusted]
#[thrust::callable]
fn make() -> S { unimplemented!() }

fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false min.rs; echo "exit=$?"

thread 'rustc' (12366) has overflowed its stack
fatal runtime error: stack overflow, aborting
exit=134

All of the following abort the same way, and all of them are accepted by rustc:

struct S    { b: Box<S> }                        // direct
struct Node { v: i32, next: Option<Box<Node>> }  // through an enum's generic argument
struct Tree { v: i32, kids: Vec<Tree> }          // through Seq/Array
struct A { b: Option<Box<B>> }                   // mutual recursion
struct B { a: Option<Box<A>> }

A realistic program — a list length function — never gets as far as producing a verdict:

struct Node { v: i32, next: Option<Box<Node>> }
impl thrust_models::Model for Node { type Ty = Self; }

fn len(n: &Option<Box<Node>>) -> i32 {
    match n {
        Some(b) => 1 + len(&b.next),
        None => 0,
    }
}

#[thrust::callable]
fn f() {
    let l = Some(Box::new(Node { v: 1, next: None }));
    assert!(len(&l) == 1);
}
fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false list.rs; echo "exit=$?"
thread 'rustc' (12418) has overflowed its stack
fatal runtime error: stack overflow, aborting
exit=134

Independent of -C opt-level (0, 1, 2 all abort) — this is type-level work done before any MIR is analysed.

No value of the type is ever created

The reproducers above deliberately avoid constructing, matching or dropping a value, to separate this from the drop-time recursion of #178.

program	verdict
struct Node {..} declared, not named by any signature or body	safe (nothing builds the type)
#[thrust::trusted] #[thrust::callable] fn make() -> Node (never called)	stack overflow
#[thrust::trusted] #[thrust::callable] fn take(_n: &Node) (never called)	stack overflow
#[thrust::callable] fn f() { let _n: Option<Node> = None; }	stack overflow

The middle two rows are the decisive ones: #[thrust::trusted] puts the def in skip_analysis, the function is never called, and no value of Node exists anywhere. The only work performed is turning the signature into a refinement type. That is TypeBuilder::build, and it is where the recursion is.

Enum vs. struct, side by side

The same cycle expressed with an enum at the recursive position terminates, because build stops at the enum's name:

type	result
enum L { Cons(i64, Box<L>), Nil }	safe
enum L { Cons(i64, Option<Box<L>>), Nil }	safe
enum L { Cons((i64, Box<L>)), Nil } (the #178 shape), signature only	safe
struct S { b: Box<S> }	stack overflow
struct Node { v: i32, next: Option<Box<Node>> }	stack overflow
struct Tree { v: i32, kids: Vec<Tree> }	stack overflow
enum W { V(Node), N } (Node recursive), signature only	safe — W's variants are not visited yet
enum W { V(Node), N }, a W value constructed and matched	stack overflow — see the second site below

So the trigger is precisely "the recursion passes through a struct", not "the type is recursive".

The recursion cycle

Adding a one-line eprintln! at the top of TypeBuilder::build (after resolve_model_ty) prints the cycle verbatim. struct S { b: Box<S> }, tail of the output before the abort (3153 calls in the ~1 s before the stack runs out):

DBGBUILD closed S
DBGBUILD closed thrust_models::model::Box<S>
DBGBUILD closed S
DBGBUILD closed thrust_models::model::Box<S>
...

struct Node { v: i32, next: Option<Box<Node>> } — the cycle closes through the Option's generic argument, which build does descend into even though the variants are not visited:

DBGBUILD closed Node
DBGBUILD closed thrust_models::model::Int
DBGBUILD closed std::option::Option<thrust_models::model::Box<Node>>
DBGBUILD closed thrust_models::model::Box<Node>
DBGBUILD closed Node
...

struct Tree { v: i32, kids: Vec<Tree> } — through the Seq/Array model:

DBGBUILD closed Tree
DBGBUILD closed thrust_models::model::Int
DBGBUILD closed thrust_models::model::Seq<Tree>
DBGBUILD closed thrust_models::model::Array<thrust_models::model::Int, Tree>
DBGBUILD closed thrust_models::model::Int
DBGBUILD closed Tree
...

For contrast, enum L { Cons(i64, Box<L>), Nil } calls build(L) exactly once for the whole run.

The three descents that close a cycle are all in build itself:

• the struct branch (src/refine/template.rs:247, :426) — every field;
• the enum branch (src/refine/template.rs:240, :421) — every generic argument (params.types()), which is how Option<Box<Node>> gets back to Node;
• model_adt — Box/Mut/Array payloads (src/refine/template.rs:172-200, :363-389).

None of them is guarded, and there is no cache keyed on the mir_ty::Ty being built.

Second site

analyze::Analyzer::build_enum_def (src/analyze.rs:315) builds each variant's field types with the same TypeBuilder::build, so an enum whose variant holds a recursive struct also aborts as soon as the enum def is actually registered:

struct Node { v: i32, next: Option<Box<Node>> }
impl thrust_models::Model for Node { type Ty = Self; }
enum W { V(Node), N }
impl thrust_models::Model for W { type Ty = Self; }

#[thrust::callable]
fn f() {
    let w = W::N;
    match w { W::V(_) => {}, W::N => {} }   // registers W -> builds Node -> overflow
}
fn main() {}

Any fix that only guards refine::template will want to cover this call too.

Distinct from the known issues

• Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 is the other stack overflow, but in Env::dropping_formula_for_term, and it is about the drop-formula cutoff for a recursive enum whose self-pointer sits inside a tuple/struct field. It needs a value to be constructed and dropped: its own reproducer shape (enum L { Cons((i64, Box<L>)), Nil }) is safe here when the type only appears in a never-called signature, whereas every reproducer above overflows with no value in existence. Different function, different trigger, and the enum-side cutoff Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 discusses is not on the path at all — the recursion never leaves TypeBuilder::build.
• Incompleteness: dropping a recursively-defined ADT does not resolve &mut prophecies stored in its recursive-position field, so safe programs are wrongly rejected #173 (dropping a recursively-defined ADT does not resolve &mut prophecies in the recursive-position field) and Incompleteness: a &mut stored in a Box has its prophecy resolved only at the Box's drop, so reading the referent before the box is dropped wrongly rejects safe programs #175 (&mut in a Box) are wrong-verdict issues about prophecies; there is no &mut anywhere in these reproducers and no verdict is ever produced.
• Incompleteness: Box<T> (Own) is related invariantly in subtyping, wrongly rejecting valid refinement weakening through a box #157 (Box related invariantly) and Refinements on Box (own-pointer) pointee in return position are not enforced — unsound #97 (Box pointee refinement in return position) are about Box subtyping/refinement, not about building the type at all.
• Panic / undeclared SMT sort: an enum reachable only through an ADT's field type is never registered in EnumDefs, so any struct with an enum-typed field (struct W { o: Option<i32> }) aborts verification #221 (an enum reachable only through an ADT field is never registered) is the opposite failure — a type not being visited; here the visiting is what does not terminate.
• Not a numerical-range, unsigned or overflow issue: the reproducers contain the literal 1 and nothing else.

Suggested direction

Both build impls would need a cycle cut. The cheapest is a HashSet<mir_ty::Ty> (or a HashMap memo) of types currently being built, but a struct has no rty name to tie the knot to, so a real fix probably wants the nominal struct representation that rty.rs:585 already lists as a TODO — a datatype_symbol-keyed representation for structs, the way enums already have one, at which point the enum branch's cutoff mechanism applies to structs unchanged.

Environment

• thrust @ 35eea46 (current main)
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (the version .github/actions/setup-z3 pins), default solver configuration — never reached in any of these runs