Simplify the typechecking of RULES

Not only does this fix Trac #5853, but it also eliminate
the horrid SimplEqsOnly part of the constraint simplifier.

The new plan is described in TcRules
 Note [Simplifying RULE constraints]

4 files changed, 179 insertions, 228 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a2e0b993ed..4496eef729 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -233,12 +233,9 @@ lookupInInertsStage :: SimplifierStage
 lookupInInertsStage ct
   | isWantedCt ct
   = do { is <- getTcSInerts
-       ; ctxt <- getTcSContext
        ; case lookupInInerts is (ctPred ct) of
            Just ct_cached 
-             | (not $ isDerivedCt ct) && (not $ simplEqsOnly ctxt) 
-               -- Don't share if we are simplifying a RULE 
-               -- see Note [Simplifying RULE lhs constraints]
+             |  not (isDerivedCt ct)
              -> setEvBind (ctId ct) (EvId (ctId ct_cached)) >> 
                 return Stop
            _ -> continueWith ct }
@@ -682,15 +679,10 @@ interactWithInertsStage :: WorkItem -> TcS StopOrContinue
 -- Precondition: if the workitem is a CTyEqCan then it will not be able to 
 -- react with anything at this stage. 
 interactWithInertsStage wi 
-  = do { ctxt <- getTcSContext
-       ; if simplEqsOnly ctxt && not (isCFunEqCan wi) then 
-                    -- Why not just "simplEqsOnly"? See Note [SimplEqsOnly and InteractWithInerts]
-             return (ContinueWith wi)
-         else 
-           do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
-              ; rels <- extractRelevantInerts wi 
-              ; traceTcS "relevant inerts are:" $ ppr rels
-              ; foldlBagM interact_next (ContinueWith wi) rels } }
+  = do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
+       ; rels <- extractRelevantInerts wi 
+       ; traceTcS "relevant inerts are:" $ ppr rels
+       ; foldlBagM interact_next (ContinueWith wi) rels }
 
   where interact_next Stop atomic_inert 
           = updInertSetTcS atomic_inert >> return Stop
@@ -719,33 +711,6 @@ interactWithInertsStage wi
 
 \end{code}
 
-Note [SimplEqsOnly and InteractWithInerts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-It may be possible when we are simplifying a RULE that we have two wanted constraints
-of the form: 
-  [W] c1 : F Int ~ Bool
-  [W] c2 : F Int ~ alpha
-
-When we simplify RULES we only do equality reactions (simplEqsOnly). So the question is:
-are we allowed to do type family interactions? We definitely do not want to apply top-level
-family and dictionary instances but what should we do with the constraint set above? 
-
-Suppose that c1 gets processed first and enters the inert. Remember that he will enter a 
-CtFamHead map with (F Int) as the index. Now c2 comes along, we can't add him to the inert
-set since it has exactly the same key, so we'd better react him with the inert c1. In fact 
-one might think that we should react him anyway to learn that (alpha ~ Bool). This is why
-we allow CFunEqCan's to perform reactions with the inerts. 
-
-If we don't allow this, we will try to add both elements to the inert set and will panic! 
-The relevant example that fails when we don't allow such family reactions is:
-
-        indexed_types/should_compile/T2291.hs
-
-NB: In previous versions of TcInteract the extra guard (not (isCFunEqCan wi)) was not there 
-but family reactions were actually happening earlier, during canonicalization. So the behaviour 
-has not changed -- previously this tricky point was completely lost and worked by accident.
-
 \begin{code}
 --------------------------------------------
 
@@ -1441,12 +1406,8 @@ topReactionsStage workItem
 tryTopReact :: WorkItem -> TcS StopOrContinue
 tryTopReact wi 
  = do { inerts <- getTcSInerts
-      ; ctxt   <- getTcSContext
-      ; if simplEqsOnly ctxt then 
-          return (ContinueWith wi) 
-        else 
-          do { tir <- doTopReact inerts wi
-             ; case tir of 
+      ; tir <- doTopReact inerts wi
+      ; case tir of 
                  NoTopInt 
                      -> return (ContinueWith wi)
                  SomeTopInt rule what_next 
@@ -1455,7 +1416,7 @@ tryTopReact wi
                              vcat [ ptext (sLit "Top react:") <+> text rule
                                   , text "WorkItem =" <+> ppr wi ]
                            ; return what_next }
-             } }
+      }
 
 data TopInteractResult 
  = NoTopInt
diff --git a/compiler/typecheck/TcRules.lhs b/compiler/typecheck/TcRules.lhs
index 5e935c2459..4f2dab07fe 100644
--- a/compiler/typecheck/TcRules.lhs
+++ b/compiler/typecheck/TcRules.lhs
@@ -23,8 +23,10 @@ import TcType
 import TcHsType
 import TcExpr
 import TcEnv
+import TcEvidence( TcEvBinds(..) )
 import Type
 import Id
+import NameEnv( emptyNameEnv )
 import Name
 import Var
 import VarSet
@@ -50,6 +52,82 @@ an example (test simplCore/should_compile/rule2.hs) produced by Roman:
 
 He wanted the rule to typecheck.
 
+Note [Simplifying RULE constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+On the LHS of transformation rules we only simplify only equalities,
+but not dictionaries.  We want to keep dictionaries unsimplified, to
+serve as the available stuff for the RHS of the rule.  We *do* want to
+simplify equalities, however, to detect ill-typed rules that cannot be
+applied.
+
+Implementation: the TcSFlags carried by the TcSMonad controls the
+amount of simplification, so simplifyRuleLhs just sets the flag
+appropriately.
+
+Example.  Consider the following left-hand side of a rule
+	f (x == y) (y > z) = ...
+If we typecheck this expression we get constraints
+	d1 :: Ord a, d2 :: Eq a
+We do NOT want to "simplify" to the LHS
+	forall x::a, y::a, z::a, d1::Ord a.
+	  f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
+Instead we want	
+	forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
+	  f ((==) d2 x y) ((>) d1 y z) = ...
+
+Here is another example:
+	fromIntegral :: (Integral a, Num b) => a -> b
+	{-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
+In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
+we *dont* want to get
+	forall dIntegralInt.
+	   fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
+because the scsel will mess up RULE matching.  Instead we want
+	forall dIntegralInt, dNumInt.
+	  fromIntegral Int Int dIntegralInt dNumInt = id Int
+
+Even if we have 
+	g (x == y) (y == z) = ..
+where the two dictionaries are *identical*, we do NOT WANT
+	forall x::a, y::a, z::a, d1::Eq a
+	  f ((==) d1 x y) ((>) d1 y z) = ...
+because that will only match if the dict args are (visibly) equal.
+Instead we want to quantify over the dictionaries separately.
+
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.  
+
+Also note that we can't solve the LHS constraints in isolation:
+Example   foo :: Ord a => a -> a
+	  foo_spec :: Int -> Int
+          {-# RULE "foo"  foo = foo_spec #-}
+Here, it's the RHS that fixes the type variable
+
+HOWEVER, under a nested implication things are different
+Consider
+  f :: (forall a. Eq a => a->a) -> Bool -> ...
+  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
+       f b True = ...
+    #-}
+Here we *must* solve the wanted (Eq a) from the given (Eq a)
+resulting from skolemising the agument type of g.  So we 
+revert to SimplCheck when going under an implication.  
+
+
+------------------------ So the plan is this -----------------------
+
+* Step 1: Simplify the LHS and RHS constraints all together in one bag
+          We do this to discover all unification equalities
+
+* Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
+          the ones we will quantify over, and the others
+
+* Step 3: Decide on the type varialbes to quantify over
+
+* Step 4: Simplify the LHS and RHS constraints separately, using the
+          quantified constraint sas givens
+
+
 \begin{code}
 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
 tcRules decls = mapM (wrapLocM tcRule) decls
@@ -62,52 +140,71 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
     	-- Note [Typechecking rules]
        ; vars <- tcRuleBndrs hs_bndrs
        ; let (id_bndrs, tv_bndrs) = partition (isId . snd) vars
-       ; (lhs', lhs_lie, rhs', rhs_lie, rule_ty)
+       ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
             <- tcExtendTyVarEnv2 tv_bndrs $
                tcExtendIdEnv2    id_bndrs $
-               do { ((lhs', rule_ty), lhs_lie) <- captureConstraints (tcInferRho lhs)
-                  ; (rhs', rhs_lie) <- captureConstraints (tcMonoExpr rhs rule_ty)
-                  ; return (lhs', lhs_lie, rhs', rhs_lie, rule_ty) }
-
-       ; (lhs_dicts, lhs_ev_binds, rhs_ev_binds) 
-             <- simplifyRule name (map snd tv_bndrs) lhs_lie rhs_lie
-
-	-- IMPORTANT!  We *quantify* over any dicts that appear in the LHS
-	-- Reason: 
-	--	(a) The particular dictionary isn't important, because its value
-	--	   depends only on the type
-	--		e.g	gcd Int $fIntegralInt
-	--         Here we'd like to match against (gcd Int any_d) for any 'any_d'
-	--
-	--	(b) We'd like to make available the dictionaries bound 
-	--	    on the LHS in the RHS, so quantifying over them is good
-	--	    See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
+               do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
+                  ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
+                  ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
 
+       ; (lhs_evs, other_lhs_wanted) <- simplifyRule name lhs_wanted rhs_wanted
+
+	-- Now figure out what to quantify over
+	-- c.f. TcSimplify.simplifyInfer
 	-- We quantify over any tyvars free in *either* the rule
 	--  *or* the bound variables.  The latter is important.  Consider
 	--	ss (x,(y,z)) = (x,z)
 	--	RULE:  forall v. fst (ss v) = fst v
 	-- The type of the rhs of the rule is just a, but v::(a,(b,c))
 	--
-	-- We also need to get the free tyvars of the LHS; but we do that
+	-- We also need to get the completely-uconstrained tyvars of
+	-- the LHS, lest they otherwise get defaulted to Any; but we do that
 	-- during zonking (see TcHsSyn.zonkRule)
 
-       ; let tpl_ids    = lhs_dicts ++ map snd id_bndrs
+       ; let tpl_ids    = lhs_evs ++ map snd id_bndrs
              forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
-
-	     -- Now figure out what to quantify over
-	     -- c.f. TcSimplify.simplifyInfer
        ; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
        ; gbl_tvs           <- tcGetGlobalTyVars	     -- Already zonked
        ; let tvs_to_quantify = varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
        ; qkvs <- kindGeneralize $ tyVarsOfTypes (map tyVarKind tvs_to_quantify)
        ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
+       ; let qtkvs = qkvs ++ qtvs
+       ; traceTc "tcRule" (vcat [ doubleQuotes (ftext name)
+                                , ppr forall_tvs
+                                , ppr qtvs
+                                , ppr rule_ty
+                                , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] 
+                  ])
+
+           -- Simplify the RHS constraints
+       ; loc           <- getCtLoc (RuleSkol name)
+       ; rhs_binds_var <- newTcEvBinds
+       ; emitImplication $ Implic { ic_untch  = NoUntouchables
+                                  , ic_env    = emptyNameEnv
+                                  , ic_skols  = qtkvs
+                                  , ic_given  = lhs_evs
+                                  , ic_wanted = rhs_wanted
+                                  , ic_insol  = insolubleWC rhs_wanted
+                                  , ic_binds  = rhs_binds_var
+                                  , ic_loc    = loc } 
+
+           -- For the LHS constraints we must solve the remaining constraints
+           -- (a) so that we report insoluble ones
+           -- (b) so that we bind any soluble ones
+       ; lhs_binds_var <- newTcEvBinds
+       ; emitImplication $ Implic { ic_untch  = NoUntouchables
+                                  , ic_env    = emptyNameEnv
+                                  , ic_skols  = qtkvs
+                                  , ic_given  = lhs_evs
+                                  , ic_wanted = other_lhs_wanted
+                                  , ic_insol  = insolubleWC other_lhs_wanted
+                                  , ic_binds  = lhs_binds_var
+                                  , ic_loc    = loc } 
 
-       	      -- The tv_bndrs are already skolems, so no need to zonk them
        ; return (HsRule name act
-		    (map (RuleBndr . noLoc) (qkvs ++ qtvs ++ tpl_ids))
-		    (mkHsDictLet lhs_ev_binds lhs') fv_lhs
-		    (mkHsDictLet rhs_ev_binds rhs') fv_rhs) }
+		    (map (RuleBndr . noLoc) (qtkvs ++ tpl_ids))
+		    (mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
+		    (mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }
 
 tcRuleBndrs :: [RuleBndr Name] -> TcM [(Name, Var)]
 tcRuleBndrs [] 
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index b3a64e3b14..e1dbfa378c 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -39,7 +39,7 @@ module TcSMonad (
     tryTcS, nestImplicTcS, recoverTcS,
     wrapErrTcS, wrapWarnTcS,
 
-    SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
+    SimplContext(..), isInteractive, performDefaulting,
 
     -- Getting and setting the flattening cache
     getFlatCache, updFlatCache, addToSolved, 
@@ -803,30 +803,20 @@ type TcsUntouchables = (Untouchables,TcTyVarSet)
 \begin{code}
 data SimplContext
   = SimplInfer SDoc	   -- Inferring type of a let-bound thing
-  | SimplRuleLhs RuleName  -- Inferring type of a RULE lhs
   | SimplInteractive	   -- Inferring type at GHCi prompt
   | SimplCheck SDoc	   -- Checking a type signature or RULE rhs
 
 instance Outputable SimplContext where
   ppr (SimplInfer d)   = ptext (sLit "SimplInfer") <+> d
   ppr (SimplCheck d)   = ptext (sLit "SimplCheck") <+> d
-  ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 
 isInteractive :: SimplContext -> Bool
 isInteractive SimplInteractive = True
 isInteractive _                = False
 
-simplEqsOnly :: SimplContext -> Bool
--- Simplify equalities only, not dictionaries
--- This is used for the LHS of rules; ee
--- Note [Simplifying RULE lhs constraints] in TcSimplify
-simplEqsOnly (SimplRuleLhs {}) = True
-simplEqsOnly _                 = False
-
 performDefaulting :: SimplContext -> Bool
 performDefaulting (SimplInfer {})   = False
-performDefaulting (SimplRuleLhs {}) = False
 performDefaulting SimplInteractive  = True
 performDefaulting (SimplCheck {})   = True
 
@@ -960,7 +950,7 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
                                , tcs_untch       = inner_untch
                                , tcs_count       = count
                                , tcs_ic_depth    = idepth+1
-                               , tcs_context     = ctxtUnderImplic ctxt 
+                               , tcs_context     = ctxt 
                                , tcs_inerts      = new_inert_var
                                , tcs_worklist    = wl_var 
                                -- NB: worklist is going to be empty anyway, 
@@ -974,12 +964,6 @@ recoverTcS (TcS recovery_code) (TcS thing_inside)
   = TcS $ \ env ->
     TcM.recoverM (recovery_code env) (thing_inside env)
 
-ctxtUnderImplic :: SimplContext -> SimplContext
--- See Note [Simplifying RULE lhs constraints] in TcSimplify
-ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") 
-                                               <+> doubleQuotes (ftext n))
-ctxtUnderImplic ctxt              = ctxt
-
 tryTcS :: TcS a -> TcS a
 -- Like runTcS, but from within the TcS monad 
 -- Completely afresh inerts and worklist, be careful! 
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 26d4c9f124..e6a4fd2f79 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -22,13 +22,13 @@ import TcSMonad
 import TcInteract 
 import Inst
 import Unify	( niFixTvSubst, niSubstTvSet )
+import Type     ( classifyPredType, PredTree(..) )
 import Var
 import VarSet
 import VarEnv 
 import TcEvidence
 import TypeRep
 import Name
-import NameEnv	( emptyNameEnv )
 import Bag
 import ListSetOps
 import Util
@@ -527,150 +527,59 @@ over implicit parameters. See the predicate isFreeWhenInferring.
 *                                                                                 *
 ***********************************************************************************
 
-Note [Simplifying RULE lhs constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-On the LHS of transformation rules we only simplify only equalities,
-but not dictionaries.  We want to keep dictionaries unsimplified, to
-serve as the available stuff for the RHS of the rule.  We *do* want to
-simplify equalities, however, to detect ill-typed rules that cannot be
-applied.
-
-Implementation: the TcSFlags carried by the TcSMonad controls the
-amount of simplification, so simplifyRuleLhs just sets the flag
-appropriately.
-
-Example.  Consider the following left-hand side of a rule
-	f (x == y) (y > z) = ...
-If we typecheck this expression we get constraints
-	d1 :: Ord a, d2 :: Eq a
-We do NOT want to "simplify" to the LHS
-	forall x::a, y::a, z::a, d1::Ord a.
-	  f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
-Instead we want	
-	forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
-	  f ((==) d2 x y) ((>) d1 y z) = ...
+See note [Simplifying RULE consraints] in TcRule
 
-Here is another example:
-	fromIntegral :: (Integral a, Num b) => a -> b
-	{-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
-In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
-we *dont* want to get
-	forall dIntegralInt.
-	   fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
-because the scsel will mess up RULE matching.  Instead we want
-	forall dIntegralInt, dNumInt.
-	  fromIntegral Int Int dIntegralInt dNumInt = id Int
-
-Even if we have 
-	g (x == y) (y == z) = ..
-where the two dictionaries are *identical*, we do NOT WANT
-	forall x::a, y::a, z::a, d1::Eq a
-	  f ((==) d1 x y) ((>) d1 y z) = ...
-because that will only match if the dict args are (visibly) equal.
-Instead we want to quantify over the dictionaries separately.
-
-In short, simplifyRuleLhs must *only* squash equalities, leaving
-all dicts unchanged, with absolutely no sharing.  
-
-HOWEVER, under a nested implication things are different
-Consider
-  f :: (forall a. Eq a => a->a) -> Bool -> ...
-  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
-       f b True = ...
-    #-}
-Here we *must* solve the wanted (Eq a) from the given (Eq a)
-resulting from skolemising the agument type of g.  So we 
-revert to SimplCheck when going under an implication.  
+Note [RULE quanfification over equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Decideing which equalities to quantify over is tricky:
+ * We do not want to quantify over insoluble equalities (Int ~ Bool)
+    (a) because we prefer to report a LHS type error
+    (b) because if such things end up in 'givens' we get a bogus
+        "inaccessible code" error
+
+ * But we do want to quantify over things like (a ~ F b), where
+   F is a type function.
+
+The difficulty is that it's hard to tell what is insoluble!
+So we see whether the simplificaiotn step yielded any type errors,
+and if so refrain from quantifying over *any* equalites.
 
 \begin{code}
 simplifyRule :: RuleName 
-             -> [TcTyVar]		-- Explicit skolems
              -> WantedConstraints	-- Constraints from LHS
              -> WantedConstraints	-- Constraints from RHS
-             -> TcM ([EvVar], 		-- LHS dicts
-                     TcEvBinds,		-- Evidence for LHS
-                     TcEvBinds)		-- Evidence for RHS
--- See Note [Simplifying RULE lhs constraints]
-simplifyRule name tv_bndrs lhs_wanted rhs_wanted
-  = do { loc        <- getCtLoc (RuleSkol name)
+             -> TcM ([EvVar], WantedConstraints)   -- LHS evidence varaibles
+-- See Note [Simplifying RULE constraints] in TcRule
+simplifyRule name lhs_wanted rhs_wanted
+  = do { zonked_all <- zonkWC (lhs_wanted `andWC` rhs_wanted)
+       ; let doc = ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
+	     untch = NoUntouchables
+             	 -- We allow ourselves to unify environment 
+		 -- variables; hence NoUntouchables
+
+       ; (resid_wanted, _) <- runTcS (SimplInfer doc) untch emptyInert emptyWorkList $
+              solveWanteds zonked_all
+
        ; zonked_lhs <- zonkWC lhs_wanted
-       ; let untch = NoUntouchables
-	     	 -- We allow ourselves to unify environment 
-		 -- variables; hence *no untouchables*
-
--- DV: SPJ and I discussed a new plan here:
--- Step 1: Simplify everything in the same bag
--- Step 2: zonk away the lhs constraints and get only the non-trivial ones
--- Step 3: do the implications with these constraints
--- This will have the advantage that (i) we no longer need simplEqsOnly flag
--- and (ii) will fix problems appearing from touchable unification variables
--- in the givens, manifested by #5853
--- TODO ... 
-
-       ; (lhs_results, lhs_binds)
-              <- runTcS (SimplRuleLhs name) untch emptyInert emptyWorkList $
-                 solveWanteds zonked_lhs
 
+       ; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
+             quantify_me  -- Note [RULE quantification over equalities]
+               | insolubleWC resid_wanted = quantify_insol
+               | otherwise                = quantify_normal
+
+             quantify_insol ct = not (isEqPred (ctPred ct))
+
+             quantify_normal ct
+               | EqPred t1 t2 <- classifyPredType (ctPred ct)
+               = not (t1 `eqType` t2)
+               | otherwise
+               = True
+             
        ; traceTc "simplifyRule" $
-         vcat [ text "zonked_lhs"   <+> ppr zonked_lhs 
-              , text "lhs_results"  <+> ppr lhs_results
-              , text "lhs_binds"    <+> ppr lhs_binds 
-              , text "rhs_wanted"   <+> ppr rhs_wanted ]
-
-
-       -- Don't quantify over equalities (judgement call here)
-       ; let (eqs, dicts) = partitionBag (isEqPred . ctPred)
-                                         (wc_flat lhs_results)
-             lhs_dicts    = map ctId (bagToList dicts)
-                                 -- Dicts and implicit parameters
-                                 -- NB: dicts come from lhs_results which
-                                 -- are all Wanted, hence have ids, hence
-                                 -- it's fine to call ctId on them
-
-           -- Fail if we have not got down to unsolved flats
-       ; ev_binds_var <- newTcEvBinds
-       ; emitImplication $ Implic { ic_untch  = untch
-                                  , ic_env    = emptyNameEnv
-                                  , ic_skols  = tv_bndrs
-                                  , ic_given  = lhs_dicts
-                                  , ic_wanted = lhs_results { wc_flat = eqs }
-                                  , ic_insol  = insolubleWC lhs_results
-                                  , ic_binds  = ev_binds_var
-                                  , ic_loc    = loc }
-
-	     -- Notice that we simplify the RHS with only the explicitly
-	     -- introduced skolems, allowing the RHS to constrain any 
-	     -- unification variables.
-	     -- Then, and only then, we call zonkQuantifiedTypeVariables
-	     -- Example   foo :: Ord a => a -> a
-	     --		  foo_spec :: Int -> Int
-	     --		  {-# RULE "foo"  foo = foo_spec #-}
-	     --	    Here, it's the RHS that fixes the type variable
-
-	     -- So we don't want to make untouchable the type
-	     -- variables in the envt of the RHS, because they include
-	     -- the template variables of the RULE
-
-	     -- Hence the rather painful ad-hoc treatement here
-       ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
-       ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
-       ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
-            WC { wc_flat = emptyBag
-               , wc_insol = emptyBag
-               , wc_impl = unitBag $
-                    Implic { ic_untch   = NoUntouchables
-                            , ic_env    = emptyNameEnv
-                            , ic_skols  = tv_bndrs
-                            , ic_given  = lhs_dicts
-                            , ic_wanted = rhs_wanted
-                            , ic_insol  = insolubleWC rhs_wanted
-                            , ic_binds  = rhs_binds_var
-                            , ic_loc    = loc } }
-       ; rhs_binds2 <- readTcRef evb_ref
-
-       ; return ( lhs_dicts
-                , EvBinds lhs_binds 
-                , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
+         vcat [ text "zonked_lhs" <+> ppr zonked_lhs 
+              , text "q_cts"      <+> ppr q_cts ]
+
+       ; return (map ctId (bagToList q_cts), zonked_lhs { wc_flat = non_q_cts }) }
 \end{code}