Store a SrcSpan instead of a SrcLoc inside a Name
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index 23d0b23..b9ff789 100644 (file)
@@ -15,7 +15,7 @@ module TcSimplify (
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
-       bindInstsOfLocalFuns
+       bindInstsOfLocalFuns, bindIrreds,
     ) where
 
 #include "HsVersions.h"
@@ -28,11 +28,10 @@ import Inst
 import TcEnv
 import InstEnv
 import TcGadt
-import TcMType
 import TcType
+import TcMType
 import TcIface
 import Var
-import TyCon
 import Name
 import NameSet
 import Class
@@ -398,8 +397,8 @@ When m is later unified with [], we can solve both constraints.
                Notes on implicit parameters
        --------------------------------------
 
-Question 1: can we "inherit" implicit parameters
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
 
        f x = (x::Int) + ?y
@@ -424,6 +423,21 @@ BOTTOM LINE: when *inferring types* you *must* quantify
 over implicit parameters. See the predicate isFreeWhenInferring.
 
 
+Note [Implicit parameters and ambiguity] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What type should we infer for this?
+       f x = (show ?y, x::Int)
+Since we must quantify over the ?y, the most plausible type is
+       f :: (Show a, ?y::a) => Int -> (String, Int)
+But notice that the type of the RHS is (String,Int), with no type 
+varibables mentioned at all!  The type of f looks ambiguous.  But
+it isn't, because at a call site we might have
+       let ?y = 5::Int in f 7
+and all is well.  In effect, implicit parameters are, well, parameters,
+so we can take their type variables into account as part of the
+"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
+
+
 Question 2: type signatures
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 BUT WATCH OUT: When you supply a type signature, we can't force you
@@ -642,83 +656,98 @@ tcSimplifyInfer
        :: 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}
-tcSimplifyInfer doc tau_tvs wanted_lie
-  = inferLoop doc (varSetElems tau_tvs)
-             wanted_lie                `thenM` \ (qtvs, frees, binds, irreds) ->
-
-    extendLIEs frees                                                   `thenM_`
-    returnM (qtvs, binds, map instToId irreds)
-
-inferLoop doc tau_tvs wanteds
-  =    -- Step 1
-    zonkTcTyVarsAndFV tau_tvs          `thenM` \ tau_tvs' ->
-    mappM zonkInst wanteds             `thenM` \ wanteds' ->
-    tcGetGlobalTyVars                  `thenM` \ gbl_tvs ->
-    let
-       preds = fdPredsOfInsts wanteds'
-       qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
-
-       try_me inst
-         | isFreeWhenInferring qtvs inst = Free
-         | isClassDict inst              = Irred               -- Dicts
-         | otherwise                     = ReduceMe NoSCs      -- Lits and Methods
-       env = mkRedEnv doc try_me []
-    in
-    traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, 
-                                     ppr (grow preds tau_tvs'), ppr qtvs])     `thenM_`
-               -- Step 2
-    reduceContext env wanteds'    `thenM` \ (improved, frees, binds, irreds) ->
-
-               -- Step 3
-    if not improved then
-       returnM (varSetElems qtvs, frees, binds, irreds)
-    else
-       -- If improvement did some unification, we go round again.  There
-       -- are two subtleties:
-       --   a) We start again with irreds, not 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 example [LOOP]
-       --
-       --   b) It's also essential to re-process frees, because unification
-       --      might mean that a type variable that looked free isn't now.
-       --
-       -- Hence the (irreds ++ frees)
-
-       -- However, NOTICE that when we are done, we might have some bindings, but
-       -- the final qtvs might be empty.  See [NO TYVARS] below.
-                               
-       inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
-       returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
+tcSimplifyInfer doc tau_tvs wanted
+  = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+       ; wanted' <- mappM zonkInst wanted      -- Zonk before deciding quantified tyvars
+       ; gbl_tvs  <- tcGetGlobalTyVars
+       ; let preds = fdPredsOfInsts wanted'
+             qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+             (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
+
+               -- To make types simple, reduce as much as possible
+       ; let try_me inst = ReduceMe AddSCs
+       ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
+
+       ; 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}
 
-Example [LOOP]
+\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
 
-       class If b t e r | b t e -> r
-       instance If T t e t
-       instance If F t e e
-       class Lte a b c | a b -> c where lte :: a -> b -> c
-       instance Lte Z b T
-       instance (Lte a b l,If l b a c) => Max a b c
+tcSimplifyInferCheck loc tau_tvs givens wanteds
+  = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
 
-Wanted:        Max Z (S x) y
+       -- 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
 
-Then we'll reduce using the Max instance to:
-       (Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints.  What we *can't* do is start again
-with (Max Z (S x) y)!
+       ; qtvs' <- zonkQuantifiedTyVars qtvs
 
-[NO TYVARS]
+               -- 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:
+       truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
+From an application (truncate f i) we get
+       t1 = truncate at f
+       t2 = t1 at i
+If we have also have a second occurrence of truncate, we get
+       t3 = truncate at f
+       t4 = t3 at i
+When simplifying with i,f free, we might still notice that
+t1=t3; but alas, the binding for t2 (which mentions t1)
+may continue to float out!
+
+
+Note [NO TYVARS]
+~~~~~~~~~~~~~~~~~
        class Y a b | a -> b where
            y :: a -> X b
        
@@ -743,9 +772,9 @@ The net effect of [NO TYVARS]
 \begin{code}
 isFreeWhenInferring :: TyVarSet -> Inst        -> Bool
 isFreeWhenInferring qtvs inst
-  =  isFreeWrtTyVars qtvs inst         -- Constrains no quantified vars
-  && isInheritableInst inst            -- And no implicit parameter involved
-                                       -- (see "Notes on implicit parameters")
+  =  isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
+  && isInheritableInst inst    -- and no implicit parameter involved
+                               --   see Note [Inheriting implicit parameters]
 
 {-     No longer used (with implication constraints)
 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
@@ -780,10 +809,9 @@ tcSimplifyCheck    :: InstLoc
                -> [Inst]               -- Wanted
                -> TcM TcDictBinds      -- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
-  = ASSERT( all isSkolemTyVar qtvs )
-    do { (binds, irreds) <- innerCheckLoop loc AddSCs givens wanteds
-       ; implic_bind <- makeImplicationBind 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) }
 
 -----------------------------------------------------------
@@ -795,53 +823,76 @@ tcSimplifyCheckPat :: InstLoc
                   -> [Inst]            -- Wanted
                   -> TcM TcDictBinds   -- Bindings
 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
-  = ASSERT( all isSkolemTyVar qtvs )
-    do { (binds, irreds) <- innerCheckLoop loc AddSCs givens wanteds
-       ; implic_bind <- makeImplicationBind 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) }
 
 -----------------------------------------------------------
-makeImplicationBind :: 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
-makeImplicationBind 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
+               -- See Note [Pruning the givens in an implication constraint]
 
-          -- If there are no 'givens', then it's safe to 
+          -- If there are no 'givens' *and* the refinement is empty
+          -- (the refinement is like more givens), then it's safe to 
           -- partition the 'wanteds' by their qtvs, thereby trimming irreds
           -- See Note [Freeness and implications]
-       ; irreds <- if null givens'
-            then do
-               { let qtv_set = mkVarSet qtvs
-                     (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
-               ; extendLIEs frees
-               ; return real_irreds }
-            else 
-               return irreds
-
-       -- If there are no irreds, we are done!
-       ; if null irreds then 
-               return emptyBag
-         else do
+       ; irreds' <- if null givens' && isEmptyRefinement reft
+                    then do
+                       { let qtv_set = mkVarSet qtvs
+                             (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
+                       ; extendLIEs frees
+                       ; return real_irreds }
+                    else return irreds
+       
+       ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
+       ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
+                       -- This call does the real work
+                       -- If irreds' is empty, it does something sensible
+       ; extendLIEs implics
+       ; return bind } 
 
-       -- Otherwise we must generate a binding
-       -- The binding looks like
-       --      (ir1, .., irn) = f qtvs givens
-       -- where f is (evidence for) the new implication constraint
-       --
-       -- This binding must line up the 'rhs' in reduceImplication
 
-       { uniq <- newUnique 
+makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
+                   -> [Inst] -> [Inst]
+                   -> TcM ([Inst], TcDictBinds)
+-- Make a binding that binds 'irreds', by generating an implication
+-- constraint for them, *and* throwing the constraint into the LIE
+-- The binding looks like
+--     (ir1, .., irn) = f qtvs givens
+-- where f is (evidence for) the new implication constraint
+--     f :: forall qtvs. {reft} givens => (ir1, .., irn)
+-- qtvs includes coercion variables
+--
+-- This binding must line up the 'rhs' in reduceImplication
+makeImplicationBind loc all_tvs reft
+                   givens      -- Guaranteed all Dicts
+                   irreds
+ | null irreds                 -- If there are no irreds, we are done
+ = return ([], emptyBag)
+ | otherwise                   -- Otherwise we must generate a binding
+ = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
-       ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
-             name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
+       ; let name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 
-                                        tci_given = givens',
+                                        tci_given = givens,
                                         tci_wanted = irreds, tci_loc = loc }
 
        ; let n_irreds = length irreds
@@ -849,22 +900,19 @@ makeImplicationBind loc co_vars reft qtvs givens irreds
              tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
              pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-             co  = mkWpApps (map instToId givens') <.> mkWpTyApps (mkTyVarTys all_tvs)
+             co  = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
              bind | n_irreds==1 = VarBind (head irred_ids) rhs
                   | otherwise   = PatBind { pat_lhs = L span pat, 
                                             pat_rhs = unguardedGRHSs rhs, 
                                             pat_rhs_ty = tup_ty,
                                             bind_fvs = placeHolderNames }
        ; -- pprTrace "Make implic inst" (ppr implic_inst) $
-         extendLIE implic_inst
-       ; return (unitBag (L span bind)) }}
-
+         return ([implic_inst], unitBag (L span bind)) }
 
 -----------------------------------------------------------
 topCheckLoop :: SDoc
             -> [Inst]                  -- Wanted
-            -> TcM (TcDictBinds,
-                    [Inst])            -- Irreducible
+            -> TcM ([Inst], TcDictBinds)
 
 topCheckLoop doc wanteds
   = checkLoop (mkRedEnv doc try_me []) wanteds
@@ -872,19 +920,18 @@ topCheckLoop doc wanteds
     try_me inst = ReduceMe AddSCs
 
 -----------------------------------------------------------
-innerCheckLoop :: InstLoc -> WantSCs
+innerCheckLoop :: InstLoc
               -> [Inst]                -- Given
               -> [Inst]                -- Wanted
-              -> TcM (TcDictBinds,
-                      [Inst])          -- Irreducible
+              -> TcM ([Inst], TcDictBinds)
 
-innerCheckLoop inst_loc want_scs givens wanteds
+innerCheckLoop inst_loc givens wanteds
   = checkLoop env wanteds
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
-    try_me inst | isMethodOrLit inst = ReduceMe want_scs
-               | otherwise          = Irred
+    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+               | otherwise          = Stop
        -- When checking against a given signature 
        -- we MUST be very gentle: Note [Check gently]
 \end{code}
@@ -917,66 +964,45 @@ with topCheckLooop.
 -----------------------------------------------------------
 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
         wanteds' <- mappM zonkInst wanteds
 
-       ; (improved, _frees, binds, irreds) <- reduceContext env wanteds'
+       ; (improved, binds, irreds) <- reduceContext env wanteds'
 
-       ; ASSERT( null _frees )
-
-         if not improved then
-            return (binds, irreds)
+       ; if not improved then
+            return (irreds, binds)
          else do
 
-       { (binds1, irreds1) <- checkLoop env irreds
-       ; return (binds `unionBags` binds1, irreds1) } }
+       -- If improvement did some unification, we go round again.
+       -- We start again with irreds, not 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]
+       { (irreds1, binds1) <- checkLoop env irreds
+       ; return (irreds1, binds `unionBags` binds1) } }
 \end{code}
 
+Note [LOOP]
+~~~~~~~~~~~
+       class If b t e r | b t e -> r
+       instance If T t e t
+       instance If F t e e
+       class Lte a b c | a b -> c where lte :: a -> b -> c
+       instance Lte Z b T
+       instance (Lte a b l,If l b a c) => Max a b c
 
-\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 AddSCs givens wanteds
+Wanted:        Max Z (S x) y
 
-       -- 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
+Then we'll reduce using the Max instance to:
+       (Lte Z (S x) l, If l (S x) Z y)
+and improve by binding l->T, after which we can do some reduction
+on both the Lte and If constraints.  What we *can't* do is start again
+with (Max Z (S x) y)!
 
-               -- Now we are back to normal (c.f. tcSimplCheck)
-       ; implic_bind <- makeImplicationBind loc [] emptyRefinement 
-                                            qtvs givens irreds
-       ; return (qtvs, binds `unionBags` implic_bind) }
-\end{code}
 
 
 %************************************************************************
@@ -1030,7 +1056,7 @@ tcSimplifySuperClasses
        -> [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 }
@@ -1149,7 +1175,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
-       -> 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.
@@ -1157,9 +1183,9 @@ tcSimplifyRestricted      -- Used for restricted binding groups
 
 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
+       -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
        -- variables as possible, and we don't want to stop
        -- at (say) Monad (ST s), because that reduces
@@ -1168,29 +1194,40 @@ 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
-    let env = mkNoImproveRedEnv doc reduceMe
-    in
-    reduceContext env wanteds'                 `thenM` \ (_imp, _frees, _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
-    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')
-                        `minusVarSet` constrained_tvs'
-    in
-    traceTc (text "tcSimplifyRestricted" <+> vcat [
-               pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts',
+       ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+       ; gbl_tvs' <- tcGetGlobalTyVars
+       ; constrained_dicts' <- mappM zonkInst constrained_dicts
+
+       ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
+                               -- As in tcSimplifyInfer
+
+               -- Do not quantify over constrained type variables:
+               -- this is the monomorphism restriction
+             constrained_tvs' = tyVarsOfInsts constrained_dicts'
+             qtvs = qtvs1 `minusVarSet` constrained_tvs'
+             pp_bndrs = pprWithCommas (quotes . ppr) bndrs
+
+       -- Warn in the mono
+       ; warn_mono <- doptM Opt_WarnMonomorphism
+       ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
+                (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
+                               <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
+                       ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
+
+       ; traceTc (text "tcSimplifyRestricted" <+> vcat [
+               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
        -- set of type variables to quantify over.
        --
-       -- We quantify only over constraints that are captured by qtvs';
+       -- We quantify only over constraints that are captured by qtvs;
        -- these will just be a subset of non-dicts.  This in contrast
        -- to normal inference (using isFreeWhenInferring) in which we quantify over
        -- all *non-inheritable* constraints too.  This implements choice
@@ -1202,27 +1239,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
-    let
-       is_nested_group = isNotTopLevel top_lvl
-        try_me inst | isFreeWrtTyVars qtvs' inst,
-                     (is_nested_group || isDict inst) = Free
-                   | otherwise                        = ReduceMe AddSCs
-       env = mkNoImproveRedEnv doc try_me
-   in
-    reduceContext env wanteds'   `thenM` \ (_imp, frees, binds, irreds) ->
-    ASSERT( null irreds )
+       ; 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"
-    if is_nested_group then
-       extendLIEs frees        `thenM_`
-        returnM (varSetElems qtvs', binds)
-    else
-       let
-           (non_ips, bad_ips) = partition isClassDict frees
-       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}
 
 
@@ -1359,7 +1392,7 @@ tcSimplifyIPs given_ips wanteds
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me given_ips'
-       ; (improved, _frees, binds, irreds) <- reduceContext env wanteds'
+       ; (improved, binds, irreds) <- reduceContext env wanteds'
 
        ; if not improved then 
                ASSERT( all is_free irreds )
@@ -1373,7 +1406,7 @@ tcSimplifyIPs given_ips wanteds
     is_free inst = isFreeWrtIPs ip_set inst
 
        -- Simplify any methods that mention the implicit parameter
-    try_me inst | is_free inst = Irred
+    try_me inst | is_free inst = Stop
                | otherwise    = ReduceMe NoSCs
 \end{code}
 
@@ -1419,7 +1452,7 @@ bindInstsOfLocalFuns wanteds local_ids
     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 }
@@ -1434,7 +1467,7 @@ bindInstsOfLocalFuns wanteds local_ids
                                                -- so it's worth building a set, so that
                                                -- lookup (in isMethodFor) is faster
     try_me inst | isMethod inst = ReduceMe NoSCs
-               | otherwise     = Irred
+               | otherwise     = Stop
 \end{code}
 
 
@@ -1492,13 +1525,9 @@ data WhatToDo
                        -- message of any kind.
                        -- It might be quite legitimate such as (Eq a)!
 
- | Irred               -- Return as irreducible unless it can
+ | Stop                -- Return as irreducible unless it can
                        -- be reduced to a constant in one step
-
- | Free                          -- Return as free
-
-reduceMe :: Inst -> WhatToDo
-reduceMe inst = ReduceMe AddSCs
+                       -- Do not add superclasses; see 
 
 data WantSCs = NoSCs | AddSCs  -- Tells whether we should add the superclasses
                                -- of a predicate when adding it to the avails
@@ -1517,7 +1546,6 @@ data WantSCs = NoSCs | AddSCs     -- Tells whether we should add the superclasses
 reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
-                     [Inst],           -- Free
                      TcDictBinds,      -- Dictionary bindings
                      [Inst])           -- Irreducible
 
@@ -1537,7 +1565,7 @@ reduceContext env wanteds
        ; avails <- reduceList env wanteds init_state
 
        ; let improved = availsImproved avails
-       ; (binds, irreds, frees) <- extractResults avails wanteds
+       ; (binds, irreds) <- extractResults avails wanteds
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
@@ -1546,12 +1574,11 @@ reduceContext env wanteds
             text "wanted" <+> ppr wanteds,
             text "----",
             text "avails" <+> pprAvails avails,
-            text "frees" <+> ppr frees,
             text "improved =" <+> ppr improved,
             text "----------------------"
             ]))
 
-       ; return (improved, frees, binds, irreds) }
+       ; return (improved, binds, irreds) }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
 tcImproveOne avails inst
@@ -1624,8 +1651,7 @@ reduce env wanted avails
 
   | otherwise
   = case red_try_me env wanted of {
-      Free  -> try_simple addFree              -- It's free so just chuck it upstairs
-    ; Irred -> try_simple (addIrred AddSCs)    -- Assume want superclasses
+    ; Stop -> try_simple (addIrred NoSCs)      -- See Note [No superclasses for Stop]
 
     ; ReduceMe want_scs ->     -- It should be reduced
        reduceInst env avails wanted      `thenM` \ (avails, lookup_result) ->
@@ -1695,7 +1721,7 @@ At first I had a gross hack, whereby I simply did not add superclass constraints
 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
 becuase it lost legitimate superclass sharing, and it still didn't do the job:
 I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an Irred
+simplifier got two bites a the cherry... so something seemed to be an Stop
 first time, but reducible next time.
 
 Now we implement the Right Solution, which is to check for loops directly 
@@ -1809,28 +1835,37 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                         , 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
 
                -- Extract the binding
-       ; (binds, irreds, _frees) <- extractResults avails wanteds
-                       -- No frees, because try_me never says Free
+       ; (binds, irreds) <- extractResults avails wanteds
  
+               -- We always discard the extra avails we've generated;
+               -- but we remember if we have done any (global) improvement
+       ; let ret_avails = updateImprovement orig_avails avails
+
+       ; if isEmptyLHsBinds binds then         -- No progress
+               return (ret_avails, NoInstance)
+         else do
+       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+                       -- This binding is useless if the recursive simplification
+                       -- made no progress; but currently we don't try to optimise that
+                       -- case.  After all, we only try hard to reduce at top level, or
+                       -- when inferring types.
+
        ; let   dict_ids = map instToId extra_givens
-               co  = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet binds
+               co  = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
                rhs = mkHsWrap co payload
                loc = instLocSpan inst_loc
                payload | isSingleton wanteds = HsVar (instToId (head wanteds))
                        | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
 
                -- If there are any irreds, we back off and return NoInstance
-               -- Either way, we discard the extra avails we've generated;
-               -- but we remember if we have done any (global) improvement
-       ; let ret_avails = updateImprovement orig_avails avails
-       ; case irreds of
-               []    -> return (ret_avails, GenInst [] (L loc rhs))
-               other -> return (ret_avails, NoInstance)
-  }
+       ; return (ret_avails, GenInst implic_insts (L loc rhs))
+  } }
 \end{code}
 
 Note [Freeness and implications]
@@ -1858,6 +1893,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!
 
+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
@@ -1874,8 +1923,7 @@ type ImprovementDone = Bool       -- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
-  = IsFree             -- Used for free Insts
-  | IsIrred            -- Used for irreducible dictionaries,
+  = IsIrred            -- Used for irreducible dictionaries,
                        -- which are going to be lambda bound
 
   | Given TcId                 -- Used for dictionaries for which we have a binding
@@ -1898,7 +1946,6 @@ instance Outputable AvailHow where
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
-pprAvail IsFree                = text "Free"
 pprAvail IsIrred       = text "Irred"
 pprAvail (Given x)     = text "Given" <+> ppr x
 pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
@@ -1947,77 +1994,54 @@ dependency analyser can sort them out later
 extractResults :: Avails
               -> [Inst]                -- Wanted
               -> TcM ( TcDictBinds,    -- Bindings
-                       [Inst],         -- Irreducible ones
-                       [Inst])         -- Free ones
+                       [Inst])         -- Irreducible ones
 
 extractResults (Avails _ avails) wanteds
-  = go avails emptyBag [] [] wanteds
+  = go avails emptyBag [] wanteds
   where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
-       -> TcM (TcDictBinds, [Inst], [Inst])
-    go avails binds irreds frees [] 
-      = returnM (binds, irreds, frees)
+    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
+       -> TcM (TcDictBinds, [Inst])
+    go avails binds irreds [] 
+      = returnM (binds, irreds)
 
-    go avails binds irreds frees (w:ws)
+    go avails binds irreds (w:ws)
       = case findAvailEnv avails w of
          Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
-                       go avails binds irreds frees ws
+                       go avails binds irreds ws
 
-         Just IsFree  -> go (add_free avails w)  binds irreds     (w:frees) ws
-         Just IsIrred -> go (add_given avails w) binds (w:irreds) frees     ws
+         Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
 
-         Just (Given id) -> go avails new_binds irreds frees ws
-                         where
-                              new_binds | id == instToId w = binds
-                                        | otherwise        = addBind binds w (L (instSpan w) (HsVar id))
+         Just (Given id) 
+               | id == instToId w
+               -> go avails binds irreds ws 
                -- The sought Id can be one of the givens, via a superclass chain
                -- and then we definitely don't want to generate an x=x binding!
 
-         Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
+               | otherwise
+               -> go avails (addBind binds w (nlHsVar id)) irreds ws
+
+         Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
                             where
                                new_binds = addBind binds w rhs
 
     add_given avails w = extendAvailEnv avails w (Given (instToId w))
 
-    add_free avails w | isMethod w = avails
-                     | otherwise  = add_given avails w
-       -- NB: Hack alert!  
-       -- Do *not* replace Free by Given if it's a method.
-       -- The following situation shows why this is bad:
-       --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
-       -- From an application (truncate f i) we get
-       --      t1 = truncate at f
-       --      t2 = t1 at i
-       -- If we have also have a second occurrence of truncate, we get
-       --      t3 = truncate at f
-       --      t4 = t3 at i
-       -- When simplifying with i,f free, we might still notice that
-       --   t1=t3; but alas, the binding for t2 (which mentions t1)
-       --   will continue to float out!
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
+addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst) 
                                                      (VarBind (instToId inst) rhs))
-instSpan wanted = instLocSpan (instLoc wanted)
 \end{code}
 
 
-\begin{code}
--------------------------
-addFree :: Avails -> Inst -> TcM Avails
-       -- When an Inst is tossed upstairs as 'free' we nevertheless add it
-       -- to avails, so that any other equal Insts will be commoned up right
-       -- here rather than also being tossed upstairs.  This is really just
-       -- an optimisation, and perhaps it is more trouble that it is worth,
-       -- as the following comments show!
-       --
-       -- NB: do *not* add superclasses.  If we have
-       --      df::Floating a
-       --      dn::Num a
-       -- but a is not bound here, then we *don't* want to derive
-       -- dn from df here lest we lose sharing.
-       --
-addFree avails free = extendAvails avails free IsFree
+Note [No superclasses for Stop]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
+add it to avails, so that any other equal Insts will be commoned up
+right here.  However, we do *not* add superclasses.  If we have
+       df::Floating a
+       dn::Num a
+but a is not bound here, then we *don't* want to derive dn from df
+here lest we lose sharing.
 
+\begin{code}
 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
 addWanted want_scs avails wanted rhs_expr wanteds
   = addAvailAndSCs want_scs avails wanted avail
@@ -2036,7 +2060,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
-  , 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))
@@ -2047,7 +2073,30 @@ addRefinedGiven reft (refined_givens, avails) given
            -- 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
@@ -2150,7 +2199,7 @@ tc_simplify_top doc interactive 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
@@ -2158,10 +2207,9 @@ tc_simplify_top doc interactive wanteds
        -- OK, so there are some errors
        {       -- Use the defaulting rules to do extra unification
                -- NB: irreds are already zonked
-       ; extended_default <- if interactive then return True
-                             else doptM Opt_ExtendedDefaultRules
-       ; disambiguate extended_default irreds1 -- Does unification
-       ; (binds2, irreds2) <- topCheckLoop doc irreds1
+       ; dflags <- getDOpts
+       ; disambiguate interactive dflags irreds1       -- Does unification
+       ; (irreds2, binds2) <- topCheckLoop doc irreds1
 
                -- Deal with implicit parameter
        ; let (bad_ips, non_ips) = partition isIPDict irreds2
@@ -2208,24 +2256,23 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
-disambiguate :: Bool -> [Inst] -> TcM ()
+disambiguate :: Bool -> DynFlags -> [Inst] -> TcM ()
        -- Just does unification to fix the default types
        -- The Insts are assumed to be pre-zonked
-disambiguate extended_defaulting insts
+disambiguate interactive dflags 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
-       ; default_tys <- case mb_defaults of
-                          Just tys -> return tys
-                          Nothing  ->  -- No use-supplied default;
-                                       -- use [Integer, Double]
-                               do { integer_ty <- tcMetaTy integerTyConName
-                                  ; checkWiredInTyCon doubleTyCon
-                                  ; return [integer_ty, doubleTy] }
+       ; default_tys <- getDefaultTys extended_defaulting ovl_strings
+
+       ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
        ; mapM_ (disambigGroup default_tys) defaultable_groups  }
   where
+   extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
+   ovl_strings = dopt Opt_OverloadedStrings dflags
+
    unaries :: [(Inst,Class, TcTyVar)]  -- (C tv) constraints
    bad_tvs :: TcTyVarSet         -- Tyvars mentioned by *other* constraints
    (unaries, bad_tvs) = getDefaultableDicts insts
@@ -2237,21 +2284,26 @@ disambiguate extended_defaulting insts
 
    defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
    defaultable_group ds@((_,_,tv):_)
-       =  not (isSkolemTyVar tv)       -- Note [Avoiding spurious errors]
+       =  isTyConableTyVar tv  -- Note [Avoiding spurious errors]
        && not (tv `elemVarSet` bad_tvs)
        && defaultable_classes [c | (_,c,_) <- ds]
    defaultable_group [] = panic "defaultable_group"
 
    defaultable_classes clss 
        | extended_defaulting = any isInteractiveClass clss
-       | otherwise = all isStandardClass clss && any isNumericClass clss
+       | otherwise           = all is_std_class clss && (any is_num_class clss)
 
        -- In interactive mode, or with -fextended-default-rules,
        -- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
-       = isNumericClass cls
-       || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+       = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+
+   is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+       -- is_num_class adds IsString to the standard numeric classes, 
+       -- when -foverloaded-strings is enabled
 
+   is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+       -- Similarly is_std_class
 
 disambigGroup :: [Type]                        -- The default types
              -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
@@ -2276,8 +2328,43 @@ disambigGroup default_tys dicts
                -- After this we can't fail
           ; warnDefault dicts default_ty
           ; unifyType default_ty (mkTyVarTy tyvar) }
+
+
+getDefaultTys :: Bool -> Bool -> TcM [Type]
+getDefaultTys extended_deflts ovl_strings
+  = do { mb_defaults <- getDeclaredDefaultTys
+       ; case mb_defaults of {
+          Just tys -> return tys ;     -- User-supplied defaults
+          Nothing  -> do
+
+       -- No use-supplied default
+       -- Use [Integer, Double], plus modifications
+       { integer_ty <- tcMetaTy integerTyConName
+       ; checkWiredInTyCon doubleTyCon
+       ; string_ty <- tcMetaTy stringTyConName
+       ; return (opt_deflt extended_deflts unitTy
+                       -- Note [Default unitTy]
+                       ++
+                 [integer_ty,doubleTy]
+                       ++
+                 opt_deflt ovl_strings string_ty) } } }
+  where
+    opt_deflt True  ty = [ty]
+    opt_deflt False ty = []
 \end{code}
 
+Note [Default unitTy]
+~~~~~~~~~~~~~~~~~~~~~
+In interative mode (or with -fextended-default-rules) we add () as the first type we
+try when defaulting.  This has very little real impact, except in the following case.
+Consider: 
+       Text.Printf.printf "hello"
+This has type (forall a. IO a); it prints "hello", and returns 'undefined'.  We don't
+want the GHCi repl loop to try to print that 'undefined'.  The neatest thing is to
+default the 'a' to (), rather than to Integer (which is what would otherwise happen;
+and then GHCi doesn't attempt to print the ().  So in interactive mode, we add
+() to the list of defaulting types.  See Trac #1200.
+
 Note [Avoiding spurious errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When doing the unification for defaulting, we check for skolem
@@ -2310,78 +2397,34 @@ instance declarations.
 
 \begin{code}
 tcSimplifyDeriv :: InstOrigin
-                -> TyCon
                -> [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?
-    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)
-               -- 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)
+       ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+       ; (irreds, _) <- topCheckLoop doc wanteds
+
+       ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+             simpl_theta = substTheta rev_env (map dictPred irreds)
+               -- This reverse-mapping is a pain, but the result
+               -- should mention the original TyVars not TcTyVars
+
+       -- NB: the caller will further check the tv_dicts for
+       --     legal instance-declaration form
+
+       ; return simpl_theta }
   where
     doc = ptext SLIT("deriving classes for a data type")
 \end{code}
 
-Note [Deriving context]
-~~~~~~~~~~~~~~~~~~~~~~~
-With -fglasgow-exts, we allow things like (C Int a) in the simplified
-context for a derived instance declaration, because at a use of this
-instance, we might know that a=Bool, and have an instance for (C Int
-Bool)
-
-We nevertheless insist that each predicate meets the termination
-conditions. If not, the deriving mechanism generates larger and larger
-constraints.  Example:
-  data Succ a = S a
-  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ.  First we'll generate
-  instance (Show (Succ a), Show a) => Show (Seq a)
-and then
-  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on.  Instead we want to complain of no instance for (Show (Succ a)).
-  
 
 
 @tcSimplifyDefault@ just checks class-type constraints, essentially;
@@ -2394,7 +2437,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
 
 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 ()
@@ -2450,7 +2493,8 @@ addTopIPErrs bndrs ips
   where
     (tidy_env, tidy_ips) = tidyInsts ips
     mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
-                           nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
+                           nest 2 (ptext SLIT("the monomorphic top-level binding") 
+                                           <> plural bndrs <+> ptext SLIT("of")
                                            <+> pprBinders bndrs <> colon)],
                       nest 2 (vcat (map ppr_ip ips)),
                       monomorphism_fix]
@@ -2533,7 +2577,7 @@ report_no_instances tidy_env mb_what insts
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
                              ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
       where
-       ispecs = [ispec | (_, ispec) <- matches]
+       ispecs = [ispec | (ispec, _) <- matches]
 
     mk_no_inst_err insts
       | null insts = empty
@@ -2606,6 +2650,10 @@ mkMonomorphismMsg tidy_env inst_tvs
   = findGlobals (mkVarSet inst_tvs) tidy_env   `thenM` \ (tidy_env, docs) ->
     returnM (tidy_env, mk_msg docs)
   where
+    mk_msg _ | any isRuntimeUnk inst_tvs
+        =  vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
+                   (pprWithCommas ppr inst_tvs),
+                ptext SLIT("Use :print or :force to determine these types")]
     mk_msg []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
                        -- This happens in things like
                        --      f x = show (read "foo")
@@ -2614,6 +2662,11 @@ mkMonomorphismMsg tidy_env inst_tvs
                        nest 2 (vcat docs),
                        monomorphism_fix
                       ]
+
+isRuntimeUnk :: TcTyVar -> Bool
+isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
+               | otherwise = False
+
 monomorphism_fix :: SDoc
 monomorphism_fix = ptext SLIT("Probable fix:") <+> 
                   (ptext SLIT("give these definition(s) an explicit type signature")
@@ -2631,12 +2684,6 @@ warnDefault ups default_ty
                                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"),