fix unification of existing variables

src/data/expr.rs

@@ -19,6 +19,9 @@ pub(crate) enum Expr {
 }
 
 impl Expr {
+    pub(crate) fn build_equate(exprs: Vec<Expr>) -> Self {
+        Expr::Apply(&OP_EQ, exprs.into())
+    }
     pub(crate) fn negate(self) -> Self {
         Expr::Apply(&OP_NOT, Box::new([self]))
     }

src/query/compile.rs

@@ -2,6 +2,7 @@ use std::collections::{BTreeMap, BTreeSet};
 
 use anyhow::{anyhow, ensure, Result};
 
+use crate::data::expr::Expr;
 use crate::data::keyword::Keyword;
 use crate::data::program::{MagicAtom, MagicKeyword, MagicRule};
 use crate::query::relation::Relation;
@@ -164,8 +165,15 @@ impl SessionTx {
                     ret = ret.filter(p.clone());
                 }
                 MagicAtom::Unification(u) => {
-                    seen_variables.insert(u.binding.clone());
+                    if seen_variables.contains(&u.binding) {
-                    ret = ret.unify(u.binding.clone(), u.expr.clone());
+                        ret = ret.filter(Expr::build_equate(vec![
+                            Expr::Binding(u.binding.clone(), None),
+                            u.expr.clone(),
+                        ]));
+                    } else {
+                        seen_variables.insert(u.binding.clone());
+                        ret = ret.unify(u.binding.clone(), u.expr.clone());
+                    }
                 }
             }
         }