x+5~y ==> [x:=y-5] only when x+5~y is a given constraint

CHANGELOG.md

@@ -4,7 +4,7 @@
 * Find more unifications:
   * `(2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]`
   * `a^d * a^e ~ a^c ==> [c := d + e]`
-  * `x+5 ~ y ==> [x := y - 5]`
+  * `x+5 ~ y ==> [x := y - 5]`, but only when `x+5 ~ y` is a given constraint
 
 ## 0.4.1 *February 4th 2016*
 * Find more unifications:

src/GHC/TypeLits/Normalise/Unify.hs

@@ -341,12 +341,9 @@ unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))
     | i < j     = unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))
     | i > j     = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)
 
-unifiers' ct (S [P [I i],P [V v]]) s2 = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]])) ct]
-unifiers' ct s1 (S [P [I i],P [V v]]) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]])) ct]
-
 -- (a + c) ~ (b + c) ==> [a := b]
 unifiers' ct (S ps1)       (S ps2)
-    | null psx  = []
+    | null psx  = unifiers'' ct (S ps1) (S ps2)
     | otherwise = unifiers' ct (S ps1'') (S ps2'')
   where
     ps1'  = ps1 \\ psx
@@ -357,6 +354,12 @@ unifiers' ct (S ps1)       (S ps2)
           | otherwise = ps2'
     psx = intersect ps1 ps2
 
+unifiers'' ct (S [P [I i],P [V v]]) s2
+  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]])) ct]
+unifiers'' ct s1 (S [P [I i],P [V v]])
+  | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]])) ct]
+unifiers'' _ _ _ = []
+
 collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
 collectBases = fmap unzip . traverse go . unP
   where