Simon's big boxy-type commit
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 5c0a22d..f187cdc 100644 (file)
@@ -10,6 +10,7 @@ module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, 
+       tcSimplifySuperClasses,
        tcSimplifyTop, tcSimplifyInteractive,
        tcSimplifyBracket,
 
@@ -19,43 +20,44 @@ module TcSimplify (
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TcUnify( unifyTauTy )
-import TcEnv           -- temp
+import {-# SOURCE #-} TcUnify( unifyType )
 import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
-import TcHsSyn         ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
+import TcHsSyn         ( mkHsApp, mkHsTyApp, mkHsDictApp )
 
 import TcRnMonad
 import Inst            ( lookupInst, LookupInstResult(..),
                          tyVarsOfInst, fdPredsOfInsts, newDicts, 
                          isDict, isClassDict, isLinearInst, linearInstType,
-                         isStdClassTyVarDict, isMethodFor, isMethod,
+                         isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
-                         instBindingRequired, fdPredsOfInst,
-                         newDictsFromOld, tcInstClassOp,
-                         getDictClassTys, isTyVarDict,
-                         instLoc, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
-                         isInheritableInst, pprDFuns, pprDictsTheta
+                         fdPredsOfInst,
+                         newDictsAtLoc, tcInstClassOp,
+                         getDictClassTys, isTyVarDict, instLoc,
+                         zonkInst, tidyInsts, tidyMoreInsts,
+                         pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
+                         isInheritableInst, pprDictsTheta
                        )
-import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
-import InstEnv         ( lookupInstEnv, classInstances )
+import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
+                         lclEnvElts, tcMetaTy )
+import InstEnv         ( lookupInstEnv, classInstances, pprInstances )
 import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
-import TcType          ( TcTyVar, TcTyVarSet, ThetaType, 
-                          mkClassPred, isOverloadedTy, mkTyConApp,
+import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, 
+                          mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
-                         tyVarsOfPred, tcEqType, pprPred )
+                         tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
+import TcIface         ( checkWiredInTyCon )
 import Id              ( idType, mkUserLocal )
 import Var             ( TyVar )
 import Name            ( Name, getOccName, getSrcLoc )
 import NameSet         ( NameSet, mkNameSet, elemNameSet )
 import Class           ( classBigSig, classKey )
 import FunDeps         ( oclose, grow, improve, pprEquationDoc )
-import PrelInfo                ( isNumericClass ) 
+import PrelInfo                ( isNumericClass, isStandardClass ) 
 import PrelNames       ( splitName, fstName, sndName, integerTyConName,
                          showClassKey, eqClassKey, ordClassKey )
 import Type            ( zipTopTvSubst, substTheta, substTy )
-import TysWiredIn      ( pairTyCon, doubleTy )
+import TysWiredIn      ( pairTyCon, doubleTy, doubleTyCon )
 import ErrUtils                ( Message )
 import BasicTypes      ( TopLevelFlag, isNotTopLevel )
 import VarSet
@@ -67,7 +69,8 @@ import ListSetOps     ( equivClasses )
 import Util            ( zipEqual, isSingleton )
 import List            ( partition )
 import SrcLoc          ( Located(..) )
-import CmdLineOpts
+import DynFlags                ( DynFlag(..) )
+import StaticFlags
 \end{code}
 
 
@@ -665,7 +668,7 @@ inferLoop doc tau_tvs wanteds
        try_me inst
          | isFreeWhenInferring qtvs inst = Free
          | isClassDict inst              = DontReduceUnlessConstant    -- Dicts
-         | otherwise                     = ReduceMe                    -- Lits and Methods
+         | otherwise                     = ReduceMe NoSCs              -- Lits and Methods
     in
     traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, 
                                      ppr (grow preds tau_tvs'), ppr qtvs])     `thenM_`
@@ -778,12 +781,13 @@ tcSimplifyCheck
 --     global type variables in the environment; so you don't
 --     need to worry about setting them before calling tcSimplifyCheck
 tcSimplifyCheck doc qtvs givens wanted_lie
-  = tcSimplCheck doc get_qtvs
-                givens wanted_lie      `thenM` \ (qtvs', binds) ->
-    returnM binds
+  = ASSERT( all isSkolemTyVar qtvs )
+    do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
+       ; extendLIEs frees
+       ; return binds }
   where
---    get_qtvs = zonkTcTyVarsAndFV qtvs
-    get_qtvs = return (mkVarSet qtvs)
+--  get_qtvs = zonkTcTyVarsAndFV qtvs
+    get_qtvs = return (mkVarSet qtvs)  -- All skolems
 
 
 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
@@ -798,7 +802,9 @@ tcSimplifyInferCheck
                 TcDictBinds)   -- Bindings
 
 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
-  = tcSimplCheck doc get_qtvs givens wanted_lie
+  = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
+       ; extendLIEs frees
+       ; return (qtvs', binds) }
   where
        -- Figure out which type variables to quantify over
        -- You might think it should just be the signature tyvars,
@@ -825,17 +831,16 @@ tcSimplifyInferCheck doc tau_tvs givens wanted_lie
 Here is the workhorse function for all three wrappers.
 
 \begin{code}
-tcSimplCheck doc get_qtvs givens wanted_lie
-  = check_loop givens wanted_lie       `thenM` \ (qtvs, frees, binds, irreds) ->
-
-       -- Complain about any irreducible ones
-    mappM zonkInst given_dicts_and_ips                         `thenM` \ givens' ->
-    groupErrs (addNoInstanceErrs (Just doc) givens') irreds    `thenM_`
+tcSimplCheck doc get_qtvs want_scs givens wanted_lie
+  = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
 
-       -- Done
-    extendLIEs frees           `thenM_`
-    returnM (qtvs, binds)
+               -- Complain about any irreducible ones
+       ; if not (null irreds)
+         then do { givens' <- mappM zonkInst given_dicts_and_ips
+                 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
+         else return ()
 
+       ; returnM (qtvs, frees, binds) }
   where
     given_dicts_and_ips = filter (not . isMethod) givens
        -- For error reporting, filter out methods, which are 
@@ -854,7 +859,7 @@ tcSimplCheck doc get_qtvs givens wanted_lie
            -- When checking against a given signature we always reduce
            -- until we find a match against something given, or can't reduce
            try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
-                       | otherwise                            = ReduceMe
+                       | otherwise                            = ReduceMe want_scs
        in
        reduceContext doc try_me givens' wanteds'       `thenM` \ (no_improvement, frees, binds, irreds) ->
 
@@ -869,6 +874,62 @@ tcSimplCheck doc get_qtvs givens wanted_lie
 
 %************************************************************************
 %*                                                                     *
+               tcSimplifySuperClasses
+%*                                                                     *
+%************************************************************************
+
+Note [SUPERCLASS-LOOP 1]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We have to be very, very careful when generating superclasses, lest we
+accidentally build a loop. Here's an example:
+
+  class S a
+
+  class S a => C a where { opc :: a -> a }
+  class S b => D b where { opd :: b -> b }
+  
+  instance C Int where
+     opc = opd
+  
+  instance D Int where
+     opd = opc
+
+From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
+Simplifying, we may well get:
+       $dfCInt = :C ds1 (opd dd)
+       dd  = $dfDInt
+       ds1 = $p1 dd
+Notice that we spot that we can extract ds1 from dd.  
+
+Alas!  Alack! We can do the same for (instance D Int):
+
+       $dfDInt = :D ds2 (opc dc)
+       dc  = $dfCInt
+       ds2 = $p1 dc
+
+And now we've defined the superclass in terms of itself.
+
+Solution: never generate a superclass selectors at all when
+satisfying the superclass context of an instance declaration.
+
+Two more nasty cases are in
+       tcrun021
+       tcrun033
+
+\begin{code}
+tcSimplifySuperClasses qtvs givens sc_wanteds
+  = ASSERT( all isSkolemTyVar qtvs )
+    do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
+       ; binds2             <- tc_simplify_top doc False NoSCs frees
+       ; return (binds1 `unionBags` binds2) }
+  where
+    get_qtvs = return (mkVarSet qtvs)
+    doc = ptext SLIT("instance declaration superclass context")
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
 \subsection{tcSimplifyRestricted}
 %*                                                                     *
 %************************************************************************
@@ -1028,7 +1089,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        is_nested_group = isNotTopLevel top_lvl
         try_me inst | isFreeWrtTyVars qtvs inst,
                      (is_nested_group || isDict inst) = Free
-                   | otherwise                        = ReduceMe
+                   | otherwise                        = ReduceMe AddSCs
     in
     reduceContextWithoutImprovement 
        doc try_me wanteds'             `thenM` \ (frees, binds, irreds) ->
@@ -1086,7 +1147,7 @@ want to get
        forall dIntegralInt.
        fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 
-because the scsel will mess up matching.  Instead we want
+because the scsel will mess up RULE matching.  Instead we want
 
        forall dIntegralInt, dNumInt.
        fromIntegral Int Int dIntegralInt dNumInt = id Int
@@ -1108,7 +1169,7 @@ tcSimplifyToDicts wanteds
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
     try_me inst        | isDict inst = KeepDictWithoutSCs      -- See notes above re "WithoutSCs"
-               | otherwise   = ReduceMe
+               | otherwise   = ReduceMe NoSCs
 \end{code}
 
 
@@ -1164,7 +1225,7 @@ tcSimplifyIPs given_ips wanteds
 
        -- Simplify any methods that mention the implicit parameter
     try_me inst | isFreeWrtIPs ip_set inst = Free
-               | otherwise                = ReduceMe
+               | otherwise                = ReduceMe NoSCs
 
     simpl_loop givens wanteds
       = mappM zonkInst givens          `thenM` \ givens' ->
@@ -1236,7 +1297,7 @@ bindInstsOfLocalFuns wanteds local_ids
     overloaded_set = mkVarSet overloaded_ids   -- There can occasionally be a lot of them
                                                -- so it's worth building a set, so that
                                                -- lookup (in isMethodFor) is faster
-    try_me inst | isMethod inst = ReduceMe
+    try_me inst | isMethod inst = ReduceMe NoSCs
                | otherwise     = Free
 \end{code}
 
@@ -1251,11 +1312,10 @@ The main control over context reduction is here
 
 \begin{code}
 data WhatToDo
- = ReduceMe            -- Try to reduce this
+ = ReduceMe WantSCs    -- Try to reduce this
                        -- If there's no instance, behave exactly like
-                       -- DontReduce: add the inst to
-                       -- the irreductible ones, but don't
-                       -- produce an error message of any kind.
+                       -- DontReduce: add the inst to the irreductible ones, 
+                       -- but don't produce an error message of any kind.
                        -- It might be quite legitimate such as (Eq a)!
 
  | KeepDictWithoutSCs  -- Return as irreducible; don't add its superclasses
@@ -1267,10 +1327,12 @@ data WhatToDo
  | Free                          -- Return as free
 
 reduceMe :: Inst -> WhatToDo
-reduceMe inst = ReduceMe
+reduceMe inst = ReduceMe AddSCs
 
 data WantSCs = NoSCs | AddSCs  -- Tells whether we should add the superclasses
                                -- of a predicate when adding it to the avails
+       -- The reason for this flag is entirely the super-class loop problem
+       -- Note [SUPER-CLASS LOOP 1]
 \end{code}
 
 
@@ -1288,10 +1350,6 @@ data Avail
                        -- e.g. those "given" in a signature
          Bool          -- True <=> actually consumed (splittable IPs only)
 
-  | NoRhs              -- Used for Insts like (CCallable f)
-                       -- where no witness is required.
-                       -- ToDo: remove?
-
   | Rhs                -- Used when there is a RHS
        (LHsExpr TcId)  -- The RHS
        [Inst]          -- Insts free in the RHS; we need these too
@@ -1313,7 +1371,6 @@ pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
 instance Outputable Avail where
     ppr = pprAvail
 
-pprAvail NoRhs         = text "<no rhs>"
 pprAvail IsFree                = text "Free"
 pprAvail Irred         = text "Irred"
 pprAvail (Given x b)           = text "Given" <+> ppr x <+> 
@@ -1347,7 +1404,6 @@ extractResults avails wanteds
          Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
                        go avails binds irreds frees ws
 
-         Just NoRhs  -> go avails               binds irreds     frees     ws
          Just IsFree -> go (add_free avails w)  binds irreds     (w:frees) ws
          Just Irred  -> go (add_given avails w) binds (w:irreds) frees     ws
 
@@ -1381,11 +1437,7 @@ extractResults avails wanteds
     get_root irreds frees IsFree       w = cloneDict w `thenM` \ w' ->
                                           returnM (irreds, w':frees, instToId w')
 
-    add_given avails w 
-       | instBindingRequired w = addToFM avails w (Given (instToId w) True)
-       | otherwise             = addToFM avails w NoRhs
-       -- NB: make sure that CCallable/CReturnable use NoRhs rather
-       --      than Given, else we end up with bogus bindings.
+    add_given avails w = addToFM avails w (Given (instToId w) True)
 
     add_free avails w | isMethod w = avails
                      | otherwise  = add_given avails w
@@ -1609,7 +1661,7 @@ tcImprove avails
         = addErrCtxt doc                       $
           tcInstTyVars (varSetElems qtvs)      `thenM` \ (_, _, tenv) ->
           mapM_ (unif_pr tenv) pairs
-    unif_pr tenv (ty1,ty2) =  unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
+    unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -1650,7 +1702,7 @@ reduceList (n,stack) try_me wanteds state
 #ifdef DEBUG
    (if n > 8 then
        pprTrace "Interesting! Context reduction stack deeper than 8:" 
-                (nest 2 (pprStack stack))
+               (int n $$ ifPprDebug (nest 2 (pprStack stack)))
     else (\x->x))
 #endif
     go wanteds state
@@ -1682,12 +1734,12 @@ reduce stack try_me wanted avails
                -- First, see if the inst can be reduced to a constant in one step
        try_simple addFree
 
-    ; ReduceMe ->              -- It should be reduced
+    ; ReduceMe want_scs ->     -- It should be reduced
        lookupInst wanted             `thenM` \ lookup_result ->
        case lookup_result of
            GenInst wanteds' rhs -> addIrred NoSCs avails wanted                `thenM` \ avails1 ->
                                    reduceList stack try_me wanteds' avails1    `thenM` \ avails2 ->
-                                   addWanted avails2 wanted rhs wanteds'
+                                   addWanted want_scs avails2 wanted rhs wanteds'
                -- Experiment with temporarily doing addIrred *before* the reduceList, 
                -- which has the effect of adding the thing we are trying
                -- to prove to the database before trying to prove the things it
@@ -1697,17 +1749,17 @@ reduce stack try_me wanted avails
                --     the examples in [SUPERCLASS-LOOP]
                -- So we do an addIrred before, and then overwrite it afterwards with addWanted
 
-           SimpleInst rhs       -> addWanted avails wanted rhs []
+           SimpleInst rhs -> addWanted want_scs avails wanted rhs []
 
            NoInstance ->    -- No such instance!
                             -- Add it and its superclasses
-                            addIrred AddSCs avails wanted
+                            addIrred want_scs avails wanted
     }
   where
     try_simple do_this_otherwise
       = lookupInst wanted        `thenM` \ lookup_result ->
        case lookup_result of
-           SimpleInst rhs -> addWanted avails wanted rhs []
+           SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
            other          -> do_this_otherwise avails wanted
 \end{code}
 
@@ -1717,7 +1769,7 @@ reduce stack try_me wanted avails
 isAvailable :: Avails -> Inst -> Maybe Avail
 isAvailable avails wanted = lookupFM avails wanted
        -- NB 1: the Ord instance of Inst compares by the class/type info
-       -- *not* by unique.  So
+       --  *not* by unique.  So
        --      d1::C Int ==  d2::C Int
 
 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
@@ -1762,39 +1814,41 @@ addFree :: Avails -> Inst -> TcM Avails
        --
 addFree avails free = returnM (addToFM avails free IsFree)
 
-addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted avails wanted rhs_expr wanteds
-  = addAvailAndSCs avails wanted avail
+addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
+addWanted want_scs avails wanted rhs_expr wanteds
+  = addAvailAndSCs want_scs avails wanted avail
   where
-    avail | instBindingRequired wanted = Rhs rhs_expr wanteds
-         | otherwise                  = ASSERT( null wanteds ) NoRhs
+    avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
+       -- Always add superclasses for 'givens'
+       --
        -- No ASSERT( not (given `elemFM` avails) ) because in an instance
        -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
        -- so the assert isn't true
 
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
-addIrred NoSCs  avails irred = returnM (addToFM avails irred Irred)
-addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
-                              addAvailAndSCs avails irred Irred
-
-addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
-addAvailAndSCs avails inst avail
-  | not (isClassDict inst) = returnM avails1
-  | otherwise             = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
-                            addSCs is_loop avails1 inst 
+addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
+                                addAvailAndSCs want_scs avails irred Irred
+
+addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
+addAvailAndSCs want_scs avails inst avail
+  | not (isClassDict inst) = return avails_with_inst
+  | NoSCs <- want_scs     = return avails_with_inst
+  | otherwise             = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
+                               ; addSCs is_loop avails_with_inst inst }
   where
-    avails1     = addToFM avails inst avail
-    is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
+    avails_with_inst = addToFM avails inst avail
+
+    is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
                        -- Note: this compares by *type*, not by Unique
     deps         = findAllDeps (unitVarSet (instToId inst)) avail
     dep_tys     = map idType (varSetElems deps)
 
     findAllDeps :: IdSet -> Avail -> IdSet
     -- Find all the Insts that this one depends on
-    -- See Note [SUPERCLASS-LOOP]
+    -- See Note [SUPERCLASS-LOOP 2]
     -- Watch out, though.  Since the avails may contain loops 
     -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
     findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
@@ -1809,46 +1863,45 @@ addAvailAndSCs avails inst avail
        so_far' = extendVarSet so_far kid_id    -- Add the new kid to so_far
        kid_id = instToId kid
 
-addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
+addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
        -- Add all the superclasses of the Inst to Avails
        -- The first param says "dont do this because the original thing
        --      depends on this one, so you'd build a loop"
        -- Invariant: the Inst is already in Avails.
 
 addSCs is_loop avails dict
-  = newDictsFromOld dict sc_theta'     `thenM` \ sc_dicts ->
-    foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
+  = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
+       ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
     sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
 
-    add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
-      | add_me sc_dict = addSCs is_loop avails' sc_dict
-      | otherwise      = returnM avails
+    add_sc avails (sc_dict, sc_sel)
+      | is_loop (dictPred sc_dict) = return avails     -- See Note [SUPERCLASS-LOOP 2]
+      | is_given sc_dict          = return avails
+      | otherwise                 = addSCs is_loop avails' sc_dict
       where
        sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
        avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
 
-    add_me :: Inst -> Bool
-    add_me sc_dict
-       | is_loop sc_dict = False       -- See Note [SUPERCLASS-LOOP]
-       | otherwise       = case lookupFM avails sc_dict of
-                               Just (Given _ _) -> False       -- Given is cheaper than superclass selection
-                               other            -> True        
+    is_given :: Inst -> Bool
+    is_given sc_dict = case lookupFM avails sc_dict of
+                         Just (Given _ _) -> True      -- Given is cheaper than superclass selection
+                         other            -> False     
 \end{code}
 
-Note [SUPERCLASS-LOOP]: Checking for loops
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be careful here.  If we are *given* d1:Ord a,
+Note [SUPERCLASS-LOOP 2]
+~~~~~~~~~~~~~~~~~~~~~~~~
+But the above isn't enough.  Suppose we are *given* d1:Ord a,
 and want to deduce (d2:C [a]) where
 
        class Ord a => C a where
-       instance Ord a => C [a] where ...
+       instance Ord [a] => C [a] where ...
 
-Then we'll use the instance decl to deduce C [a] and then add the
+Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
 superclasses of C [a] to avails.  But we must not overwrite the binding
-for d1:Ord a (which is given) with a superclass selection or we'll just
+for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
 build a loop! 
 
 Here's another variant, immortalised in tcrun020
@@ -1938,77 +1991,104 @@ It's OK: the final zonking stage should zap y to (), which is fine.
 
 \begin{code}
 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
-tcSimplifyTop         wanteds = tc_simplify_top False {- Not interactive loop -} wanteds
-tcSimplifyInteractive wanteds = tc_simplify_top True  {- Interactive loop -}     wanteds
+tcSimplifyTop wanteds
+  = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
+  where 
+    doc = text "tcSimplifyTop"
 
+tcSimplifyInteractive wanteds
+  = tc_simplify_top doc True  {- Interactive loop -}     AddSCs wanteds
+  where 
+    doc = text "tcSimplifyTop"
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
-tc_simplify_top is_interactive wanteds
-  = getLclEnv                                                  `thenM` \ lcl_env ->
-    traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))        `thenM_`
-    simpleReduceLoop (text "tcSimplTop") reduceMe wanteds      `thenM` \ (frees, binds, irreds) ->
-    ASSERT( null frees )
+tc_simplify_top doc is_interactive want_scs wanteds
+  = do { lcl_env <- getLclEnv
+       ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
 
-    let
-               -- All the non-std ones are definite errors
-       (stds, non_stds) = partition isStdClassTyVarDict irreds
+       ; let try_me inst = ReduceMe want_scs
+       ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
+
+       ; let
+               -- First get rid of implicit parameters
+           (non_ips, bad_ips) = partition isClassDict irreds
+
+               -- All the non-tv or multi-param ones are definite errors
+           (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
+           bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
 
                -- Group by type variable
-       std_groups = equivClasses cmp_by_tyvar stds
+           tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
 
                -- Pick the ones which its worth trying to disambiguate
-               -- namely, the onese whose type variable isn't bound
-               -- up with one of the non-standard classes
-       (std_oks, std_bads)     = partition worth_a_try std_groups
-       worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
-       non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
-
-               -- Collect together all the bad guys
-       bad_guys           = non_stds ++ concat std_bads
-       (non_ips, bad_ips) = partition isClassDict bad_guys
-       (ambigs, no_insts) = partition is_ambig non_ips
-       is_ambig d         = not (tyVarsOfInst d `subVarSet` fixed_tvs)
-       fixed_tvs          = oclose (fdPredsOfInsts irreds) emptyVarSet
-       -- If the dict has free type variables, it's almost certainly ambiguous,
-       -- and that's the first thing to fix.  
-       -- Otherwise, addNoInstanceErrs does the right thing
-       -- I say "almost certain" because we might have
-       --       class C a b | a -> B where ...
-       -- plus an Inst (C Int x).  Then the 'x' isn't ambiguous; it's just that
-       -- there's no instance decl for (C Int ...).  Hence the oclose.
-    in
+               -- namely, the ones whose type variable isn't bound
+               -- up with one of the non-tyvar classes
+           (default_gps, non_default_gps) = partition defaultable_group tv_groups
+           defaultable_group ds
+               =  not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
+               && defaultable_classes (map get_clas ds)
+           defaultable_classes clss 
+               | is_interactive = any isInteractiveClass clss
+               | otherwise      = all isStandardClass clss && any isNumericClass clss
+
+           isInteractiveClass cls = isNumericClass cls
+                                 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+                       -- In interactive mode, we default Show a to Show ()
+                       -- to avoid graututious errors on "show []"
+
+    
+                   -- Collect together all the bad guys
+           bad_guys           = non_tvs ++ concat non_default_gps
+           (ambigs, no_insts) = partition isTyVarDict bad_guys
+           -- If the dict has no type constructors involved, it must be ambiguous,
+           -- except I suppose that another error with fundeps maybe should have
+           -- constrained those type variables
 
        -- Report definite errors
-    groupErrs (addNoInstanceErrs Nothing []) no_insts  `thenM_`
-    strangeTopIPErrs bad_ips                           `thenM_`
+       ; ASSERT( null frees )
+         groupErrs (addNoInstanceErrs Nothing []) no_insts
+       ; strangeTopIPErrs bad_ips
 
        -- Deal with ambiguity errors, but only if
-       -- if there has not been an error so far; errors often
-       -- give rise to spurious ambiguous Insts
-    ifErrsM (returnM []) (
-       
-       -- Complain about the ones that don't fall under
-       -- the Haskell rules for disambiguation
-       -- This group includes both non-existent instances
-       --      e.g. Num (IO a) and Eq (Int -> Int)
-       -- and ambiguous dictionaries
-       --      e.g. Num a
-       addTopAmbigErrs ambigs          `thenM_`
-
-       -- Disambiguate the ones that look feasible
-        mappM (disambigGroup is_interactive) std_oks
-    )                                  `thenM` \ binds_ambig ->
-
-    returnM (binds `unionBags` unionManyBags binds_ambig)
+       -- if there has not been an error so far:
+       -- errors often give rise to spurious ambiguous Insts.
+       -- For example:
+       --   f = (*)    -- Monomorphic
+       --   g :: Num a => a -> a
+       --   g x = f x x
+       -- Here, we get a complaint when checking the type signature for g,
+       -- that g isn't polymorphic enough; but then we get another one when
+       -- dealing with the (Num a) context arising from f's definition;
+       -- we try to unify a with Int (to default it), but find that it's
+       -- already been unified with the rigid variable from g's type sig
+       ; binds_ambig <- ifErrsM (returnM []) $
+           do  { -- Complain about the ones that don't fall under
+                 -- the Haskell rules for disambiguation
+                 -- This group includes both non-existent instances
+                 --    e.g. Num (IO a) and Eq (Int -> Int)
+                 -- and ambiguous dictionaries
+                 --    e.g. Num a
+                 addTopAmbigErrs ambigs
+
+                 -- Disambiguate the ones that look feasible
+               ; mappM disambigGroup default_gps }
+
+       ; return (binds `unionBags` unionManyBags binds_ambig) }
 
 ----------------------------------
 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
+is_unary_tyvar_dict :: Inst -> Bool    -- Dicts of form (C a)
+  -- Invariant: argument is a ClassDict, not IP or method
+is_unary_tyvar_dict d = case getDictClassTys d of
+                         (_, [ty]) -> tcIsTyVarTy ty
+                         other     -> False
+
 get_tv d   = case getDictClassTys d of
                   (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
 get_clas d = case getDictClassTys d of
-                  (clas, [ty]) -> clas
+                  (clas, _) -> clas
 \end{code}
 
 If a dictionary constrains a type variable which is
@@ -2044,12 +2124,10 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
-disambigGroup :: Bool  -- True <=> simplifying at top-level interactive loop
-             -> [Inst] -- All standard classes of form (C a)
+disambigGroup :: [Inst]        -- All standard classes of form (C a)
              -> TcM TcDictBinds
 
-disambigGroup is_interactive dicts
-  |   any std_default_class classes    -- Guaranteed all standard classes
+disambigGroup dicts
   =    -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
        -- SO, TRY DEFAULT TYPES IN ORDER
 
@@ -2075,27 +2153,16 @@ disambigGroup is_interactive dicts
     case mb_ty of
        Left  _                 -> bomb_out
        Right chosen_default_ty -> choose_default chosen_default_ty
-
-  | otherwise                          -- No defaults
-  = bomb_out
-
   where
     tyvar   = get_tv (head dicts)      -- Should be non-empty
     classes = map get_clas dicts
 
-    std_default_class cls
-      =  isNumericClass cls
-      || (is_interactive && 
-         classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
-               -- In interactive mode, we default Show a to Show ()
-               -- to avoid graututious errors on "show []"
-
     choose_default default_ty  -- Commit to tyvar = default_ty
       =        -- Bind the type variable 
-       unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
+       unifyType default_ty (mkTyVarTy tyvar)  `thenM_`
        -- and reduce the context, for real this time
        simpleReduceLoop (text "disambig" <+> ppr dicts)
-                    reduceMe dicts                     `thenM` \ (frees, binds, ambigs) ->
+                        reduceMe dicts                 `thenM` \ (frees, binds, ambigs) ->
        WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
        warnDefault dicts default_ty                    `thenM_`
        returnM binds
@@ -2110,6 +2177,7 @@ get_default_tys
                Nothing  ->     -- No use-supplied default;
                                -- use [Integer, Double]
                            do { integer_ty <- tcMetaTy integerTyConName
+                              ; checkWiredInTyCon doubleTyCon
                               ; return [integer_ty, doubleTy] } }
 \end{code}
 
@@ -2118,9 +2186,7 @@ get_default_tys
 
 When typechecking _ccall_s, TcExpr ensures that the external
 function is only passed arguments (and in the other direction,
-results) of a restricted set of 'native' types. This is
-implemented via the help of the pseudo-type classes,
-@CReturnable@ (CR) and @CCallable@ (CC.)
+results) of a restricted set of 'native' types.
 
 The interaction between the defaulting mechanism for numeric
 values and CC & CR can be a bit puzzling to the user at times.
@@ -2139,10 +2205,6 @@ is not an instance of CR. If the default list is equal to
 Haskell 1.4's default-default of (Int, Double), 'x' has type
 Int.
 
-To try to minimise the potential for surprises here, the
-defaulting mechanism is turned off in the presence of
-CCallable and CReturnable.
-
 End of aside]
 
 
@@ -2276,9 +2338,6 @@ groupErrs report_err (inst:insts)
 addInstLoc :: [Inst] -> Message -> Message
 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
 
-plural [x] = empty
-plural xs  = char 's'
-
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
 addTopIPErrs bndrs [] 
   = return ()
@@ -2286,10 +2345,11 @@ addTopIPErrs bndrs ips
   = addErrTcM (tidy_env, mk_msg tidy_ips)
   where
     (tidy_env, tidy_ips) = tidyInsts ips
-    mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
-                           pprBinders bndrs <> colon],
+    mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
+                           nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
+                                           <+> pprBinders bndrs <> colon)],
                       nest 2 (vcat (map ppr_ip ips)),
-                      ptext SLIT("Probably fix: add type signatures for the top-level binding(s)")]
+                      monomorphism_fix]
     ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
 
 strangeTopIPErrs :: [Inst] -> TcM ()
@@ -2311,7 +2371,6 @@ addNoInstanceErrs mb_what givens []
 addNoInstanceErrs mb_what givens dicts
   =    -- Some of the dicts are here because there is no instances
        -- and some because there are too many instances (overlap)
-    getDOpts           `thenM` \ dflags ->
     tcGetInstEnvs      `thenM` \ inst_envs ->
     let
        (tidy_env1, tidy_givens) = tidyInsts givens
@@ -2324,7 +2383,7 @@ addNoInstanceErrs mb_what givens dicts
        check_overlap (overlap_doc, no_inst_dicts) dict 
          | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
          | otherwise
-         = case lookupInstEnv dflags inst_envs clas tys of
+         = case lookupInstEnv inst_envs clas tys of
                -- The case of exactly one match and no unifiers means
                -- a successful lookup.  That can't happen here, becuase
                -- dicts only end up here if they didn't match in Inst.lookupInst
@@ -2354,7 +2413,7 @@ addNoInstanceErrs mb_what givens dicts
       = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
                                        <+> pprPred (dictPred dict))),
                sep [ptext SLIT("Matching instances") <> colon,
-                    nest 2 (vcat [pprDFuns dfuns, pprDFuns unifiers])],
+                    nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
                ASSERT( not (null matches) )
                if not (isSingleton matches)
                then    -- Two or more matches
@@ -2365,10 +2424,10 @@ addNoInstanceErrs mb_what givens dicts
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
                              ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
       where
-       dfuns = [df | (_, (_,_,df)) <- matches]
+       ispecs = [ispec | (_, ispec) <- matches]
 
     mk_probable_fix tidy_env dicts     
-      = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
+      = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
       where
        fixes = add_ors (fix1 ++ fix2)
 
@@ -2385,7 +2444,8 @@ addNoInstanceErrs mb_what givens dicts
                -- Insts for which it is worth suggesting an adding an instance declaration
                -- Exclude implicit parameters, and tyvar dicts
 
-       add_ors :: [SDoc] -> [SDoc]
+       add_ors :: [SDoc] -> [SDoc]     -- The empty case should not happen
+       add_ors []      = [ptext SLIT("[No suggested fixes]")]  -- Strange
        add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
 
 addTopAmbigErrs dicts
@@ -2427,7 +2487,12 @@ mkMonomorphismMsg tidy_env inst_tvs
                        -- whre 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),
-                       ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
+                       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"))
     
 warnDefault dicts default_ty
   = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->