Stop dropping an enum at any enum already being dropped around it

src/refine/env.rs

@@ -1118,32 +1118,47 @@ 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> {
         if ty.is_mut() {
             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,23 +1174,17 @@ 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,
                 ));
             }
 
             pred_args.push(term);
             body.push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
+            enclosing_enums.pop();
             body
         } else {
             chc::Body::default()

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);
+}

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);
+}