Big tidy-up of deriving code

[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 2347d37..342114b 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -15,7 +15,7 @@ module TcSimplify (
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,

-       bindInstsOfLocalFuns
+       bindInstsOfLocalFuns, bindIrreds,

     ) where
 
 #include "HsVersions.h"
     ) where
 
 #include "HsVersions.h"

@@ -28,11 +28,10 @@ import Inst
 import TcEnv
 import InstEnv
 import TcGadt
 import TcEnv
 import InstEnv
 import TcGadt

-import TcMType

 import TcType
 import TcType

+import TcMType

 import TcIface
 import Var
 import TcIface
 import Var

-import TyCon

 import Name
 import NameSet
 import Class
 import Name
 import NameSet
 import Class

@@ -657,42 +656,81 @@ tcSimplifyInfer
        :: SDoc
        -> TcTyVarSet           -- fv(T); type vars
        -> [Inst]               -- Wanted
        :: SDoc
        -> TcTyVarSet           -- fv(T); type vars
        -> [Inst]               -- Wanted

-       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
-               TcDictBinds,    -- Bindings
-               [TcId])         -- Dict Ids that must be bound here (zonked)
+       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked and quantified)
+               [Inst],         -- Dict Ids that must be bound here (zonked)
+               TcDictBinds)    -- Bindings

        -- Any free (escaping) Insts are tossed into the environment
 \end{code}
 
 
 \begin{code}
        -- Any free (escaping) Insts are tossed into the environment
 \end{code}
 
 
 \begin{code}

-tcSimplifyInfer doc tau_tvs wanted_lie
-  = do { let try_me inst | isDict inst = Stop                  -- Dicts
-                         | otherwise   = ReduceMe NoSCs        -- Lits, Methods, 
-                                                               -- and impliciation constraints
-               -- In an effort to make the inferred types simple, we try 
-               -- to squeeze out implication constraints if we can.
-               -- See Note [Squashing methods]
-
-       ; (binds1, irreds) <- checkLoop (mkRedEnv doc try_me []) wanted_lie
-
-       ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+tcSimplifyInfer doc tau_tvs wanted
+  = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+       ; wanted' <- mappM zonkInst wanted      -- Zonk before deciding quantified tyvars

        ; gbl_tvs  <- tcGetGlobalTyVars
        ; gbl_tvs  <- tcGetGlobalTyVars

-       ; let preds = fdPredsOfInsts irreds
+       ; let preds = fdPredsOfInsts wanted'

              qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
              qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs

-             (free, bound) = partition (isFreeWhenInferring qtvs) irreds
+             (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+       ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
+       ; extendLIEs free

 
 

-               -- Remove redundant superclasses from 'bound'
-               -- The 'Stop' try_me result does not do so, 
-               -- see Note [No superclasses for Stop]
+               -- To make types simple, reduce as much as possible

        ; let try_me inst = ReduceMe AddSCs
        ; let try_me inst = ReduceMe AddSCs

-       ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) bound
+       ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound

 
 

-       ; extendLIEs free
-       ; return (varSetElems qtvs, binds1 `unionBags` binds2, map instToId irreds) }
+       ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+
+       -- We can't abstract over implications
+       ; let (dicts, implics) = partition isDict irreds
+       ; loc <- getInstLoc (ImplicOrigin doc)
+       ; implic_bind <- bindIrreds loc qtvs' dicts implics
+
+       ; return (qtvs', dicts, binds `unionBags` implic_bind) }

        -- NB: when we are done, we might have some bindings, but
        -- the final qtvs might be empty.  See Note [NO TYVARS] below.
 \end{code}
 
        -- NB: when we are done, we might have some bindings, but
        -- the final qtvs might be empty.  See Note [NO TYVARS] below.
 \end{code}
 

+\begin{code}
+-----------------------------------------------------------
+-- tcSimplifyInferCheck is used when we know the constraints we are to simplify
+-- against, but we don't know the type variables over which we are going to quantify.
+-- This happens when we have a type signature for a mutually recursive group
+tcSimplifyInferCheck
+        :: InstLoc
+        -> TcTyVarSet          -- fv(T)
+        -> [Inst]              -- Given
+        -> [Inst]              -- Wanted
+        -> TcM ([TyVar],       -- Fully zonked, and quantified
+                TcDictBinds)   -- Bindings
+
+tcSimplifyInferCheck loc tau_tvs givens wanteds
+  = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+
+       -- Figure out which type variables to quantify over
+       -- You might think it should just be the signature tyvars,
+       -- but in bizarre cases you can get extra ones
+       --      f :: forall a. Num a => a -> a
+       --      f x = fst (g (x, head [])) + 1
+       --      g a b = (b,a)
+       -- Here we infer g :: forall a b. a -> b -> (b,a)
+       -- We don't want g to be monomorphic in b just because
+       -- f isn't quantified over b.
+       ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
+       ; all_tvs <- zonkTcTyVarsAndFV all_tvs
+       ; gbl_tvs <- tcGetGlobalTyVars
+       ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
+               -- We could close gbl_tvs, but its not necessary for
+               -- soundness, and it'll only affect which tyvars, not which
+               -- dictionaries, we quantify over
+
+       ; qtvs' <- zonkQuantifiedTyVars qtvs
+
+               -- Now we are back to normal (c.f. tcSimplCheck)
+       ; implic_bind <- bindIrreds loc qtvs' givens irreds
+
+       ; return (qtvs', binds `unionBags` implic_bind) }
+\end{code}
+

 Note [Squashing methods]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Be careful if you want to float methods more:
 Note [Squashing methods]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Be careful if you want to float methods more:

@@ -771,10 +809,9 @@ tcSimplifyCheck    :: InstLoc
                -> [Inst]               -- Wanted
                -> TcM TcDictBinds      -- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
                -> [Inst]               -- Wanted
                -> TcM TcDictBinds      -- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 

-  = ASSERT( all isSkolemTyVar qtvs )
-    do { (binds, irreds) <- innerCheckLoop loc givens wanteds
-       ; implic_bind <- bindIrreds loc [] emptyRefinement 
-                                            qtvs givens irreds
+  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
+    do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+       ; implic_bind <- bindIrreds loc qtvs givens irreds

        ; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------
        ; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------

@@ -786,21 +823,31 @@ tcSimplifyCheckPat :: InstLoc
                   -> [Inst]            -- Wanted
                   -> TcM TcDictBinds   -- Bindings
 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
                   -> [Inst]            -- Wanted
                   -> TcM TcDictBinds   -- Bindings
 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds

-  = ASSERT( all isSkolemTyVar qtvs )
-    do { (binds, irreds) <- innerCheckLoop loc givens wanteds
-       ; implic_bind <- bindIrreds loc co_vars reft 
-                                   qtvs givens irreds
+  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
+    do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+       ; implic_bind <- bindIrredsR loc qtvs co_vars reft 
+                                   givens irreds

        ; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------
        ; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------

-bindIrreds :: InstLoc -> [CoVar] -> Refinement
-          -> [TcTyVar] -> [Inst] -> [Inst]
-          -> TcM TcDictBinds   
+bindIrreds :: InstLoc -> [TcTyVar]
+          -> [Inst] -> [Inst]
+          -> TcM TcDictBinds
+bindIrreds loc qtvs givens irreds 
+  = bindIrredsR loc qtvs [] emptyRefinement givens irreds
+
+bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
+           -> Refinement -> [Inst] -> [Inst]
+           -> TcM TcDictBinds  

 -- Make a binding that binds 'irreds', by generating an implication
 -- constraint for them, *and* throwing the constraint into the LIE
 -- Make a binding that binds 'irreds', by generating an implication
 -- constraint for them, *and* throwing the constraint into the LIE

-bindIrreds loc co_vars reft qtvs givens irreds
+bindIrredsR loc qtvs co_vars reft givens irreds
+  | null irreds
+  = return emptyBag
+  | otherwise

   = do { let givens' = filter isDict givens
                -- The givens can include methods
   = do { let givens' = filter isDict givens
                -- The givens can include methods

+               -- See Note [Pruning the givens in an implication constraint]

 
           -- If there are no 'givens', then it's safe to 
           -- partition the 'wanteds' by their qtvs, thereby trimming irreds
 
           -- If there are no 'givens', then it's safe to 
           -- partition the 'wanteds' by their qtvs, thereby trimming irreds

@@ -861,8 +908,7 @@ makeImplicationBind loc all_tvs reft
 -----------------------------------------------------------
 topCheckLoop :: SDoc
             -> [Inst]                  -- Wanted
 -----------------------------------------------------------
 topCheckLoop :: SDoc
             -> [Inst]                  -- Wanted

-            -> TcM (TcDictBinds,
-                    [Inst])            -- Irreducible
+            -> TcM ([Inst], TcDictBinds)

 
 topCheckLoop doc wanteds
   = checkLoop (mkRedEnv doc try_me []) wanteds
 
 topCheckLoop doc wanteds
   = checkLoop (mkRedEnv doc try_me []) wanteds

@@ -873,8 +919,7 @@ topCheckLoop doc wanteds
 innerCheckLoop :: InstLoc
               -> [Inst]                -- Given
               -> [Inst]                -- Wanted
 innerCheckLoop :: InstLoc
               -> [Inst]                -- Given
               -> [Inst]                -- Wanted

-              -> TcM (TcDictBinds,
-                      [Inst])          -- Irreducible
+              -> TcM ([Inst], TcDictBinds)

 
 innerCheckLoop inst_loc givens wanteds
   = checkLoop env wanteds
 
 innerCheckLoop inst_loc givens wanteds
   = checkLoop env wanteds

@@ -915,10 +960,8 @@ with topCheckLooop.
 -----------------------------------------------------------
 checkLoop :: RedEnv
          -> [Inst]                     -- Wanted
 -----------------------------------------------------------
 checkLoop :: RedEnv
          -> [Inst]                     -- Wanted

-         -> TcM (TcDictBinds,
-                 [Inst])               -- Irreducible
--- Precondition: the try_me never returns Free
---              givens are completely rigid
+         -> TcM ([Inst], TcDictBinds)
+-- Precondition: givens are completely rigid

 
 checkLoop env wanteds
   = do { -- Givens are skolems, so no need to zonk them
 
 checkLoop env wanteds
   = do { -- Givens are skolems, so no need to zonk them

@@ -927,7 +970,7 @@ checkLoop env wanteds
        ; (improved, binds, irreds) <- reduceContext env wanteds'
 
        ; if not improved then
        ; (improved, binds, irreds) <- reduceContext env wanteds'
 
        ; if not improved then

-            return (binds, irreds)
+            return (irreds, binds)

          else do
 
        -- If improvement did some unification, we go round again.
          else do
 
        -- If improvement did some unification, we go round again.

@@ -935,8 +978,8 @@ checkLoop env wanteds
        -- Using an instance decl might have introduced a fresh type variable
        -- which might have been unified, so we'd get an infinite loop
        -- if we started again with wanteds!  See Note [LOOP]
        -- Using an instance decl might have introduced a fresh type variable
        -- which might have been unified, so we'd get an infinite loop
        -- if we started again with wanteds!  See Note [LOOP]

-       { (binds1, irreds1) <- checkLoop env irreds
-       ; return (binds `unionBags` binds1, irreds1) } }
+       { (irreds1, binds1) <- checkLoop env irreds
+       ; return (irreds1, binds `unionBags` binds1) } }

 \end{code}
 
 Note [LOOP]
 \end{code}
 
 Note [LOOP]

@@ -957,45 +1000,6 @@ on both the Lte and If constraints.  What we *can't* do is start again
 with (Max Z (S x) y)!
 
 
 with (Max Z (S x) y)!
 
 

-\begin{code}
------------------------------------------------------------
--- tcSimplifyInferCheck is used when we know the constraints we are to simplify
--- against, but we don't know the type variables over which we are going to quantify.
--- This happens when we have a type signature for a mutually recursive group
-tcSimplifyInferCheck
-        :: InstLoc
-        -> TcTyVarSet          -- fv(T)
-        -> [Inst]              -- Given
-        -> [Inst]              -- Wanted
-        -> TcM ([TcTyVar],     -- Variables over which to quantify
-                TcDictBinds)   -- Bindings
-
-tcSimplifyInferCheck loc tau_tvs givens wanteds
-  = do { (binds, irreds) <- innerCheckLoop loc givens wanteds
-
-       -- Figure out which type variables to quantify over
-       -- You might think it should just be the signature tyvars,
-       -- but in bizarre cases you can get extra ones
-       --      f :: forall a. Num a => a -> a
-       --      f x = fst (g (x, head [])) + 1
-       --      g a b = (b,a)
-       -- Here we infer g :: forall a b. a -> b -> (b,a)
-       -- We don't want g to be monomorphic in b just because
-       -- f isn't quantified over b.
-       ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
-       ; all_tvs <- zonkTcTyVarsAndFV all_tvs
-       ; gbl_tvs <- tcGetGlobalTyVars
-       ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
-               -- We could close gbl_tvs, but its not necessary for
-               -- soundness, and it'll only affect which tyvars, not which
-               -- dictionaries, we quantify over
-
-               -- Now we are back to normal (c.f. tcSimplCheck)
-       ; implic_bind <- bindIrreds loc [] emptyRefinement 
-                                          qtvs givens irreds
-       ; return (qtvs, binds `unionBags` implic_bind) }
-\end{code}
-

 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *

@@ -1048,7 +1052,7 @@ tcSimplifySuperClasses
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds

-  = do { (binds1, irreds) <- checkLoop env sc_wanteds
+  = do { (irreds, binds1) <- checkLoop env sc_wanteds

        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
        ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
        ; return binds1 }
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
        ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
        ; return binds1 }

@@ -1167,7 +1171,7 @@ tcSimplifyRestricted      -- Used for restricted binding groups
        -> [Name]               -- Things bound in this group
        -> TcTyVarSet           -- Free in the type of the RHSs
        -> [Inst]               -- Free in the RHSs
        -> [Name]               -- Things bound in this group
        -> TcTyVarSet           -- Free in the type of the RHSs
        -> [Inst]               -- Free in the RHSs

-       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
+       -> TcM ([TyVar],        -- Tyvars to quantify (zonked and quantified)

                TcDictBinds)    -- Bindings
        -- tcSimpifyRestricted returns no constraints to
        -- quantify over; by definition there are none.
                TcDictBinds)    -- Bindings
        -- tcSimpifyRestricted returns no constraints to
        -- quantify over; by definition there are none.

@@ -1175,7 +1179,7 @@ tcSimplifyRestricted      -- Used for restricted binding groups
 
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
 
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight

-  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
+  = do { wanteds' <- mappM zonkInst wanteds

 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type

@@ -1186,23 +1190,21 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- BUT do no improvement!  See Plan D above
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint
        -- BUT do no improvement!  See Plan D above
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint

-    let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
-    in
-    reduceContext env wanteds'                 `thenM` \ (_imp, _binds, constrained_dicts) ->
+       ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
+       ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'

 
        -- Next, figure out the tyvars we will quantify over
 
        -- Next, figure out the tyvars we will quantify over

-    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
-    tcGetGlobalTyVars                          `thenM` \ gbl_tvs' ->
-    mappM zonkInst constrained_dicts           `thenM` \ constrained_dicts' ->
-    let
-       constrained_tvs' = tyVarsOfInsts constrained_dicts'
-       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
+       ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+       ; gbl_tvs' <- tcGetGlobalTyVars
+       ; constrained_dicts' <- mappM zonkInst constrained_dicts
+
+       ; let constrained_tvs' = tyVarsOfInsts constrained_dicts'
+             qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')

                         `minusVarSet` constrained_tvs'
                         `minusVarSet` constrained_tvs'

-    in
-    traceTc (text "tcSimplifyRestricted" <+> vcat [
+       ; traceTc (text "tcSimplifyRestricted" <+> vcat [

                pprInsts wanteds, pprInsts constrained_dicts',
                ppr _binds,
                pprInsts wanteds, pprInsts constrained_dicts',
                ppr _binds,

-               ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) `thenM_`
+               ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])

 
        -- The first step may have squashed more methods than
        -- necessary, so try again, this time more gently, knowing the exact
 
        -- The first step may have squashed more methods than
        -- necessary, so try again, this time more gently, knowing the exact

@@ -1220,27 +1222,23 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        --
        -- At top level, we *do* squash methods becuase we want to 
        -- expose implicit parameters to the test that follows
        --
        -- At top level, we *do* squash methods becuase we want to 
        -- expose implicit parameters to the test that follows

-    let
-       is_nested_group = isNotTopLevel top_lvl
-        try_me inst | isFreeWrtTyVars qtvs inst,
-                     (is_nested_group || isDict inst) = Stop
-                   | otherwise                        = ReduceMe AddSCs
-       env = mkNoImproveRedEnv doc try_me
-   in
-    reduceContext env wanteds'   `thenM` \ (_imp, binds, irreds) ->
-    ASSERT( all (isFreeWrtTyVars qtvs) irreds )        -- None should be captured
+       ; let is_nested_group = isNotTopLevel top_lvl
+             try_me inst | isFreeWrtTyVars qtvs inst,
+                          (is_nested_group || isDict inst) = Stop
+                         | otherwise            = ReduceMe AddSCs
+             env = mkNoImproveRedEnv doc try_me
+       ; (_imp, binds, irreds) <- reduceContext env wanteds'

 
        -- See "Notes on implicit parameters, Question 4: top level"
 
        -- See "Notes on implicit parameters, Question 4: top level"

-    if is_nested_group then
-       extendLIEs irreds       `thenM_`
-        returnM (varSetElems qtvs, binds)
-    else
-       let
-           (non_ips, bad_ips) = partition isClassDict irreds
-       in    
-       addTopIPErrs bndrs bad_ips      `thenM_`
-       extendLIEs non_ips              `thenM_`
-        returnM (varSetElems qtvs, binds)
+       ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
+         if is_nested_group then
+               extendLIEs irreds
+         else do { let (bad_ips, non_ips) = partition isIPDict irreds
+                 ; addTopIPErrs bndrs bad_ips
+                 ; extendLIEs non_ips }
+
+       ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+       ; return (qtvs', binds) }

 \end{code}
 
 
 \end{code}
 
 

@@ -1437,7 +1435,7 @@ bindInstsOfLocalFuns wanteds local_ids
     returnM emptyLHsBinds
 
   | otherwise
     returnM emptyLHsBinds
 
   | otherwise

-  = do { (binds, irreds) <- checkLoop env for_me
+  = do { (irreds, binds) <- checkLoop env for_me

        ; extendLIEs not_for_me 
        ; extendLIEs irreds
        ; return binds }
        ; extendLIEs not_for_me 
        ; extendLIEs irreds
        ; return binds }

@@ -1820,10 +1818,12 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                         , red_try_me = try_me }
 
        ; traceTc (text "reduceImplication" <+> vcat
                         , red_try_me = try_me }
 
        ; traceTc (text "reduceImplication" <+> vcat

-                       [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ])
+                       [ ppr orig_avails,
+                         ppr (red_givens env), ppr extra_givens, 
+                         ppr reft, ppr wanteds, ppr avails ])

        ; avails <- reduceList env' wanteds avails
 
        ; avails <- reduceList env' wanteds avails
 

-               -- Extract the binding (no frees, because try_me never says Free)
+               -- Extract the binding

        ; (binds, irreds) <- extractResults avails wanteds
  
                -- We always discard the extra avails we've generated;
        ; (binds, irreds) <- extractResults avails wanteds
  
                -- We always discard the extra avails we've generated;

@@ -1876,6 +1876,20 @@ We can satisfy the (C Int) from the superclass of D, so we don't want
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 

+Note [Pruning the givens in an implication constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to form the implication constraint
+       forall tvs.  Eq a => Ord b
+The (Eq a) cannot contribute to the (Ord b), because it has no access to
+the type variable 'b'.  So we could filter out the (Eq a) from the givens.
+
+Doing so would be a bit tidier, but all the implication constraints get
+simplified away by the optimiser, so it's no great win.   So I don't take
+advantage of that at the moment.
+
+If you do, BE CAREFUL of wobbly type variables.
+
+

 %************************************************************************
 %*                                                                     *
                Avails and AvailHow: the pool of evidence
 %************************************************************************
 %*                                                                     *
                Avails and AvailHow: the pool of evidence

@@ -1992,9 +2006,6 @@ extractResults (Avails _ avails) wanteds
          Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
                             where
                                new_binds = addBind binds w rhs
          Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
                             where
                                new_binds = addBind binds w rhs

-       where
-         w_span = instSpan w
-         w_id = instToId w

 
     add_given avails w = extendAvailEnv avails w (Given (instToId w))
 
 
     add_given avails w = extendAvailEnv avails w (Given (instToId w))
 

@@ -2032,7 +2043,9 @@ addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails
 addRefinedGiven reft (refined_givens, avails) given
   | isDict given       -- We sometimes have 'given' methods, but they
                        -- are always optional, so we can drop them
 addRefinedGiven reft (refined_givens, avails) given
   | isDict given       -- We sometimes have 'given' methods, but they
                        -- are always optional, so we can drop them

-  , Just (co, pred) <- refinePred reft (dictPred given)
+  , let pred = dictPred given
+  , isRefineablePred pred      -- See Note [ImplicInst rigidity]
+  , Just (co, pred) <- refinePred reft pred

   = do         { new_given <- newDictBndr (instLoc given) pred
        ; let rhs = L (instSpan given) $
                    HsWrap (WpCo co) (HsVar (instToId given))
   = do         { new_given <- newDictBndr (instLoc given) pred
        ; let rhs = L (instSpan given) $
                    HsWrap (WpCo co) (HsVar (instToId given))

@@ -2043,7 +2056,30 @@ addRefinedGiven reft (refined_givens, avails) given
            -- and hopefully the optimiser will spot the duplicated work
   | otherwise
   = return (refined_givens, avails)
            -- and hopefully the optimiser will spot the duplicated work
   | otherwise
   = return (refined_givens, avails)

+\end{code}

 
 

+Note [ImplicInst rigidity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+       C :: forall ab. (Eq a, Ord b) => b -> T a
+       
+       ...(case x of C v -> <body>)...
+
+From the case (where x::T ty) we'll get an implication constraint
+       forall b. (Eq ty, Ord b) => <body-constraints>
+Now suppose <body-constraints> itself has an implication constraint 
+of form
+       forall c. <reft> => <payload>
+Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
+existential, but we probably should not apply it to the (Eq ty) because it may
+be wobbly. Hence the isRigidInst
+
+@Insts@ are ordered by their class/type info, rather than by their
+unique.  This allows the context-reduction mechanism to use standard finite
+maps to do their stuff.  It's horrible that this code is here, rather
+than with the Avails handling stuff in TcSimplify
+
+\begin{code}

 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
                                 addAvailAndSCs want_scs avails irred IsIrred
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
                                 addAvailAndSCs want_scs avails irred IsIrred

@@ -2146,7 +2182,7 @@ tc_simplify_top doc interactive wanteds
   = do { wanteds <- mapM zonkInst wanteds
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
   = do { wanteds <- mapM zonkInst wanteds
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 

-       ; (binds1, irreds1) <- topCheckLoop doc wanteds
+       ; (irreds1, binds1) <- topCheckLoop doc wanteds

 
        ; if null irreds1 then 
                return binds1
 
        ; if null irreds1 then 
                return binds1

@@ -2157,7 +2193,7 @@ tc_simplify_top doc interactive wanteds
        ; extended_default <- if interactive then return True
                              else doptM Opt_ExtendedDefaultRules
        ; disambiguate extended_default irreds1 -- Does unification
        ; extended_default <- if interactive then return True
                              else doptM Opt_ExtendedDefaultRules
        ; disambiguate extended_default irreds1 -- Does unification

-       ; (binds2, irreds2) <- topCheckLoop doc irreds1
+       ; (irreds2, binds2) <- topCheckLoop doc irreds1

 
                -- Deal with implicit parameter
        ; let (bad_ips, non_ips) = partition isIPDict irreds2
 
                -- Deal with implicit parameter
        ; let (bad_ips, non_ips) = partition isIPDict irreds2

@@ -2209,7 +2245,8 @@ disambiguate :: Bool -> [Inst] -> TcM ()
        -- The Insts are assumed to be pre-zonked
 disambiguate extended_defaulting insts
   | null defaultable_groups
        -- The Insts are assumed to be pre-zonked
 disambiguate extended_defaulting insts
   | null defaultable_groups

-  = return ()
+  = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+       ;     return () }

   | otherwise
   = do         {       -- Figure out what default types to use
          mb_defaults <- getDefaultTys
   | otherwise
   = do         {       -- Figure out what default types to use
          mb_defaults <- getDefaultTys

@@ -2220,6 +2257,7 @@ disambiguate extended_defaulting insts
                                do { integer_ty <- tcMetaTy integerTyConName
                                   ; checkWiredInTyCon doubleTyCon
                                   ; return [integer_ty, doubleTy] }
                                do { integer_ty <- tcMetaTy integerTyConName
                                   ; checkWiredInTyCon doubleTyCon
                                   ; return [integer_ty, doubleTy] }

+       ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])

        ; mapM_ (disambigGroup default_tys) defaultable_groups  }
   where
    unaries :: [(Inst,Class, TcTyVar)]  -- (C tv) constraints
        ; mapM_ (disambigGroup default_tys) defaultable_groups  }
   where
    unaries :: [(Inst,Class, TcTyVar)]  -- (C tv) constraints

@@ -2233,7 +2271,7 @@ disambiguate extended_defaulting insts
 
    defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
    defaultable_group ds@((_,_,tv):_)
 
    defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
    defaultable_group ds@((_,_,tv):_)

-       =  not (isSkolemTyVar tv)       -- Note [Avoiding spurious errors]
+       =  not (isImmutableTyVar tv)    -- Note [Avoiding spurious errors]

        && not (tv `elemVarSet` bad_tvs)
        && defaultable_classes [c | (_,c,_) <- ds]
    defaultable_group [] = panic "defaultable_group"
        && not (tv `elemVarSet` bad_tvs)
        && defaultable_classes [c | (_,c,_) <- ds]
    defaultable_group [] = panic "defaultable_group"

@@ -2306,55 +2344,31 @@ instance declarations.
 
 \begin{code}
 tcSimplifyDeriv :: InstOrigin
 
 \begin{code}
 tcSimplifyDeriv :: InstOrigin

-                -> TyCon

                -> [TyVar]      
                -> ThetaType            -- Wanted
                -> TcM ThetaType        -- Needed
                -> [TyVar]      
                -> ThetaType            -- Wanted
                -> TcM ThetaType        -- Needed

+-- Given  instance (wanted) => C inst_ty 
+-- Simplify 'wanted' as much as possible
+-- The inst_ty is needed only for the termination check

 
 

-tcSimplifyDeriv orig tc tyvars theta
-  = tcInstTyVars tyvars                        `thenM` \ (tvs, _, tenv) ->
+tcSimplifyDeriv orig tyvars theta
+  = do { (tvs, _, tenv) <- tcInstTyVars tyvars

        -- The main loop may do unification, and that may crash if 
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?
        -- The main loop may do unification, and that may crash if 
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?

-    newDictBndrsO orig (substTheta tenv theta) `thenM` \ wanteds ->
-    topCheckLoop doc wanteds                   `thenM` \ (_, irreds) ->
-
-    doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
-    doptM Opt_AllowUndecidableInstances                `thenM` \ undecidable_ok ->
-    let
-       inst_ty = mkTyConApp tc (mkTyVarTys tvs)
-       (ok_insts, bad_insts) = partition is_ok_inst irreds
-       is_ok_inst inst
-          = isDict inst        -- Exclude implication consraints
-          && (isTyVarClassPred pred || (gla_exts && ok_gla_pred pred))
-          where
-            pred = dictPred inst
-
-       ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred])
-               -- See Note [Deriving context]
-          
-       tv_set = mkVarSet tvs
-       simpl_theta = map dictPred ok_insts
-       weird_preds = [pred | pred <- simpl_theta
-                           , not (tyVarsOfPred pred `subVarSet` tv_set)]  
-
-         -- Check for a bizarre corner case, when the derived instance decl should
-         -- have form  instance C a b => D (T a) where ...
-         -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
-         -- of problems; in particular, it's hard to compare solutions for
-         -- equality when finding the fixpoint.  So I just rule it out for now.
-       
-       rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+       ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+       ; (irreds, _) <- topCheckLoop doc wanteds
+
+       ; let (dicts, non_dicts) = partition isDict irreds
+                                       -- Exclude implication consraints
+       ; addNoInstanceErrs non_dicts   -- I'm not sure if these can really happen
+
+       ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+             simpl_theta = substTheta rev_env (map dictPred dicts)

                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars
                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars

-    in
-       -- In effect, the bad and wierd insts cover all of the cases that
-       -- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv
-       --   * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance)
-       --   * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance)
-    addNoInstanceErrs bad_insts                                `thenM_`
-    mapM_ (addErrTc . badDerivedPred) weird_preds      `thenM_`
-    returnM (substTheta rev_env simpl_theta)
+
+       ; return simpl_theta }

   where
     doc = ptext SLIT("deriving classes for a data type")
 \end{code}
   where
     doc = ptext SLIT("deriving classes for a data type")
 \end{code}

@@ -2390,7 +2404,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
 
 tcSimplifyDefault theta
   = newDictBndrsO DefaultOrigin theta  `thenM` \ wanteds ->
 
 tcSimplifyDefault theta
   = newDictBndrsO DefaultOrigin theta  `thenM` \ wanteds ->

-    topCheckLoop doc wanteds           `thenM` \ (_, irreds) ->
+    topCheckLoop doc wanteds           `thenM` \ (irreds, _) ->

     addNoInstanceErrs  irreds          `thenM_`
     if null irreds then
        returnM ()
     addNoInstanceErrs  irreds          `thenM_`
     if null irreds then
        returnM ()

@@ -2628,12 +2642,6 @@ warnDefault ups default_ty
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 

--- Used for the ...Thetas variants; all top level
-badDerivedPred pred
-  = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
-         ptext SLIT("type variables that are not data type parameters"),
-         nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
-

 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
          ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
          ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),