residuation: open membership returns residual constraints

1 files changed, 13 insertions, 1 deletions

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