Fix a bug in the handling of implication constraints (Trac #1430)
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index 451e3b1..adf0f78 100644 (file)
@@ -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
@@ -210,8 +209,8 @@ Notice that
 
 -----------------------------------------
 
-Choosing Q
-~~~~~~~~~~
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Here's a good way to choose Q:
 
        Q = grow( fv(T), C ) \ oclose( fv(G), C )
@@ -671,26 +670,88 @@ tcSimplifyInfer doc tau_tvs wanted
        ; 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
+                       -- See Note [Choosing which variables to quantify]
+
+               -- To maximise sharing, remove from consideration any 
+               -- constraints that don't mention qtvs at all
+       ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
+       ; extendLIEs free1
 
                -- To make types simple, reduce as much as possible
+       ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ 
+                  ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
        ; 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
+             red_env     = mkRedEnv doc try_me []
+       ; (irreds1, binds1) <- checkLoop red_env bound
+
+               -- Note [Inference and implication constraints]
+               -- By putting extra_dicts first, we make them available
+               -- to solve the implication constraints
+       ; let extra_dicts = getImplicWanteds qtvs irreds1
+       ; (irreds2, binds2) <- if null extra_dicts 
+                              then return (irreds1, emptyBag)
+                              else do { extra_dicts' <- mapM cloneDict extra_dicts
+                                      ; checkLoop red_env (extra_dicts' ++ irreds1) }
+
+               -- By now improvment may have taken place, and we must *not*
+               -- quantify over any variable free in the environment
+               -- tc137 (function h inside g) is an example
+       ; gbl_tvs <- tcGetGlobalTyVars
+       ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
+       ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
+
+               -- Do not quantify over constraints that *now* do not
+               -- mention quantified type variables, because they are
+               -- simply ambiguous (or might be bound further out).  Example:
+               --      f :: Eq b => a -> (a, b)
+               --      g x = fst (f x)
+               -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+               -- We decide to quantify over 'alpha' alone, but free1 does not include f77
+               -- because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
+               -- constraint (Eq beta), which we dump back into the free set
+               -- See test tcfail181
+       ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
+       ; extendLIEs free3
+       
+               -- We can't abstract over any remaining unsolved 
+               -- implications so instead just float them outwards. Ugh.
+       ; let (q_dicts, implics) = partition isDict irreds3
        ; loc <- getInstLoc (ImplicOrigin doc)
-       ; implic_bind <- bindIrreds loc qtvs' dicts implics
+       ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
 
-       ; return (qtvs', dicts, binds `unionBags` implic_bind) }
+       ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `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.
+
+getImplicWanteds :: TcTyVarSet -> [Inst] -> [Inst]
+-- See Note [Inference and implication constraints]
+-- Find the wanted constraints in implication constraints that mention the 
+-- quantified type variables, and are not bound by forall's in the constraint itself
+-- Returns only Dicts
+getImplicWanteds qtvs implics
+  = concatMap get implics
+  where
+    get d@(Dict {}) | tyVarsOfInst d `intersectsVarSet` qtvs = [d]
+                   | otherwise                              = []
+    get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+       = [ d | let tv_set = mkVarSet tvs
+             , d <- getImplicWanteds qtvs wanteds 
+             , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
 \end{code}
 
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+We can't (or at least don't) abstract over implications.  But we might
+have an implication constraint (perhaps arising from a nested pattern
+match) like
+       C a => D a
+when we are now trying to quantify over 'a'.  Our best approximation
+is to make (D a) part of the inferred context, so we can use that to
+discharge the implication. Hence getImplicWanteds.
+
+See Trac #1430 and test tc228.
+
+
 \begin{code}
 -----------------------------------------------------------
 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
@@ -850,10 +911,11 @@ bindIrredsR loc qtvs co_vars reft givens irreds
                -- 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'
+       ; irreds' <- if null givens' && isEmptyRefinement reft
                     then do
                        { let qtv_set = mkVarSet qtvs
                              (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
@@ -863,7 +925,8 @@ bindIrredsR loc qtvs co_vars reft givens 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
+                       -- This call does the real work
+                       -- If irreds' is empty, it does something sensible
        ; extendLIEs implics
        ; return bind } 
 
@@ -876,6 +939,8 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
 -- 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
@@ -886,7 +951,7 @@ makeImplicationBind loc all_tvs reft
  | otherwise                   -- Otherwise we must generate a binding
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
-       ; let 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,
@@ -948,7 +1013,7 @@ Inside the pattern match, which binds (a:*, x:a), we know that
 Hence we have a dictionary for Show [a] available; and indeed we 
 need it.  We are going to build an implication contraint
        forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledge (Show b)
+Later, we will solve this constraint using the knowledg e(Show b)
        
 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
@@ -1199,9 +1264,22 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        ; 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'
+       ; 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,
@@ -1318,7 +1396,7 @@ tcSimplifyRuleLhs wanteds
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
-                GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+                GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
                 NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
          }
 \end{code}
@@ -1559,6 +1637,7 @@ reduceContext env wanteds
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,
+            text "irreds = " <+> ppr irreds,
             text "----------------------"
             ]))
 
@@ -1827,6 +1906,9 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                -- Extract the binding
        ; (binds, irreds) <- extractResults avails wanteds
  
+       ; traceTc (text "reduceImplication result" <+> vcat
+                       [ ppr irreds, ppr binds])
+
                -- 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
@@ -1835,16 +1917,12 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                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 `unionBags` bind)
                rhs = mkHsWrap co payload
                loc = instLocSpan inst_loc
-               payload | isSingleton wanteds = HsVar (instToId (head wanteds))
+               payload | [wanted] <- wanteds = HsVar (instToId wanted)
                        | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
 
                -- If there are any irreds, we back off and return NoInstance
@@ -1907,7 +1985,7 @@ type ImprovementDone = Bool       -- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
-  = IsIrred            -- Used for irreducible dictionaries,
+  = IsIrred TcId       -- Used for irreducible dictionaries,
                        -- which are going to be lambda bound
 
   | Given TcId                 -- Used for dictionaries for which we have a binding
@@ -1930,7 +2008,7 @@ instance Outputable AvailHow where
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
-pprAvail IsIrred       = text "Irred"
+pprAvail (IsIrred x)   = text "Irred" <+> ppr x
 pprAvail (Given x)     = text "Given" <+> ppr x
 pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
 
@@ -1993,25 +2071,30 @@ extractResults (Avails _ avails) wanteds
          Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
                        go avails binds irreds ws
 
-         Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
-
          Just (Given id) 
-               | id == instToId w
-               -> go avails binds irreds ws 
+               | id == w_id -> go avails binds irreds ws 
+               | otherwise  -> go avails (addBind binds w_id (nlHsVar id)) 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!
 
-               | otherwise
-               -> go avails (addBind binds w (nlHsVar id)) irreds ws
+         Just (IsIrred id) 
+               | id == w_id -> go (add_given avails w) binds           (w:irreds) ws
+               | otherwise  -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
+               -- The add_given handles the case where we want (Ord a, Eq a), and we
+               -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
+               -- This showed up in a dupliated Ord constraint in the error message for 
+               --      test tcfail043
 
          Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
-                            where
-                               new_binds = addBind binds w rhs
+                            where      
+                               new_binds = addBind binds w_id rhs
+      where
+       w_id = instToId w       
 
     add_given avails w = extendAvailEnv avails w (Given (instToId w))
+       -- Don't add the same binding twice
 
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst) 
-                                                     (VarBind (instToId inst) rhs))
+addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
 \end{code}
 
 
@@ -2083,7 +2166,7 @@ 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
+                                addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
 
 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
 addAvailAndSCs want_scs avails inst avail
@@ -2191,12 +2274,12 @@ 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
-       ; (irreds2, binds2) <- topCheckLoop doc irreds1
+       ; dflags <- getDOpts
+       ; disambiguate interactive dflags irreds1       -- Does unification
+                                                       -- hence try again
 
-               -- Deal with implicit parameter
+               -- Deal with implicit parameters
+       ; (irreds2, binds2) <- topCheckLoop doc irreds1
        ; let (bad_ips, non_ips) = partition isIPDict irreds2
              (ambigs, others)   = partition isTyVarDict non_ips
 
@@ -2241,26 +2324,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
   = 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
@@ -2272,22 +2352,28 @@ disambiguate extended_defaulting insts
 
    defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
    defaultable_group ds@((_,_,tv):_)
-       =  not (isImmutableTyVar 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)
              -> TcM () -- Just does unification, to fix the default types
@@ -2311,8 +2397,64 @@ 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 = []
+
+-----------------------
+getDefaultableDicts :: [Inst] -> ([(Inst, Class, TcTyVar)], TcTyVarSet)
+-- Look for free dicts of the form (C tv), even inside implications
+-- *and* the set of tyvars mentioned by all *other* constaints
+-- This disgustingly ad-hoc function is solely to support defaulting
+getDefaultableDicts insts
+  = (concat ps, unionVarSets tvs)
+  where
+    (ps, tvs) = mapAndUnzip get insts
+    get d@(Dict {tci_pred = ClassP cls [ty]})
+       | Just tv <- tcGetTyVar_maybe ty = ([(d,cls,tv)], emptyVarSet)
+       | otherwise                      = ([], tyVarsOfType ty)
+    get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+       = ([ up | up@(_,_,tv) <- ups, not (tv `elemVarSet` tv_set)],
+          ftvs `minusVarSet` tv_set)
+       where
+          tv_set = mkVarSet tvs
+          (ups, ftvs) = getDefaultableDicts wanteds
+    get inst = ([], tyVarsOfInst inst)
 \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
@@ -2345,78 +2487,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;
@@ -2481,15 +2579,17 @@ addTopIPErrs :: [Name] -> [Inst] -> TcM ()
 addTopIPErrs bndrs [] 
   = return ()
 addTopIPErrs bndrs ips
-  = addErrTcM (tidy_env, mk_msg tidy_ips)
+  = do { dflags <- getDOpts
+       ; addErrTcM (tidy_env, mk_msg dflags tidy_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") 
+    mk_msg dflags ips 
+       = vcat [sep [ptext SLIT("Implicit parameters escape from"),
+               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]
+               nest 2 (vcat (map ppr_ip ips)),
+               monomorphism_fix dflags]
     ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
 
 topIPErrs :: [Inst] -> TcM ()
@@ -2569,7 +2669,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
@@ -2639,21 +2739,35 @@ mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
 -- Try to identify the offending variable
 -- ASSUMPTION: the Insts are fully zonked
 mkMonomorphismMsg tidy_env inst_tvs
-  = findGlobals (mkVarSet inst_tvs) tidy_env   `thenM` \ (tidy_env, docs) ->
-    returnM (tidy_env, mk_msg docs)
+  = do { dflags <- getDOpts
+       ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
+       ; return (tidy_env, mk_msg dflags docs) }
   where
-    mk_msg []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+    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")
                        -- where monomorphism doesn't play any role
-    mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
-                       nest 2 (vcat docs),
-                       monomorphism_fix
-                      ]
-monomorphism_fix :: SDoc
-monomorphism_fix = ptext SLIT("Probable fix:") <+> 
-                  (ptext SLIT("give these definition(s) an explicit type signature")
-                   $$ ptext SLIT("or use -fno-monomorphism-restriction"))
+    mk_msg dflags docs 
+       = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+               nest 2 (vcat docs),
+               monomorphism_fix dflags]
+
+isRuntimeUnk :: TcTyVar -> Bool
+isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
+               | otherwise = False
+
+monomorphism_fix :: DynFlags -> SDoc
+monomorphism_fix dflags
+  = ptext SLIT("Probable fix:") <+> vcat
+       [ptext SLIT("give these definition(s) an explicit type signature"),
+        if dopt Opt_MonomorphismRestriction dflags
+           then ptext SLIT("or use -fno-monomorphism-restriction")
+           else empty] -- Only suggest adding "-fno-monomorphism-restriction"
+                       -- if it is not already set!
     
 warnDefault ups default_ty
   = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
@@ -2667,12 +2781,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"),