Repository: terminusdb-labs/swipl-rs (language: rust)

Issue:
Unification incorrectly allows unifying non-unifiable values
```rust
semidet fn incorrect(_context, l) {
    l.unify([1u64, 2u64, 3u64].as_slice())
}
```

```prolog
%% Incorrect output
?- incorrect([2, 2, 3]).
true.

?- incorrect([1, 3, 3]).
true.

?- incorrect([2, 3, 3]).
true.

%% Correct output
?- incorrect([1, 2, 3]).
true.

?- incorrect([2, 3, 4]).
false.

?- incorrect([1, 2, 4]).
false.

?- incorrect([2, 3]).
false.

?- incorrect([1, 2]).
false.

?- incorrect([1, 2, 3, 4]).
false.
```

When using the unify function on a list, it is possible for all but the last value to not unify but for the overall list unification to succeed - which is probably not correct.


Discussion / hints:

Fix patch:
diff --git a/swipl/src/term.rs b/swipl/src/term.rs
index b216d4436b..c3322e79b4 100644
--- a/swipl/src/term.rs
+++ b/swipl/src/term.rs
@@ -944,25 +944,25 @@ where
 
         let frame = context.open_frame();
         let list = frame.new_term_ref();
+
         if list.unify(term).is_err() {
             return false;
         }
-        let mut success = true;
 
         for t in self.iter() {
             // create a new frame to ensure we don't just keep putting head and tail refs on the stack.
             let frame2 = frame.open_frame();
             let head = frame2.new_term_ref();
             let tail = frame2.new_term_ref();
-            success =
-                unsafe { PL_unify_list(list.term_ptr(), head.term_ptr(), tail.term_ptr()) != 0 };
 
-            if !success {
-                break;
+            // if list unification fails, or head can not be unified with current term,
+            // return false early.
+            // note: || is short-circuiting OR
+            if unsafe { PL_unify_list(list.term_ptr(), head.term_ptr(), tail.term_ptr()) == 0 }
+                || head.unify(t).is_err() {
+                return false;
             }
 
-            success = head.unify(t).is_ok();
-
             // reset term - should really be a method on term
             unsafe { PL_put_variable(list.term_ptr()) };
 
@@ -973,10 +973,8 @@ where
             frame2.close();
         }
 
-        if success {
-            success = unsafe { PL_unify_nil(list.term_ptr()) != 0 };
-            frame.close();
-        }
+        let success = unsafe { PL_unify_nil(list.term_ptr()) != 0 };
+        frame.close();
 
         success
     }


Test patch: