-rewriteEqLHS (co1,xi1) (cv2,gw,xi2)
- = do { cv2' <- if isWanted gw then
- do { cv2' <- newWantedCoVar xi1 xi2
- ; setWantedCoBind cv2 $
- co1 `mkTransCoercion` mkCoVarCoercion cv2'
- ; return cv2' }
- else newGivOrDerCoVar xi1 xi2 $
- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
+-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
+-- depends on whether the left or the right equality comes from the inert set.
+-- We must:
+-- prefer to create (xi2 ~ xi1) if the first comes from the inert
+-- prefer to create (xi1 ~ xi2) if the second comes from the inert
+rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
+ = do { cv2' <- case (isWanted gw, which) of
+ (True,LeftComesFromInert) ->
+ do { cv2' <- newWantedCoVar xi2 xi1
+ ; setWantedCoBind cv2 $
+ co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
+ ; return cv2' }
+ (True,RightComesFromInert) ->
+ do { cv2' <- newWantedCoVar xi1 xi2
+ ; setWantedCoBind cv2 $
+ co1 `mkTransCoercion` mkCoVarCoercion cv2'
+ ; return cv2' }
+ (False,LeftComesFromInert) ->
+ newGivOrDerCoVar xi2 xi1 $
+ mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
+ (False,RightComesFromInert) ->
+ newGivOrDerCoVar xi1 xi2 $
+ mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2