From ccef9c8a0d8c70742001603e25ccc30f971496b8 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 27 Oct 2026 21:42:53 +0000
Subject: [PATCH] Stop dropping an enum at any enum already being dropped
 around it

dropping_formula_for_term cut recursion only at a variant field that is
directly a pointer to an enum with the same symbol. A recursive enum
reached any other way recursed forever and overflowed the stack: through
a tuple field (#178), through another enum such as
`Node(i64, Option<Box<Node>>)`, or through a mutually recursive enum.
The symbol-only check also treated a pointer to another instantiation of
the same generic enum as recursive, leaving the `&mut` in
`Option<&mut Option<i64>>` unresolved (#341).

Track the sorts of the enums whose drop formula is being built, and skip
an enum only when its sort is already among them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Hw71PvaCsVX6Gv13CKahEf
---
 src/refine/env.rs                             | 29 ++++++++++++-------
 .../ui/fail/enum_recursive_through_option.rs  | 22 ++++++++++++++
 .../ui/pass/enum_recursive_through_option.rs  | 22 ++++++++++++++
 3 files changed, 63 insertions(+), 10 deletions(-)
 create mode 100644 tests/ui/fail/enum_recursive_through_option.rs
 create mode 100644 tests/ui/pass/enum_recursive_through_option.rs

diff --git a/src/refine/env.rs b/src/refine/env.rs
index 778bcfdec..28f37478b 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -1118,13 +1118,19 @@ where
             term,
             mut formula,
         } = self.path_type(path);
-        formula.push_conj(self.dropping_formula_for_term(&mut existentials, &ty, term));
+        formula.push_conj(self.dropping_formula_for_term(
+            &mut existentials,
+            &mut Vec::new(),
+            &ty,
+            term,
+        ));
         Assumption::new(existentials, formula)
     }
 
     fn dropping_formula_for_term(
         &self,
         existentials: &mut IndexVec<rty::ExistentialVarIdx, chc::Sort>,
+        enclosing_enums: &mut Vec<chc::Sort>,
         ty: &rty::Type<Var>,
         term: chc::Term<PlaceTypeVar>,
     ) -> chc::Body<PlaceTypeVar> {
@@ -1132,18 +1138,27 @@ where
             term.clone().mut_final().equal_to(term.mut_current()).into()
         } else if ty.is_own() {
             let inner = &ty.as_pointer().unwrap().elem.ty;
-            self.dropping_formula_for_term(existentials, inner, term.box_current())
+            self.dropping_formula_for_term(existentials, enclosing_enums, inner, term.box_current())
         } else if let Some(tty) = ty.as_tuple() {
             let mut body = chc::Body::default();
             for (i, elem) in tty.elems.iter().enumerate() {
                 body.push_conj(self.dropping_formula_for_term(
                     existentials,
+                    enclosing_enums,
                     &elem.ty,
                     term.clone().tuple_proj(i),
                 ));
             }
             body
         } else if let Some(ety) = ty.as_enum() {
+            let sort = ty.to_sort();
+            if enclosing_enums.contains(&sort) {
+                // TODO: we need recursively defined drop_pred for the recursive ADTs!
+                tracing::warn!("skipping recursive enum");
+                return chc::Body::default();
+            }
+            enclosing_enums.push(sort);
+
             let mut body = chc::Body::default();
 
             let enum_def = self.enum_defs.enum_def(&ety.symbol);
@@ -1159,16 +1174,9 @@ where
                 let field_term = chc::Term::var(ev.into());
                 pred_args.push(field_term.clone());
 
-                if let Some(p) = field_type.as_pointer() {
-                    if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) {
-                        // TODO: we need recursively defined drop_pred for the recursive ADTs!
-                        tracing::warn!("skipping recursive variant");
-                        continue;
-                    }
-                }
-
                 body.push_conj(self.dropping_formula_for_term(
                     existentials,
+                    enclosing_enums,
                     &field_type,
                     field_term,
                 ));
@@ -1176,6 +1184,7 @@ where
 
             pred_args.push(term);
             body.push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
+            enclosing_enums.pop();
             body
         } else {
             chc::Body::default()
diff --git a/tests/ui/fail/enum_recursive_through_option.rs b/tests/ui/fail/enum_recursive_through_option.rs
new file mode 100644
index 000000000..6e0df72c0
--- /dev/null
+++ b/tests/ui/fail/enum_recursive_through_option.rs
@@ -0,0 +1,22 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+enum Chain {
+    Link(i64, Option<Box<Chain>>),
+}
+
+impl thrust_models::Model for Chain {
+    type Ty = Self;
+}
+
+fn sum(c: &Chain) -> i64 {
+    match c {
+        Chain::Link(v, None) => *v,
+        Chain::Link(v, Some(next)) => *v + sum(next),
+    }
+}
+
+fn main() {
+    let c = Chain::Link(1, Some(Box::new(Chain::Link(2, None))));
+    assert!(sum(&c) == 4);
+}
diff --git a/tests/ui/pass/enum_recursive_through_option.rs b/tests/ui/pass/enum_recursive_through_option.rs
new file mode 100644
index 000000000..e7abcb245
--- /dev/null
+++ b/tests/ui/pass/enum_recursive_through_option.rs
@@ -0,0 +1,22 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+enum Chain {
+    Link(i64, Option<Box<Chain>>),
+}
+
+impl thrust_models::Model for Chain {
+    type Ty = Self;
+}
+
+fn sum(c: &Chain) -> i64 {
+    match c {
+        Chain::Link(v, None) => *v,
+        Chain::Link(v, Some(next)) => *v + sum(next),
+    }
+}
+
+fn main() {
+    let c = Chain::Link(1, Some(Box::new(Chain::Link(2, None))));
+    assert!(sum(&c) == 3);
+}