diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a6ae1cc6c1e7a47a729720233be1c9aa927ad159..a8637b7b254137eb632b0c3b9607c20623a8a202 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/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}
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 6502d6d914dcaa22e16b541e9faff5e3677855f1..41da1d4f7dbce3dd428170038f133378074fdd1d 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/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}
 
 %************************************************************************
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 1dc8713a1424c3f20ff84b7ada006988dd4dca04..a7bb3f4d8bbf31008223aa2f3ebf51e2206a43a8 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/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 
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 751b2eea7b3c11c488ebc20bd51b0adb7dc94863..deab2a2e53578b1be59204886ac34d50cfcbbba4 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/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