Fix a bug in the handling of implication constraints (Trac #1430)

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

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 182a7c5..adf0f78 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -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

@@ -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 )
 Here's a good way to choose Q:
 
        Q = grow( fv(T), C ) \ oclose( fv(G), C )

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

-       -> TcM ([TcTyVar],      -- Tyvars to quantify (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
                [Inst],         -- Dict Ids that must be bound here (zonked)
                TcDictBinds)    -- Bindings
        -- Any free (escaping) Insts are tossed into the environment

@@ -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
        ; 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
 
                -- 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
        ; 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)
        ; 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.
        -- 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}
 
 \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
 \begin{code}
 -----------------------------------------------------------
 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify

@@ -848,11 +909,13 @@ bindIrredsR loc qtvs co_vars reft givens irreds
   | otherwise
   = do { let givens' = filter isDict givens
                -- The givens can include methods
   | 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]
           -- 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
                     then do
                        { let qtv_set = mkVarSet qtvs
                              (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds

@@ -862,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'
        
        ; 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 } 
 
        ; extendLIEs implics
        ; return bind } 
 

@@ -875,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
 -- 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
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs reft

@@ -885,7 +951,7 @@ makeImplicationBind loc all_tvs reft
  | otherwise                   -- Otherwise we must generate a binding
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
  | 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,
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 
                                         tci_given = givens,

@@ -947,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]
 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
        
 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals

@@ -1171,7 +1237,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 ([TyVar],        -- 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.

@@ -1198,9 +1264,22 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        ; gbl_tvs' <- tcGetGlobalTyVars
        ; constrained_dicts' <- mappM zonkInst constrained_dicts
 
        ; 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,
        ; traceTc (text "tcSimplifyRestricted" <+> vcat [
                pprInsts wanteds, pprInsts constrained_dicts',
                ppr _binds,

@@ -1317,7 +1396,7 @@ tcSimplifyRuleLhs wanteds
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
                                 -- 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}
                 NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
          }
 \end{code}

@@ -1558,6 +1637,7 @@ reduceContext env wanteds
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,

+            text "irreds = " <+> ppr irreds,

             text "----------------------"
             ]))
 
             text "----------------------"
             ]))
 

@@ -1826,6 +1906,9 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                -- Extract the binding
        ; (binds, irreds) <- extractResults avails wanteds
  
                -- 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
                -- 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

@@ -1834,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
                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
 
        ; 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
                        | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
 
                -- If there are any irreds, we back off and return NoInstance

@@ -1876,6 +1955,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

@@ -1892,7 +1985,7 @@ type ImprovementDone = Bool       -- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
 
 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
                        -- which are going to be lambda bound
 
   | Given TcId                 -- Used for dictionaries for which we have a binding

@@ -1915,7 +2008,7 @@ instance Outputable AvailHow where
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
 
 -------------------------
 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)
 
 pprAvail (Given x)     = text "Given" <+> ppr x
 pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
 

@@ -1978,25 +2071,30 @@ extractResults (Avails _ avails) wanteds
          Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
                        go avails binds irreds ws
 
          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) 
          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!
 
                -- 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)
 
          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))
 
     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}
 
 
 \end{code}
 
 

@@ -2068,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 )
 \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
 
 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
 addAvailAndSCs want_scs avails inst avail

@@ -2176,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
        -- 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
 
        ; let (bad_ips, non_ips) = partition isIPDict irreds2
              (ambigs, others)   = partition isTyVarDict non_ips
 

@@ -2226,26 +2324,23 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
 @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
        -- 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
   | 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
        ; 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
    unaries :: [(Inst,Class, TcTyVar)]  -- (C tv) constraints
    bad_tvs :: TcTyVarSet         -- Tyvars mentioned by *other* constraints
    (unaries, bad_tvs) = getDefaultableDicts insts

@@ -2257,22 +2352,28 @@ 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 (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
        && 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 
 
        -- 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
 disambigGroup :: [Type]                        -- The default types
              -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
              -> TcM () -- Just does unification, to fix the default types

@@ -2296,8 +2397,64 @@ disambigGroup default_tys dicts
                -- After this we can't fail
           ; warnDefault dicts default_ty
           ; unifyType default_ty (mkTyVarTy tyvar) }
                -- 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}
 
 \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
 Note [Avoiding spurious errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When doing the unification for defaulting, we check for skolem

@@ -2330,78 +2487,34 @@ 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)
-               -- 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}
 
   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;
 
 
 @tcSimplifyDefault@ just checks class-type constraints, essentially;

@@ -2466,15 +2579,17 @@ addTopIPErrs :: [Name] -> [Inst] -> TcM ()
 addTopIPErrs bndrs [] 
   = return ()
 addTopIPErrs bndrs ips
 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
   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)],
                                            <> 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 ()
     ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
 
 topIPErrs :: [Inst] -> TcM ()

@@ -2554,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
                                 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
 
     mk_no_inst_err insts
       | null insts = empty

@@ -2624,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
 -- 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
   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
                        -- 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 ->
     
 warnDefault ups default_ty
   = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->

@@ -2652,12 +2781,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"),