[commit: ghc] master: Remove canSolve in favour of canRewrite (e55f516)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/e55f516766c5a0ece06f2c36dc31601dcdeb97cd/ghc

>---------------------------------------------------------------

commit e55f516766c5a0ece06f2c36dc31601dcdeb97cd
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Oct 25 14:36:37 2013 +0100

    Remove canSolve in favour of canRewrite
    
    There was no useful distinction; a simple refactoring.


>---------------------------------------------------------------

e55f516766c5a0ece06f2c36dc31601dcdeb97cd
 compiler/typecheck/TcInteract.lhs |    7 ++++---
 compiler/typecheck/TcRnTypes.lhs  |   24 ++++++++++--------------
 compiler/typecheck/TcSMonad.lhs   |    2 +-
 compiler/typecheck/TcType.lhs     |    6 ++++++
 4 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a6ae1cc..a8637b7 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,8 +725,8 @@ 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")
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 6502d6d..41da1d4 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 1dc8713..a7bb3f4 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 751b2ee..deab2a2 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