From f0e291a84d926f25b89930c0b466946e5403d551 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Mon, 14 Dec 2020 13:59:13 +0000
Subject: [PATCH] Prevent infinite loop unifying variable with itself

---
 src/Propa/Prolog/Unify.hs | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs
index 9adb323..50991ec 100644
--- a/src/Propa/Prolog/Unify.hs
+++ b/src/Propa/Prolog/Unify.hs
@@ -93,11 +93,12 @@ unifyTerm t1 t2 = do
   t1' <- lookupTerm t1
   t2' <- lookupTerm t2
   case (t1', t2') of
-    (TStat s1, TStat s2) -> unifyStat s1 s2
-    (TInt i1, TInt i2)   -> guard $ i1 == i2
-    (TVar v, t)          -> bindTerm v t
-    (t, TVar v)          -> bindTerm v t
-    (_, _)               -> empty
+    (TStat s1, TStat s2)      -> unifyStat s1 s2
+    (TInt i1, TInt i2)        -> guard $ i1 == i2
+    (TVar v, TVar w) | v == w -> pure ()
+    (TVar v, t)               -> bindTerm v t
+    (t, TVar v)               -> bindTerm v t
+    (_, _)                    -> empty
 
 unifyTerms :: [Term Int] -> [Term Int] -> UniM ()
 unifyTerms t1 t2 = do