From 0886f3c71cf8551e4f8b3726654003a4f29645f0 Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sat, 11 Jul 2026 22:12:53 -0300
Subject: residuation: open membership returns residual constraints

---
 lib/program.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'lib/program.ml')

diff --git a/lib/program.ml b/lib/program.ml
index ac62781..b0e363b 100644
--- a/lib/program.ml
+++ b/lib/program.ml
@@ -21,7 +21,19 @@ let load statements =
               pending
             in
             match Vm.Standalone.solve world pending_body with
-            | Ok (_ :: _) -> admit rest
+            (* Membership must be proven outright: an answer that is
+               itself conditioned on residual constraints does not
+               admit a fact. *)
+            | Ok solutions
+              when List.exists (fun s -> s.Vm.residue = []) solutions ->
+                admit rest
+            | Ok (_ :: _) ->
+                Error
+                  (Undecidable_criterion
+                     {
+                       relation = pending_relation;
+                       label = Label.to_string pending_label;
+                     })
             | Ok [] ->
                 Error
                   (Integrity
-- 
cgit v1.2.3