Remove canSolve in favour of canRewrite

There was no useful distinction; a simple refactoring.

compiler/typecheck/TcInteract.lhs

@@ -275,6 +275,7 @@ ppr_kicked :: Int -> SDoc
 ppr_kicked 0 = empty
 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out")) 
 \end{code}
+
 Note [Spontaneously solved in TyBinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we encounter a constraint ([W] alpha ~ tau) which can be spontaneously solved,
@@ -698,7 +699,7 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
        ; emitWorkNC d2 ctevs 
        ; return (IRWorkItemConsumed "FunEq/FunEq") }
 
-  | fl2 `canSolve` fl1
+  | w_solves_i
   = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
     do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
@@ -724,9 +725,9 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
     fl1 = ctEvFlavour ev1
     fl2 = ctEvFlavour ev2
 
-    i_solves_w = fl1 `canSolve` fl2 
-    w_solves_i = fl2 `canSolve` fl1 
-    
+    i_solves_w = fl1 `canRewrite` fl2 
+    w_solves_i = fl2 `canRewrite` fl1 
+
 
 doInteractWithInert _ _ = return (IRKeepGoing "NOP")
 \end{code}

compiler/typecheck/TcRnTypes.lhs

@@ -66,7 +66,7 @@ module TcRnTypes(
         CtEvidence(..),
         mkGivenLoc,
         isWanted, isGiven,
-        isDerived, canSolve, canRewrite,
+        isDerived, canRewrite,
         CtFlavour(..), ctEvFlavour, ctFlavour,
 
         -- Pretty printing
@@ -1249,6 +1249,7 @@ data Implication
 
       ic_given  :: [EvVar],      -- Given evidence variables
                                  --   (order does not matter)
+                                 -- See Invariant (GivenInv) in TcType
 
       ic_env   :: TcLclEnv,      -- Gives the source location and error context
                                  -- for the implicatdion, and hence for all the
@@ -1428,8 +1429,8 @@ isDerived :: CtEvidence -> Bool
 isDerived (CtDerived {}) = True
 isDerived _              = False
 
-canSolve :: CtFlavour -> CtFlavour -> Bool
--- canSolve ctid1 ctid2
+canRewrite :: CtFlavour -> CtFlavour -> Bool
+-- canRewrite ctid1 ctid2
 -- The constraint ctid1 can be used to solve ctid2
 -- "to solve" means a reaction where the active parts of the two constraints match.
 --  active(F xis ~ xi) = F xis
@@ -1437,18 +1438,13 @@ canSolve :: CtFlavour -> CtFlavour -> Bool
 --  active(D xis)      = D xis
 --  active(IP nm ty)   = nm
 --
--- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
+-- NB:  either (a `canRewrite` b) or (b `canRewrite` a) must hold
 -----------------------------------------
-canSolve Given   _       = True
-canSolve Wanted  Derived = True
-canSolve Wanted  Wanted  = True
-canSolve Derived Derived = True  -- Derived can't solve wanted/given
-canSolve _ _ = False                       -- No evidence for a derived, anyway
-
-canRewrite :: CtFlavour -> CtFlavour -> Bool
--- canRewrite ct1 ct2
--- The equality constraint ct1 can be used to rewrite inside ct2
-canRewrite = canSolve
+canRewrite Given   _       = True
+canRewrite Wanted  Derived = True
+canRewrite Wanted  Wanted  = True
+canRewrite Derived Derived = True  -- Derived can't solve wanted/given
+canRewrite _ _ = False             -- No evidence for a derived, anyway
 \end{code}
 
 %************************************************************************

compiler/typecheck/TcSMonad.lhs

@@ -28,7 +28,7 @@ module TcSMonad (
     isWanted, isDerived, 
     isGivenCt, isWantedCt, isDerivedCt, 
 
-    canRewrite, canSolve,
+    canRewrite, 
     mkGivenLoc, 
 
     TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality 

compiler/typecheck/TcType.lhs

@@ -404,6 +404,12 @@ Note [Untouchable type variables]
 * A unification variable is *touchable* if its level number
   is EQUAL TO that of its immediate parent implication.
 
+* INVARIANT
+    (GivenInv)  The free variables of the ic_given of an
+                implication are all untouchable; ie their level
+                numbers are LESS THAN the ic_untch of the implication
+
+
 Note [Skolem escape prevention]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We only unify touchable unification variables.  Because of