From 9def3636e7120dd421724ba7864e491e7dab8b7c Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Dmitrii.Kosarev@pm.me>
Date: Tue, 17 Dec 2024 19:34:35 +0300
Subject: [PATCH 1/8] Add a reproduction case for issue #173. Discovered by
 @Lozov-Petr

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <Dmitrii.Kosarev@pm.me>
---
 regression_ppx/dune            | 37 ++++++++++++++++++++++++++++------
 regression_ppx/test014.t       |  4 ++++
 regression_ppx/test014diseq.ml | 18 +++++++++++++++++
 3 files changed, 53 insertions(+), 6 deletions(-)
 create mode 100644 regression_ppx/test014.t
 create mode 100644 regression_ppx/test014diseq.ml

diff --git a/regression_ppx/dune b/regression_ppx/dune
index 05771aa4..a881ac6e 100644
--- a/regression_ppx/dune
+++ b/regression_ppx/dune
@@ -148,13 +148,29 @@
  (modules test013mutual)
  (package OCanren)
  (public_names -)
- (flags
-  (:standard
-   ;-dsource
-   ;
-   ))
  (preprocess
-  (pps OCanren-ppx.ppx_distrib GT.ppx_all -- -new-typenames -pretty))
+  (pps
+   OCanren-ppx.ppx_distrib
+   GT.ppx_all
+   OCanren-ppx.ppx_fresh
+   --
+   -new-typenames
+   -pretty))
+ (libraries OCanren OCanren.tester))
+
+(executables
+ (names test014diseq)
+ (modules test014diseq)
+ (package OCanren)
+ (public_names -)
+ (preprocess
+  (pps
+   GT.ppx_all
+   OCanren-ppx.ppx_fresh
+   OCanren-ppx.ppx_tester
+   OCanren-ppx.ppx_repr
+   --
+   -pretty))
  (libraries OCanren OCanren.tester))
 
 (cram
@@ -283,3 +299,12 @@
   %{project_root}/ppx/pp_ocanren_all.exe
   test013mutual.ml
   test013mutual.exe))
+
+(cram
+ (package OCanren)
+ (applies_to test014)
+ (deps
+  (package OCanren-ppx)
+  %{project_root}/ppx/pp_ocanren_all.exe
+  test014diseq.ml
+  test014diseq.exe))
diff --git a/regression_ppx/test014.t b/regression_ppx/test014.t
new file mode 100644
index 00000000..6811454e
--- /dev/null
+++ b/regression_ppx/test014.t
@@ -0,0 +1,4 @@
+  $ ./test014diseq.exe
+  rel, 1 answer {
+  Fatal error: exception File "src/core/Disequality.ml", line 177, characters 8-14: Assertion failed
+  [2]
diff --git a/regression_ppx/test014diseq.ml b/regression_ppx/test014diseq.ml
new file mode 100644
index 00000000..88bd6ab5
--- /dev/null
+++ b/regression_ppx/test014diseq.ml
@@ -0,0 +1,18 @@
+open OCanren
+open Tester
+
+let rel list1 =
+  let open OCanren.Std in
+  fresh
+    (list2 hd1 tl1 hd2 tl2)
+    (list1 =/= list2)
+    (list1 === hd1 % tl1)
+    (list2 === hd2 % tl2)
+    (hd2 === !!1)
+    (tl2 === nil ())
+    (hd1 === !!1)
+    (tl1 === nil ())
+;;
+
+(* let () = [%tester run_r [%show GT.int GT.list] (Std.List.reify reify) 1 (fun q -> rel q)] *)
+let () = run_r (Std.List.reify reify) ([%show: GT.int logic Std.List.logic] ()) 1 q qh (REPR rel)

From 9e7f58242953667dbdbea73ef3b31a0a0dda7bed Mon Sep 17 00:00:00 2001
From: Peter Lozov <not_kill@gmail.ru>
Date: Thu, 22 Jun 2023 04:21:17 +0300
Subject: [PATCH 2/8] Magic fix for disequality simplify exception.

---
 src/core/Subst.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index 8aa8b253..c909e708 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -157,8 +157,12 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       ~fvar:(fun ((_, subst) as acc) x y ->
         match walk env subst x, walk env subst y with
         | Var x, Var y      ->
-          if Var.equal x y then acc else extend x (Term.repr y) acc
-        | Var x, Value y    -> extend x y acc
+          (* if Var.equal x y then acc else extend x (Term.repr y) acc *)
+         let cmp = Term.Var.compare x y in
+          if cmp < 0 then extend x (Term.repr y) acc
+          else if cmp > 0 then extend y (Term.repr x) acc
+          else acc
+          | Var x, Value y    -> extend x y acc
         | Value x, Var y    -> extend y x acc
         | Value x, Value y  -> helper x y acc
       )

From db682f4eb5fa67d29cb2a8b6b879663176b251d0 Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Dmitrii.Kosarev@pm.me>
Date: Tue, 17 Dec 2024 19:46:37 +0300
Subject: [PATCH 3/8] Promote tests after Peter's fix for disequality

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <Dmitrii.Kosarev@pm.me>
---
 regression/test002.t     |  6 +++---
 regression/test005.t     |  8 ++++----
 regression/test006.t     |  4 ++--
 regression/test014.t     | 18 +++++++++---------
 regression_ppx/test014.t |  3 +--
 5 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/regression/test002.t b/regression/test002.t
index c3abc17a..99ef14d0 100644
--- a/regression/test002.t
+++ b/regression/test002.t
@@ -1,7 +1,7 @@
   $ ./test002sort.exe
-  [O; O; _.138]
-  [O; O; _.136 [=/= O]]
-  [O; O; _.153 [=/= O]]
+  [O; O; _.140]
+  [O; O; _.140 [=/= O]]
+  [O; O; _.157 [=/= O]]
   [O; S (O); S (_.497)]
   [O; S (O); S (_.516 [=/= O])]
   [O; S (O); S (_.110)]
diff --git a/regression/test005.t b/regression/test005.t
index 85d225fd..dbb8b0a5 100644
--- a/regression/test005.t
+++ b/regression/test005.t
@@ -19,14 +19,14 @@
   q=[("x", V ("y")) | _.13];
   }
   fun q -> infero (abs varX (v varX)) q, 1 answer {
-  q=Arr (_.18, _.18);
+  q=Arr (_.21, _.21);
   }
   fun q -> infero (abs varF (abs varX (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (Arr (_.30, _.26), Arr (_.30, _.26));
+  q=Arr (Arr (_.54, _.26), Arr (_.54, _.26));
   }
   fun q -> infero (abs varX (abs varF (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (_.30, Arr (Arr (_.30, _.26), _.26));
+  q=Arr (_.64, Arr (Arr (_.64, _.26), _.26));
   }
   fun q -> infero q (arr (p varX) (p varX)), 1 answer {
-  q=Abs (_.29, V (_.29));
+  q=Abs (_.30, V (_.30));
   }
diff --git a/regression/test006.t b/regression/test006.t
index f56d607c..1d0e4012 100644
--- a/regression/test006.t
+++ b/regression/test006.t
@@ -24,10 +24,10 @@
   q=V ("x");
   }
   fun q -> evalo (app q (v varX)) (v varX), 1 answer {
-  q=Abs (_.44, V (_.44));
+  q=Abs (_.59, V (_.59));
   }
   fun q r -> evalo (app r q) (v varX), 1 answer {
-  q=V ("x"); r=Abs (_.54, V (_.54));
+  q=V ("x"); r=Abs (_.68, V (_.68));
   }
   fun q r s -> a_la_quine q r s, 2 answers {
   q=Abs (_.668, V (_.668)); r=Abs (_.668, V (_.668)); s=Abs (_.668, V (_.668));
diff --git a/regression/test014.t b/regression/test014.t
index c1f784a2..8c5cbfb0 100644
--- a/regression/test014.t
+++ b/regression/test014.t
@@ -28,18 +28,18 @@
   q=[_.13 | _.14]; r=[]; s=[];
   q=[1]; r=[_.15 | _.16]; s=[_.15 | _.16];
   q=[_.17; _.18 | _.19]; r=[1]; s=[_.17; _.18 | _.19];
-  q=[0; 1]; r=[_.28; _.33 | _.34]; s=[0; _.28; _.33 | _.34];
-  q=[0; 0; 1]; r=[_.69; _.76 | _.77]; s=[0; 0; _.69; _.76 | _.77];
+  q=[0; 1]; r=[_.43; _.33 | _.34]; s=[0; _.43; _.33 | _.34];
+  q=[0; 0; 1]; r=[_.97; _.76 | _.77]; s=[0; 0; _.97; _.76 | _.77];
   q=[1; _.102 | _.103]; r=[0; 1]; s=[0; 1; _.102 | _.103];
-  q=[0; 0; 0; 1]; r=[_.149; _.164 | _.165]; s=[0; 0; 0; _.149; _.164 | _.165];
+  q=[0; 0; 0; 1]; r=[_.207; _.164 | _.165]; s=[0; 0; 0; _.207; _.164 | _.165];
   q=[1; _.192 | _.193]; r=[0; 0; 1]; s=[0; 0; 1; _.192 | _.193];
   q=[0; 1; _.218 | _.219]; r=[0; 1]; s=[0; 0; 1; _.218 | _.219];
-  q=[0; 0; 0; 0; 1]; r=[_.314; _.343 | _.344]; s=[0; 0; 0; 0; _.314; _.343 | _.344];
+  q=[0; 0; 0; 0; 1]; r=[_.437; _.343 | _.344]; s=[0; 0; 0; 0; _.437; _.343 | _.344];
   q=[1; _.375 | _.376]; r=[0; 0; 0; 1]; s=[0; 0; 0; 1; _.375 | _.376];
   q=[0; 1; _.401 | _.402]; r=[0; 0; 1]; s=[0; 0; 0; 1; _.401 | _.402];
   q=[0; 0; 1; _.459 | _.460]; r=[0; 1]; s=[0; 0; 0; 1; _.459 | _.460];
   q=[1; 1]; r=[1; 1]; s=[1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 1]; r=[_.656; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.656; _.713 | _.714];
+  q=[0; 0; 0; 0; 0; 1]; r=[_.904; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.904; _.713 | _.714];
   q=[1; _.745 | _.746]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.745 | _.746];
   q=[0; 1; _.778 | _.779]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.778 | _.779];
   q=[0; 0; 1; _.834 | _.835]; r=[0; 0; 1]; s=[0; 0; 0; 0; 1; _.834 | _.835];
@@ -48,7 +48,7 @@
   q=[0; 1; 1]; r=[1; 1]; s=[0; 1; 0; 0; 1];
   q=[1; 1]; r=[1; 1; 1]; s=[1; 0; 1; 0; 1];
   q=[1; 1]; r=[0; 1; 1]; s=[0; 1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1360; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1360; _.1493 | _.1494];
+  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1860; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1860; _.1493 | _.1494];
   q=[1; _.1523 | _.1524]; r=[0; 0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1523 | _.1524];
   q=[0; 1; _.1553 | _.1554]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1553 | _.1554];
   q=[0; 0; 1; _.1607 | _.1608]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1607 | _.1608];
@@ -64,11 +64,11 @@
   q=[1]; r=[0; 1];
   q=[0; 1]; r=[0; 0; 1];
   q=[1; 1]; r=[0; 1; 1];
-  q=[1; _.225; 1]; r=[0; 1; _.225; 1];
+  q=[1; _.653; 1]; r=[0; 1; _.653; 1];
   q=[0; 0; 1]; r=[0; 0; 0; 1];
   q=[0; 1; 1]; r=[0; 0; 1; 1];
-  q=[1; _.247; _.408; 1]; r=[0; 1; _.247; _.408; 1];
-  q=[0; 1; _.408; 1]; r=[0; 0; 1; _.408; 1];
+  q=[1; _.1001; _.408; 1]; r=[0; 1; _.1001; _.408; 1];
+  q=[0; 1; _.1243; 1]; r=[0; 0; 1; _.1243; 1];
   q=[0; 0; 0; 1]; r=[0; 0; 0; 0; 1];
   }
   fun q r -> lelo q r, 15 answers {
diff --git a/regression_ppx/test014.t b/regression_ppx/test014.t
index 6811454e..61fd08bb 100644
--- a/regression_ppx/test014.t
+++ b/regression_ppx/test014.t
@@ -1,4 +1,3 @@
   $ ./test014diseq.exe
   rel, 1 answer {
-  Fatal error: exception File "src/core/Disequality.ml", line 177, characters 8-14: Assertion failed
-  [2]
+  }

From 3bd7d44be833a85166103ff76a0008a29e62d5e3 Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Dmitrii.Kosarev@pm.me>
Date: Tue, 17 Dec 2024 19:47:02 +0300
Subject: [PATCH 4/8] Promote a BAD WRONG test after fixes (see #173)

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <Dmitrii.Kosarev@pm.me>
---
 regression/test011.t | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/test011.t b/regression/test011.t
index a4a7a153..43190636 100644
--- a/regression/test011.t
+++ b/regression/test011.t
@@ -174,7 +174,7 @@
   fun q ->
     OCanren.Fresh.two
       (fun x y -> delay (fun () -> conj (!![x; y] === q) (y =/= x))), all answers {
-  q=[_.11; _.12 [=/= _.11]];
+  q=[_.11 [=/= _.12]; _.12];
   }
   fun q ->
     OCanren.Fresh.two
@@ -247,7 +247,7 @@
   fun x ->
     OCanren.Fresh.two
       (fun y z -> delay (fun () -> conj (x =/= !![y; !2]) (x === !![z; !2]))), all answers {
-  q=[_.12 [=/= _.11]; 2];
+  q=[_.12; 2];
   }
   fun q -> distincto (!2 % (!3 %< q)), all answers {
   q=_.35 [=/= 2; =/= 3];

From cdec183648243990420524a79bd0aedac919af39 Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Dmitrii.Kosarev@pm.me>
Date: Tue, 24 Dec 2024 14:01:01 +0300
Subject: [PATCH 5/8] [chore] API for debugging diseq constraints

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <Dmitrii.Kosarev@pm.me>
---
 src/core/Core.ml         |  7 ++++++-
 src/core/Core.mli        |  4 +++-
 src/core/Disequality.ml  | 29 +++++++++++++++++++++++++++++
 src/core/Disequality.mli |  2 ++
 4 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/core/Core.ml b/src/core/Core.ml
index 954cbde3..b987b54c 100644
--- a/src/core/Core.ml
+++ b/src/core/Core.ml
@@ -795,4 +795,9 @@ module Tabling =
 
 let reify_in_empty reifier x =
   let st = State.empty () in
-  reifier (State.env st) x
\ No newline at end of file
+  reifier (State.env st) x
+
+let trace_diseq : goal = fun st ->
+  Format.printf "%a\n%!" Disequality.pp (State.constraints st);
+  success st
+
diff --git a/src/core/Core.mli b/src/core/Core.mli
index fff880bc..795be3cc 100644
--- a/src/core/Core.mli
+++ b/src/core/Core.mli
@@ -320,4 +320,6 @@ module PrunesControl : sig
 end
 
 (** Runs reifier on empty state. Useful to debug execution order *)
-val reify_in_empty: ('a, 'b) Reifier.t -> 'a -> 'b
\ No newline at end of file
+val reify_in_empty: ('a, 'b) Reifier.t -> 'a -> 'b
+
+val trace_diseq: goal
\ No newline at end of file
diff --git a/src/core/Disequality.ml b/src/core/Disequality.ml
index 8fab0dfd..6b49d7db 100644
--- a/src/core/Disequality.ml
+++ b/src/core/Disequality.ml
@@ -91,6 +91,9 @@ module Disjunct :
     (* Disjunction.t is a set of single disequalities joint by disjunction *)
     type t
 
+
+    val pp : Format.formatter -> t -> unit
+
     (* [make env subst x y] creates new disjunct from the disequality [x =/= y] *)
     val make : Env.t -> Subst.t -> 'a -> 'a -> t
 
@@ -118,6 +121,15 @@ module Disjunct :
   struct
     type t = Term.t Term.VarMap.t
 
+    let pp ppf d =
+      if Term.VarMap.is_empty d then Format.fprintf ppf "<empty>"
+      else
+        Format.fprintf ppf "[| ";
+        Term.VarMap.iter (fun k v ->
+          Format.fprintf ppf "@[%d =/= %s@], @," k.Term.Var.index (Term.show v)
+          ) d;
+        Format.fprintf ppf " |]"
+
     let update t =
       ListLabels.fold_left ~init:t
         ~f:(let open Subst.Binding in fun acc {var; term} ->
@@ -208,6 +220,8 @@ module Conjunct :
 
     val empty : t
 
+    val pp : Format.formatter -> t -> unit
+
     val is_empty : t -> bool
 
     val make : Env.t -> Subst.t -> 'a -> 'a -> t
@@ -236,6 +250,16 @@ module Conjunct :
 
     type t = Disjunct.t M.t
 
+    let pp ppf map =
+      if M.is_empty map
+      then Format.fprintf ppf "{}"
+      else
+        Format.fprintf ppf "{ ";
+        M.iter (fun k v ->
+          Format.fprintf ppf "@[%d: %a@],@ " k Disjunct.pp v
+        ) map;
+        Format.fprintf ppf " }"
+
     let empty = M.empty
 
     let is_empty = M.is_empty
@@ -394,3 +418,8 @@ let project env subst cstore fv =
 
 let reify env subst cstore x =
   Conjunct.reify env subst (combine env subst cstore) x
+
+let pp ppf : t -> unit  =
+  Term.VarMap.iter (fun k v ->
+    Format.fprintf ppf "@[%d: %a@]@," k.Term.Var.index Conjunct.pp v
+    )
\ No newline at end of file
diff --git a/src/core/Disequality.mli b/src/core/Disequality.mli
index 582d6216..72546a8a 100644
--- a/src/core/Disequality.mli
+++ b/src/core/Disequality.mli
@@ -51,3 +51,5 @@ module Answer :
   end
 
 val reify : Env.t -> Subst.t -> t -> 'a -> Answer.t list
+
+val pp: Format.formatter -> t -> unit

From 79e0390877b3d53ee072232779e05bc48415ffc8 Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Dmitrii.Kosarev@pm.me>
Date: Fri, 20 Dec 2024 19:41:50 +0300
Subject: [PATCH 6/8] Revert "Magic fix for disequality simplify exception."

This reverts commit 9e7f58242953667dbdbea73ef3b31a0a0dda7bed.
---
 src/core/Subst.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index c909e708..8aa8b253 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -157,12 +157,8 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       ~fvar:(fun ((_, subst) as acc) x y ->
         match walk env subst x, walk env subst y with
         | Var x, Var y      ->
-          (* if Var.equal x y then acc else extend x (Term.repr y) acc *)
-         let cmp = Term.Var.compare x y in
-          if cmp < 0 then extend x (Term.repr y) acc
-          else if cmp > 0 then extend y (Term.repr x) acc
-          else acc
-          | Var x, Value y    -> extend x y acc
+          if Var.equal x y then acc else extend x (Term.repr y) acc
+        | Var x, Value y    -> extend x y acc
         | Value x, Var y    -> extend y x acc
         | Value x, Value y  -> helper x y acc
       )

From 62c7b284be35d5f6dccb289f30d6cf7d9428f948 Mon Sep 17 00:00:00 2001
From: Kakadu <Kakadu@pm.me>
Date: Tue, 24 Dec 2024 01:22:40 +0300
Subject: [PATCH 7/8] Fix issue #173

Signed-off-by: Dmitrii Kosarev a.k.a. Kakadu <Kakadu@pm.me>
---
 regression_ppx/test014diseq.ml | 35 ++++++++++++++++-
 src/core/Disequality.ml        | 70 +++++++++++++++++++++++++---------
 src/core/Subst.ml              | 25 ++++++++++++
 src/core/Subst.mli             |  5 +++
 src/core/Term.ml               |  4 ++
 src/core/Term.mli              |  3 ++
 6 files changed, 123 insertions(+), 19 deletions(-)

diff --git a/regression_ppx/test014diseq.ml b/regression_ppx/test014diseq.ml
index 88bd6ab5..4d52a13c 100644
--- a/regression_ppx/test014diseq.ml
+++ b/regression_ppx/test014diseq.ml
@@ -1,17 +1,50 @@
 open OCanren
 open Tester
 
+let debug_line line =
+  debug_var !!1 OCanren.reify (function _ ->
+      Format.printf "%d\n%!" line;
+      success)
+;;
+
+let trace_index msg var =
+  debug_var var OCanren.reify (function
+      | [ Var (n, _) ] ->
+          Printf.printf "%s = _.%d\n" msg n;
+          success
+      | _ -> assert false)
+;;
+
+let trace fmt =
+  Format.kasprintf
+    (fun s ->
+      debug_var !!1 OCanren.reify (function _ ->
+          Format.printf "%s\n%!" s;
+          success))
+    fmt
+;;
+
 let rel list1 =
   let open OCanren.Std in
   fresh
     (list2 hd1 tl1 hd2 tl2)
+    (trace_index "hd1" hd1)
+    (trace_index "hd2" hd2)
+    (trace_index "tl2" tl2)
     (list1 =/= list2)
     (list1 === hd1 % tl1)
     (list2 === hd2 % tl2)
+    trace_diseq
+    (trace " hd2 === 1")
     (hd2 === !!1)
+    trace_diseq
+    (trace " tl2 === []") (* bad behaviour starts now *)
     (tl2 === nil ())
     (hd1 === !!1)
-    (tl1 === nil ())
+    (debug_line __LINE__)
+    trace_diseq
+    (tl1 === nil ()) (* crashes here *)
+    (debug_line __LINE__)
 ;;
 
 (* let () = [%tester run_r [%show GT.int GT.list] (Std.List.reify reify) 1 (fun q -> rel q)] *)
diff --git a/src/core/Disequality.ml b/src/core/Disequality.ml
index 6b49d7db..4a678991 100644
--- a/src/core/Disequality.ml
+++ b/src/core/Disequality.ml
@@ -19,6 +19,11 @@
 (* to avoid clash with Std.List (i.e. logic list) *)
 module List = Stdlib.List
 
+let log fmt =
+  if false
+  then Format.kasprintf (Format.printf "%s\n%!") fmt
+  else Format.ifprintf Format.std_formatter fmt
+
 module Answer =
   struct
     module S = Set.Make(Term)
@@ -125,14 +130,15 @@ module Disjunct :
       if Term.VarMap.is_empty d then Format.fprintf ppf "<empty>"
       else
         Format.fprintf ppf "[| ";
-        Term.VarMap.iter (fun k v ->
-          Format.fprintf ppf "@[%d =/= %s@], @," k.Term.Var.index (Term.show v)
+        Term.VarMap.iteri (fun i k v ->
+          if i<>0 then  Format.fprintf ppf ", ";
+          Format.fprintf ppf " @[%d =/= %s@]" k.Term.Var.index (Term.show v)
           ) d;
         Format.fprintf ppf " |]"
 
-    let update t =
-      ListLabels.fold_left ~init:t
-        ~f:(let open Subst.Binding in fun acc {var; term} ->
+    let update : t -> _ -> t = fun init ->
+      ListLabels.fold_left ~init
+        ~f:(fun acc {Subst.Binding.var; term} ->
           if Term.VarMap.mem var acc then
             (* in this case we have subformula of the form (x =/= t1) \/ (x =/= t2) which is always SAT *)
             raise Disequality_fulfilled
@@ -161,12 +167,32 @@ module Disjunct :
       | Fulfiled      -> raise Disequality_fulfilled
       | Violated      -> raise Disequality_violated
 
-    let rec recheck env subst t =
+    let rec recheck env subst (t: t): t  =
+      (* log "Disjunct.recheck: %a" pp t; *)
       let var, term = Term.VarMap.max_binding t in
+      (* log "       max bind index =  %d" var.Term.Var.index; *)
       let unchecked = Term.VarMap.remove var t in
+      (* log "       unchecked: %a" pp unchecked; *)
       match refine env subst (Obj.magic var) term with
-      | Fulfiled       -> raise Disequality_fulfilled
-      | Refined delta  -> update unchecked delta
+      | Fulfiled       ->
+          raise Disequality_fulfilled
+      | Refined delta  -> (
+          (* When leading terms are reified into something new, we still need to
+             do whole unification, beacuse other pairs may need walking ---
+             (we postponed walking, so som einformation may be lost.)
+             See issue #173
+          *)
+          (* log "Refined into: %a" (Format.pp_print_list Subst.Binding.pp) delta; *)
+          match Subst.unify_map env subst t with
+          | None ->
+            (* not unifiable --- always distinct *)
+            raise Disequality_fulfilled
+          | Some ([], _) -> raise Disequality_violated
+          | Some (bnds, _subst) ->
+              (* TODO(Kakadu): reconstruction of map from binding list could hurt performance  *)
+              let rez = Subst.varmap_of_bindings bnds in
+              (* log "Disjunct.recheck returns %a" pp rez; *)
+              rez)
       | Violated       ->
         if Term.VarMap.is_empty unchecked then
           raise Disequality_violated
@@ -254,9 +280,12 @@ module Conjunct :
       if M.is_empty map
       then Format.fprintf ppf "{}"
       else
+        let idx = ref 0 in
         Format.fprintf ppf "{ ";
         M.iter (fun k v ->
-          Format.fprintf ppf "@[%d: %a@],@ " k Disjunct.pp v
+          if !idx <> 0 then Format.fprintf ppf " ,";
+          Format.fprintf ppf "@[%d: %a@]" k Disjunct.pp v;
+          incr idx
         ) map;
         Format.fprintf ppf " }"
 
@@ -280,11 +309,14 @@ module Conjunct :
       ) t Term.VarMap.empty
 
     let recheck env subst t =
-      M.fold (fun id disj acc ->
+      log "Conjunct.recheck. %a" pp t;
+      let rez = M.fold (fun id disj acc ->
           try
             M.add id (Disjunct.recheck env subst disj) acc
           with Disequality_fulfilled -> acc
-      ) t M.empty
+      ) t M.empty in
+      log "rechecked =  %a" pp rez;
+      rez
 
     let merge_disjoint env subst =
       M.union (fun _ _ _ ->
@@ -375,6 +407,11 @@ type t = Conjunct.t Term.VarMap.t
 
 let empty = Term.VarMap.empty
 
+let pp ppf : t -> unit  =
+  Term.VarMap.iter (fun k v ->
+    Format.fprintf ppf "@[%d: %a@]@," k.Term.Var.index Conjunct.pp v
+    )
+
 (* merges all conjuncts (linked to different variables) into one *)
 let combine env subst cstore =
   Term.VarMap.fold (fun _ -> Conjunct.merge_disjoint env subst) cstore Conjunct.empty
@@ -394,17 +431,19 @@ let add env subst cstore x y =
     | Disequality_violated  -> None
 
 let recheck env subst cstore bs =
-  let helper var cstore =
+  let helper var cstore : t =
     try
       let conj = Term.VarMap.find var cstore in
       let cstore = Term.VarMap.remove var cstore in
       update env subst (Conjunct.recheck env subst conj) cstore
+
     with Not_found -> cstore
   in
   try
     let cstore = ListLabels.fold_left bs ~init:cstore
-      ~f:(let open Subst.Binding in fun cstore {var; term} ->
+      ~f:(fun cstore {Subst.Binding.var; term} ->
         let cstore = helper var cstore in
+        (* log "cstore = %a" pp cstore; *)
         match Env.var env term with
         | Some u -> helper u cstore
         | None   -> cstore
@@ -418,8 +457,3 @@ let project env subst cstore fv =
 
 let reify env subst cstore x =
   Conjunct.reify env subst (combine env subst cstore) x
-
-let pp ppf : t -> unit  =
-  Term.VarMap.iter (fun k v ->
-    Format.fprintf ppf "@[%d: %a@]@," k.Term.Var.index Conjunct.pp v
-    )
\ No newline at end of file
diff --git a/src/core/Subst.ml b/src/core/Subst.ml
index 8aa8b253..2b5c5c84 100644
--- a/src/core/Subst.ml
+++ b/src/core/Subst.ml
@@ -46,8 +46,18 @@ module Binding =
       if res <> 0 then res else Term.compare t p
 
     let hash {var; term} = Hashtbl.hash (Term.Var.hash var, Term.hash term)
+
+    let pp ppf {var; term} =
+      Format.fprintf ppf "{ var.idx = %d; term=%s }" var.Term.Var.index (Term.show term)
   end
 
+let varmap_of_bindings : Binding.t list -> Term.t Term.VarMap.t =
+  Stdlib.List.fold_left (fun (acc: _ Term.VarMap.t) Binding.{var;term}    ->
+    assert (not (Term.VarMap.mem var acc));
+    Term.VarMap.add var term acc
+  )
+  Term.VarMap.empty
+
 type t = Term.t Term.VarMap.t
 
 let empty = Term.VarMap.empty
@@ -145,6 +155,11 @@ let extend ~scope env subst var term  =
 
 exception Unification_failed
 
+let log fmt =
+  if false
+  then Format.kasprintf (Format.printf "%s\n%!") fmt
+  else Format.ifprintf Format.std_formatter fmt
+
 let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
   (* The idea is to do the unification and collect the unification prefix during the process *)
   let extend var term (prefix, subst) =
@@ -152,6 +167,7 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
     (Binding.({var; term})::prefix, subst)
   in
   let rec helper x y acc =
+    log "unify '%s' and '%s'" (Term.show x) (Term.show y);
     let open Term in
     fold2 x y ~init:acc
       ~fvar:(fun ((_, subst) as acc) x y ->
@@ -183,6 +199,15 @@ let apply env subst x = Obj.magic @@
     ~fvar:(fun v -> Term.repr v)
     ~fval:(fun x -> Term.repr x)
 
+let unify_map env subst map =
+  let vars, terms =
+    Term.VarMap.fold (fun v term acc -> (v :: fst acc, term :: snd acc)) map ([],[])
+  in
+  log "var   = %s" (Term.show (Obj.magic (apply env subst vars)));
+  log "terms = %s" (Term.show (Obj.magic (apply env subst terms)));
+  unify env subst (Obj.magic vars) (Obj.magic terms)
+
+
 let freevars env subst x =
   Env.freevars env @@ apply env subst x
 
diff --git a/src/core/Subst.mli b/src/core/Subst.mli
index b0312209..9054f065 100644
--- a/src/core/Subst.mli
+++ b/src/core/Subst.mli
@@ -29,8 +29,11 @@ module Binding :
     val equal : t -> t -> bool
     val compare : t -> t -> int
     val hash : t -> int
+    val pp: Format.formatter -> t -> unit
   end
 
+val varmap_of_bindings: Binding.t list -> Term.t Term.VarMap.t
+
 type t
 
 val empty : t
@@ -64,6 +67,8 @@ val freevars : Env.t -> t -> 'a -> Term.VarSet.t
  *)
 val unify : ?subsume:bool -> ?scope:Term.Var.scope -> Env.t -> t -> 'a -> 'a -> (Binding.t list * t) option
 
+val unify_map: Env.t -> t -> Term.t Term.VarMap.t -> (Binding.t list * t) option
+
 val merge_disjoint : Env.t -> t -> t -> t
 
 (* [merge env s1 s2] merges two substituions *)
diff --git a/src/core/Term.ml b/src/core/Term.ml
index b9612416..1f0bf166 100644
--- a/src/core/Term.ml
+++ b/src/core/Term.ml
@@ -90,6 +90,10 @@ module VarMap =
       match f (try Some (find k m) with Not_found -> None) with
       | Some x -> add k x m
       | None   -> remove k m
+
+    let iteri f m =
+      let i = ref 0 in
+      iter (fun k v -> f !i k v; incr i) m
   end
 
 type t = Obj.t
diff --git a/src/core/Term.mli b/src/core/Term.mli
index bf41ffa5..e99fd6f4 100644
--- a/src/core/Term.mli
+++ b/src/core/Term.mli
@@ -67,6 +67,9 @@ module VarMap :
     include Map.S with type key = Var.t
 
     val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
+
+    val iteri: (int -> key -> 'a -> unit) -> 'a t -> unit
+
   end
 
 (* [t] type of untyped OCaml term *)

From 0515231557fd9b5418342342da239c5a9a115757 Mon Sep 17 00:00:00 2001
From: "Dmitrii.Kosarev a.k.a. Kakadu" <Dmitrii.Kosarev@pm.me>
Date: Tue, 24 Dec 2024 14:01:27 +0300
Subject: [PATCH 8/8] Promote tests for issue #173

Signed-off-by: Dmitrii.Kosarev a.k.a. Kakadu <Dmitrii.Kosarev@pm.me>
---
 regression/test002.t           |  6 +++---
 regression/test005.t           |  8 +++----
 regression/test006.t           |  4 ++--
 regression/test011.t           |  4 ++--
 regression/test014.t           | 18 ++++++++--------
 regression_ppx/test014.t       | 32 ++++++++++++++++++++++++++++
 regression_ppx/test014diseq.ml | 38 +++++++++++++++++++++++++++++++++-
 7 files changed, 89 insertions(+), 21 deletions(-)

diff --git a/regression/test002.t b/regression/test002.t
index 99ef14d0..c3abc17a 100644
--- a/regression/test002.t
+++ b/regression/test002.t
@@ -1,7 +1,7 @@
   $ ./test002sort.exe
-  [O; O; _.140]
-  [O; O; _.140 [=/= O]]
-  [O; O; _.157 [=/= O]]
+  [O; O; _.138]
+  [O; O; _.136 [=/= O]]
+  [O; O; _.153 [=/= O]]
   [O; S (O); S (_.497)]
   [O; S (O); S (_.516 [=/= O])]
   [O; S (O); S (_.110)]
diff --git a/regression/test005.t b/regression/test005.t
index dbb8b0a5..85d225fd 100644
--- a/regression/test005.t
+++ b/regression/test005.t
@@ -19,14 +19,14 @@
   q=[("x", V ("y")) | _.13];
   }
   fun q -> infero (abs varX (v varX)) q, 1 answer {
-  q=Arr (_.21, _.21);
+  q=Arr (_.18, _.18);
   }
   fun q -> infero (abs varF (abs varX (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (Arr (_.54, _.26), Arr (_.54, _.26));
+  q=Arr (Arr (_.30, _.26), Arr (_.30, _.26));
   }
   fun q -> infero (abs varX (abs varF (app (v varF) (v varX)))) q, 1 answer {
-  q=Arr (_.64, Arr (Arr (_.64, _.26), _.26));
+  q=Arr (_.30, Arr (Arr (_.30, _.26), _.26));
   }
   fun q -> infero q (arr (p varX) (p varX)), 1 answer {
-  q=Abs (_.30, V (_.30));
+  q=Abs (_.29, V (_.29));
   }
diff --git a/regression/test006.t b/regression/test006.t
index 1d0e4012..f56d607c 100644
--- a/regression/test006.t
+++ b/regression/test006.t
@@ -24,10 +24,10 @@
   q=V ("x");
   }
   fun q -> evalo (app q (v varX)) (v varX), 1 answer {
-  q=Abs (_.59, V (_.59));
+  q=Abs (_.44, V (_.44));
   }
   fun q r -> evalo (app r q) (v varX), 1 answer {
-  q=V ("x"); r=Abs (_.68, V (_.68));
+  q=V ("x"); r=Abs (_.54, V (_.54));
   }
   fun q r s -> a_la_quine q r s, 2 answers {
   q=Abs (_.668, V (_.668)); r=Abs (_.668, V (_.668)); s=Abs (_.668, V (_.668));
diff --git a/regression/test011.t b/regression/test011.t
index 43190636..a4a7a153 100644
--- a/regression/test011.t
+++ b/regression/test011.t
@@ -174,7 +174,7 @@
   fun q ->
     OCanren.Fresh.two
       (fun x y -> delay (fun () -> conj (!![x; y] === q) (y =/= x))), all answers {
-  q=[_.11 [=/= _.12]; _.12];
+  q=[_.11; _.12 [=/= _.11]];
   }
   fun q ->
     OCanren.Fresh.two
@@ -247,7 +247,7 @@
   fun x ->
     OCanren.Fresh.two
       (fun y z -> delay (fun () -> conj (x =/= !![y; !2]) (x === !![z; !2]))), all answers {
-  q=[_.12; 2];
+  q=[_.12 [=/= _.11]; 2];
   }
   fun q -> distincto (!2 % (!3 %< q)), all answers {
   q=_.35 [=/= 2; =/= 3];
diff --git a/regression/test014.t b/regression/test014.t
index 8c5cbfb0..c1f784a2 100644
--- a/regression/test014.t
+++ b/regression/test014.t
@@ -28,18 +28,18 @@
   q=[_.13 | _.14]; r=[]; s=[];
   q=[1]; r=[_.15 | _.16]; s=[_.15 | _.16];
   q=[_.17; _.18 | _.19]; r=[1]; s=[_.17; _.18 | _.19];
-  q=[0; 1]; r=[_.43; _.33 | _.34]; s=[0; _.43; _.33 | _.34];
-  q=[0; 0; 1]; r=[_.97; _.76 | _.77]; s=[0; 0; _.97; _.76 | _.77];
+  q=[0; 1]; r=[_.28; _.33 | _.34]; s=[0; _.28; _.33 | _.34];
+  q=[0; 0; 1]; r=[_.69; _.76 | _.77]; s=[0; 0; _.69; _.76 | _.77];
   q=[1; _.102 | _.103]; r=[0; 1]; s=[0; 1; _.102 | _.103];
-  q=[0; 0; 0; 1]; r=[_.207; _.164 | _.165]; s=[0; 0; 0; _.207; _.164 | _.165];
+  q=[0; 0; 0; 1]; r=[_.149; _.164 | _.165]; s=[0; 0; 0; _.149; _.164 | _.165];
   q=[1; _.192 | _.193]; r=[0; 0; 1]; s=[0; 0; 1; _.192 | _.193];
   q=[0; 1; _.218 | _.219]; r=[0; 1]; s=[0; 0; 1; _.218 | _.219];
-  q=[0; 0; 0; 0; 1]; r=[_.437; _.343 | _.344]; s=[0; 0; 0; 0; _.437; _.343 | _.344];
+  q=[0; 0; 0; 0; 1]; r=[_.314; _.343 | _.344]; s=[0; 0; 0; 0; _.314; _.343 | _.344];
   q=[1; _.375 | _.376]; r=[0; 0; 0; 1]; s=[0; 0; 0; 1; _.375 | _.376];
   q=[0; 1; _.401 | _.402]; r=[0; 0; 1]; s=[0; 0; 0; 1; _.401 | _.402];
   q=[0; 0; 1; _.459 | _.460]; r=[0; 1]; s=[0; 0; 0; 1; _.459 | _.460];
   q=[1; 1]; r=[1; 1]; s=[1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 1]; r=[_.904; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.904; _.713 | _.714];
+  q=[0; 0; 0; 0; 0; 1]; r=[_.656; _.713 | _.714]; s=[0; 0; 0; 0; 0; _.656; _.713 | _.714];
   q=[1; _.745 | _.746]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.745 | _.746];
   q=[0; 1; _.778 | _.779]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 1; _.778 | _.779];
   q=[0; 0; 1; _.834 | _.835]; r=[0; 0; 1]; s=[0; 0; 0; 0; 1; _.834 | _.835];
@@ -48,7 +48,7 @@
   q=[0; 1; 1]; r=[1; 1]; s=[0; 1; 0; 0; 1];
   q=[1; 1]; r=[1; 1; 1]; s=[1; 0; 1; 0; 1];
   q=[1; 1]; r=[0; 1; 1]; s=[0; 1; 0; 0; 1];
-  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1860; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1860; _.1493 | _.1494];
+  q=[0; 0; 0; 0; 0; 0; 1]; r=[_.1360; _.1493 | _.1494]; s=[0; 0; 0; 0; 0; 0; _.1360; _.1493 | _.1494];
   q=[1; _.1523 | _.1524]; r=[0; 0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1523 | _.1524];
   q=[0; 1; _.1553 | _.1554]; r=[0; 0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1553 | _.1554];
   q=[0; 0; 1; _.1607 | _.1608]; r=[0; 0; 0; 1]; s=[0; 0; 0; 0; 0; 1; _.1607 | _.1608];
@@ -64,11 +64,11 @@
   q=[1]; r=[0; 1];
   q=[0; 1]; r=[0; 0; 1];
   q=[1; 1]; r=[0; 1; 1];
-  q=[1; _.653; 1]; r=[0; 1; _.653; 1];
+  q=[1; _.225; 1]; r=[0; 1; _.225; 1];
   q=[0; 0; 1]; r=[0; 0; 0; 1];
   q=[0; 1; 1]; r=[0; 0; 1; 1];
-  q=[1; _.1001; _.408; 1]; r=[0; 1; _.1001; _.408; 1];
-  q=[0; 1; _.1243; 1]; r=[0; 0; 1; _.1243; 1];
+  q=[1; _.247; _.408; 1]; r=[0; 1; _.247; _.408; 1];
+  q=[0; 1; _.408; 1]; r=[0; 0; 1; _.408; 1];
   q=[0; 0; 0; 1]; r=[0; 0; 0; 0; 1];
   }
   fun q r -> lelo q r, 15 answers {
diff --git a/regression_ppx/test014.t b/regression_ppx/test014.t
index 61fd08bb..e71eccae 100644
--- a/regression_ppx/test014.t
+++ b/regression_ppx/test014.t
@@ -1,3 +1,35 @@
   $ ./test014diseq.exe
   rel, 1 answer {
+  hd1 = _.12
+  hd2 = _.14
+  tl2 = _.15
+  10: { 0: [|  10 =/= _.11 |] }
+  
+  11: { 0: [|  11 =/= boxed 0 <_.12, _.13> |] }
+  
+  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+  
+   hd2 === 1
+  15: { 0: [|  14 =/= _.12,  15 =/= _.13 |] }
+  
+   tl2 === []
+  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+  
+  47
+  13: { 0: [|  12 =/= int<1>,  13 =/= int<0> |] }
+  
+  }
+  fun _ ->
+    fresh x
+      ((Std.list Fun.id [!< x; !< x]) =/=
+         (Std.list Fun.id [!< (!! 1); !< (!! 2)])), 1 answer {
+  q=_.10;
+  }
+  fun q ->
+    fresh (x y) (trace_index "x" x) (trace_index "y" y) ((x % y) === q)
+      ((x % y) =/= (Std.list Fun.id [!! 1; x]))
+      (y === (Std.list Fun.id [!! 2])) success, 1 answer {
+  x = _.11
+  y = _.12
+  q=[_.11; 2];
   }
diff --git a/regression_ppx/test014diseq.ml b/regression_ppx/test014diseq.ml
index 4d52a13c..3461120f 100644
--- a/regression_ppx/test014diseq.ml
+++ b/regression_ppx/test014diseq.ml
@@ -32,14 +32,17 @@ let rel list1 =
     (trace_index "hd2" hd2)
     (trace_index "tl2" tl2)
     (list1 =/= list2)
+    trace_diseq
     (list1 === hd1 % tl1)
+    trace_diseq
     (list2 === hd2 % tl2)
     trace_diseq
     (trace " hd2 === 1")
     (hd2 === !!1)
     trace_diseq
-    (trace " tl2 === []") (* bad behaviour starts now *)
+    (trace " tl2 === []")
     (tl2 === nil ())
+    trace_diseq
     (hd1 === !!1)
     (debug_line __LINE__)
     trace_diseq
@@ -49,3 +52,36 @@ let rel list1 =
 
 (* let () = [%tester run_r [%show GT.int GT.list] (Std.List.reify reify) 1 (fun q -> rel q)] *)
 let () = run_r (Std.List.reify reify) ([%show: GT.int logic Std.List.logic] ()) 1 q qh (REPR rel)
+
+let () =
+  let open Std in
+  run_r
+    (Std.List.reify reify)
+    ([%show: GT.int logic Std.List.logic] ())
+    1
+    q
+    qh
+    (REPR (fun _ -> fresh x (Std.list Fun.id [ !<x; !<x ] =/= Std.list Fun.id [ !<(!!1); !<(!!2) ])))
+;;
+
+let () =
+  let open OCanren.Std in
+  run_r
+    (Std.List.reify reify)
+    ([%show: GT.int logic Std.List.logic] ())
+    1
+    q
+    qh
+    (REPR
+       (fun q ->
+         fresh
+           (x y)
+           (trace_index "x" x)
+           (trace_index "y" y)
+           (x % y === q)
+           (x % y =/= Std.list Fun.id [ !!1; x ])
+           (* trace_diseq *)
+           (y === Std.list Fun.id [ !!2 ])
+           (* trace_diseq *)
+           success))
+;;