[project @ 2001-05-24 13:59:09 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 2e6c240..1cb0ca4 100644 (file)
@@ -7,8 +7,10 @@
 
 \begin{code}
 module TcSimplify (
-       tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, 
+       tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck,
+       tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop, 
+
        tcSimplifyThetas, tcSimplifyCheckThetas,
        bindInstsOfLocalFuns
     ) where
@@ -22,14 +24,14 @@ import TcHsSyn              ( TcExpr, TcId,
 
 import TcMonad
 import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
-                         tyVarsOfInst, predsOfInsts, 
-                         isDict, isClassDict, 
+                         tyVarsOfInst, predsOfInsts, predsOfInst,
+                         isDict, isClassDict, instName,
                          isStdClassTyVarDict, isMethodFor,
                          instToId, tyVarsOfInsts,
                          instBindingRequired, instCanBeGeneralised,
                          newDictsFromOld, instMentionsIPs,
-                         getDictClassTys, getIPs, isTyVarDict,
-                         instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
+                         getDictClassTys, isTyVarDict,
+                         instLoc, pprInst, zonkInst, tidyInsts,
                          Inst, LIE, pprInsts, pprInstsInFull,
                          mkLIE, lieToList 
                        )
@@ -39,24 +41,24 @@ import InstEnv              ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
 import TcType          ( zonkTcTyVarsAndFV, tcInstTyVars )
 import TcUnify         ( unifyTauTy )
 import Id              ( idType )
-import Name            ( Name )
 import NameSet         ( mkNameSet )
-import Class           ( Class, classBigSig )
+import Class           ( classBigSig )
 import FunDeps         ( oclose, grow, improve )
 import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass )
 
-import Type            ( Type, ClassContext,
-                         mkTyVarTy, getTyVar, 
-                         isTyVarTy, splitSigmaTy, tyVarsOfTypes
+import Type            ( ThetaType, PredType, mkClassPred,
+                         mkTyVarTy, getTyVar, isTyVarClassPred,
+                         splitSigmaTy, tyVarsOfPred,
+                         getClassPredTys_maybe, isClassPred, isIPPred,
+                         inheritablePred, predHasFDs
                        )
-import Subst           ( mkTopTyVarSubst, substClasses, substTy )
-import PprType         ( pprClassPred )
+import Subst           ( mkTopTyVarSubst, substTheta, substTy )
 import TysWiredIn      ( unitTy )
 import VarSet
 import FiniteMap
 import Outputable
 import ListSetOps      ( equivClasses )
-import Util            ( zipEqual, mapAccumL )
+import Util            ( zipEqual )
 import List            ( partition )
 import CmdLineOpts
 \end{code}
@@ -231,7 +233,7 @@ However, we don't *need* to report ambiguity right away.  It'll always
 show up at the call site.... and eventually at main, which needs special
 treatment.  Nevertheless, reporting ambiguity promptly is an excellent thing.
 
-So heres the plan.  We WARN about probable ambiguity if
+So here's the plan.  We WARN about probable ambiguity if
 
        fv(Cq) is not a subset of  oclose(fv(T) union fv(G), C)
 
@@ -279,65 +281,173 @@ is a "bubble" that's a set of constraints
 Hence another idea.  To decide Q start with fv(T) and grow it
 by transitive closure in Cq (no functional dependencies involved).
 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
-The definitely-ambigous can then float out, and get smashed at top level
+The definitely-ambiguous can then float out, and get smashed at top level
 (which squashes out the constants, like Eq (T a) above)
 
 
        --------------------------------------  
+               Notes on principal types
+       --------------------------------------  
+
+    class C a where
+      op :: a -> a
+    
+    f x = let g y = op (y::Int) in True
+
+Here the principal type of f is (forall a. a->a)
+but we'll produce the non-principal type
+    f :: forall a. C Int => a -> a
+
+
+       --------------------------------------  
                Notes on implicit parameters
        --------------------------------------  
 
-Consider
+Question 1: can we "inherit" implicit parameters
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
 
-       f x = ...?y...
+       f x = (x::Int) + ?y
 
-Then we get an LIE like (?y::Int).  Doesn't constrain a type variable,
-but we must nevertheless infer a type like
+where f is *not* a top-level binding.
+From the RHS of f we'll get the constraint (?y::Int).
+There are two types we might infer for f:
+
+       f :: Int -> Int
+
+(so we get ?y from the context of f's definition), or
 
        f :: (?y::Int) => Int -> Int
 
-so that f is passed the value of y at the call site.  Is this legal?
-       
+At first you might think the first was better, becuase then
+?y behaves like a free variable of the definition, rather than
+having to be passed at each call site.  But of course, the WHOLE
+IDEA is that ?y should be passed at each call site (that's what
+dynamic binding means) so we'd better infer the second.
+
+BOTTOM LINE: you *must* quantify over implicit parameters.
+
+
+Question 2: type signatures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+OK, so it it legal to give an explicit, user type signature to f, thus:
+
        f :: Int -> Int
-       f x = x + ?y
+       f x = (x::Int) + ?y
 
-Should f be overloaded on "?y" ?  Or does the type signature say that it
-shouldn't be?  Our position is that it should be illegal.  Otherwise
-you can change the *dynamic* semantics by adding a type signature:
+At first sight this seems reasonable, but it has the nasty property
+that adding a type signature changes the dynamic semantics.=20
+Consider this:
 
-       (let f x = x + ?y       -- f :: (?y::Int) => Int -> Int
+       (let f x = (x::Int) + ?y
         in (f 3, f 3 with ?y=5))  with ?y = 6
 
                returns (3+6, 3+5)
 vs
-       (let f :: Int -> Int 
-           f x = x + ?y
+       (let f :: Int -> Int=20
+            f x = x + ?y
         in (f 3, f 3 with ?y=5))  with ?y = 6
 
                returns (3+6, 3+6)
 
-URK!  Let's not do this. So this is illegal:
+Indeed, simply inlining f (at the Haskell source level) would change the
+dynamic semantics.
 
-       f :: Int -> Int
-       f x = x + ?y
+Conclusion: the above type signature is illegal.  You'll get a message
+of the form "could not deduce (?y::Int) from ()".
 
-BOTTOM LINE: you *must* quantify over implicit parameters.
 
+Question 3: monomorphism
+~~~~~~~~~~~~~~~~~~~~~~~~
+There's a nasty corner case when the monomorphism restriction bites:
 
-       --------------------------------------  
-               Notes on principal types
-       --------------------------------------  
+       z = (x::Int) + ?y
 
-    class C a where
-      op :: a -> a
-    
-    f x = let g y = op (y::Int) in True
+The argument above suggests that we *must* generalise=20
+over the ?y parameter, to get=20
+       z :: (?y::Int) => Int,
+but the monomorphism restriction says that we *must not*, giving
+       z :: Int. =20
+Why does the momomorphism restriction say this?  Because if you have
 
-Here the principal type of f is (forall a. a->a)
-but we'll produce the non-principal type
-    f :: forall a. C Int => a -> a
+       let z = x + ?y in z+z
+
+you might not expect the addition to be done twice --- but it will if
+we follow the argument of Question 2 and generalise over ?y.
+
+
+
+Possible choices
+~~~~~~~~~~~~~~~~
+(A) Always generalise over implicit parameters
+    Bindings that fall under the monomorphism restriction can't
+       be generalised
+
+    Consequences:
+       * Inlning remains valid
+       * No unexpected loss of sharing
+       * But simple bindings like
+               z = ?y + 1
+         will be rejected, unless you add an explicit type signature
+         (to avoid the monomorphism restriction)
+               z :: (?y::Int) => Int
+               z = ?y + 1
+         This seems unacceptable
+
+(B) Monomorphism restriction "wins"
+    Bindings that fall under the monomorphism restriction can't
+       be generalised
+    Always generalise over implicit parameters *except* for bindings
+       that fall under the monomorphism restriction
+
+    Consequences
+       * Inlining isn't valid in general
+       * No unexpected loss of sharing
+       * Simple bindings like
+               z = ?y + 1
+         accepted (get value of ?y from binding site)
+
+(C) Always generalise over implicit parameters
+    Bindings that fall under the monomorphism restriction can't
+       be generalised, EXCEPT for implicit parameters
+    Consequences
+       * Inlining remains valid
+       * Unexpected loss of sharing (from the extra generalisation)
+       * Simple bindings like
+               z = ?y + 1
+         accepted (get value of ?y from occurrence sites)
+
+
+Discussion
+~~~~~~~~~~
+None of these choices seems very satisfactory.  But at least we should
+decide which we want to do.
+
+It's really not clear what is the Right Thing To Do.  If you see
+
+       z = (x::Int) + ?y
+
+would you expect the value of ?y to be got from the *occurrence sites*
+of 'z', or from the valuue of ?y at the *definition* of 'z'?  In the
+case of function definitions, the answer is clearly the former, but
+less so in the case of non-fucntion definitions.   On the other hand,
+if we say that we get the value of ?y from the definition site of 'z',
+then inlining 'z' might change the semantics of the program.
+
+Choice (C) really says "the monomorphism restriction doesn't apply
+to implicit parameters".  Which is fine, but remember that every=20
+innocent binding 'x = ...' that mentions an implicit parameter in
+the RHS becomes a *function* of that parameter, called at each
+use of 'x'.  Now, the chances are that there are no intervening 'with'
+clauses that bind ?y, so a decent compiler should common up all=20
+those function calls.  So I think I strongly favour (C).  Indeed,
+one could make a similar argument for abolishing the monomorphism
+restriction altogether.
+
+BOTTOM LINE: we choose (B) at present.  See tcSimplifyRestricted
 
        
+
 %************************************************************************
 %*                                                                     *
 \subsection{tcSimplifyInfer}
@@ -406,9 +516,9 @@ inferLoop doc tau_tvs wanteds
        qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
        
        try_me inst     
-         | isFree qtvs inst  = Free
-         | isClassDict inst  = DontReduceUnlessConstant        -- Dicts
-         | otherwise         = ReduceMe                        -- Lits and Methods
+         | isFreeAndInheritable qtvs inst = Free
+         | isClassDict inst               = DontReduceUnlessConstant   -- Dicts
+         | otherwise                      = ReduceMe                   -- Lits and Methods
     in
                -- Step 2
     reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
@@ -451,10 +561,12 @@ on both the Lte and If constraints.  What we *can't* do is start again
 with (Max Z (S x) y)!
 
 \begin{code}
-isFree qtvs inst
-  =  not (tyVarsOfInst inst `intersectsVarSet` qtvs)   -- Constrains no quantified vars
-  && null (getIPs inst)                                        -- And no implicit parameter involved
+isFreeAndInheritable qtvs inst
+  =  isFree qtvs inst                                  -- Constrains no quantified vars
+  && all inheritablePred (predsOfInst inst)            -- And no implicit parameter involved
                                                        -- (see "Notes on implicit parameters")
+
+isFree qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
 \end{code}
 
 
@@ -486,24 +598,25 @@ tcSimplifyCheck doc qtvs givens wanted_lie
     returnTc (mkLIE frees, binds)
 
 checkLoop doc qtvs givens wanteds
-  =    -- Step 1
+  =            -- Step 1
     zonkTcTyVarsAndFV qtvs             `thenNF_Tc` \ qtvs' ->
     mapNF_Tc zonkInst givens           `thenNF_Tc` \ givens' ->
     mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
+
+               -- Step 2
     let
-             -- When checking against a given signature we always reduce
-             -- until we find a match against something given, or can't reduce
-       try_me inst | isFree qtvs' inst  = Free
-                   | otherwise          = ReduceMe 
+       -- When checking against a given signature we always reduce
+       -- until we find a match against something given, or can't reduce
+       try_me inst | isFreeAndInheritable qtvs' inst = Free
+                   | otherwise                       = ReduceMe 
     in
-               -- Step 2
-    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+    reduceContext doc try_me givens' wanteds'  `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
        returnTc (frees, binds, irreds)
     else
-       checkLoop doc qtvs givens' (irreds ++ frees)    `thenTc` \ (frees1, binds1, irreds1) ->
+       checkLoop doc qtvs givens' (irreds ++ frees)    `thenTc` \ (frees1, binds1, irreds1) ->
        returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
 
 complainCheck doc givens irreds
@@ -517,6 +630,66 @@ complainCheck doc givens irreds
 \end{code}
 
 
+%************************************************************************
+%*                                                                     *
+\subsection{tcSimplifyRestricted}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+tcSimplifyRestricted   -- Used for restricted binding groups
+       :: SDoc 
+       -> [TcTyVar]            -- Free in the type of the RHSs
+       -> LIE                  -- Free in the RHSs
+       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
+               LIE,            -- Free
+               TcDictBinds)    -- Bindings
+
+tcSimplifyRestricted doc tau_tvs wanted_lie
+  =    -- First squash out all methods, to find the constrained tyvars
+       -- We can't just take the free vars of wanted_lie because that'll 
+       -- have methods that may incidentally mention entirely unconstrained variables
+       --      e.g. a call to  f :: Eq a => a -> b -> b
+       -- Here, b is unconstrained.  A good example would be
+       --      foo = f (3::Int)
+       -- We want to infer the polymorphic type
+       --      foo :: forall b. b -> b
+    tcSimplifyToDicts wanted_lie       `thenTc` \ (dicts, _) ->
+    let
+       constrained_tvs = tyVarsOfInsts dicts
+    in
+
+       -- Next, figure out the tyvars we will quantify over
+    zonkTcTyVarsAndFV tau_tvs          `thenNF_Tc` \ tau_tvs' ->
+    tcGetGlobalTyVars                  `thenNF_Tc` \ gbl_tvs ->
+    let
+       qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts dicts) gbl_tvs)
+                        `minusVarSet` constrained_tvs
+    in
+
+       -- The first step may have squashed more methods than
+       -- necessary, so try again, this time knowing the exact
+       -- set of type variables to quantify over.
+       --
+       -- We quantify only over constraints that are captured by qtvs; 
+       -- these will just be a subset of non-dicts.  This in contrast
+       -- to normal inference (using isFreeAndInheritable) in which we quantify over 
+       -- all *non-inheritable* constraints too.  This implements choice 
+       -- (B) under "implicit parameter and monomorphism" above.
+    mapNF_Tc zonkInst (lieToList wanted_lie)   `thenNF_Tc` \ wanteds' ->
+    let
+        try_me inst | isFree qtvs inst = Free
+                   | otherwise        = ReduceMe
+    in
+    reduceContext doc try_me [] wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
+    ASSERT( no_improvement )
+    ASSERT( null irreds )
+       -- No need to loop because tcSimplifyToDicts will have
+       -- already done any improvement necessary
+
+    returnTc (varSetElems qtvs, mkLIE frees, binds)
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -524,7 +697,7 @@ complainCheck doc givens irreds
 %*                                                                     *
 %************************************************************************
 
-@tcSimplifyInferCheck@ is used when we know the consraints we are to simplify
+@tcSimplifyInferCheck@ is used when we know the constraints we are to simplify
 against, but we don't know the type variables over which we are going to quantify.
 This happens when we have a type signature for a mutually recursive
 group.
@@ -572,8 +745,8 @@ inferCheckLoop doc tau_tvs givens wanteds
 
              -- When checking against a given signature we always reduce
              -- until we find a match against something given, or can't reduce
-       try_me inst | isFree qtvs inst  = Free
-                   | otherwise         = ReduceMe 
+       try_me inst | isFreeAndInheritable qtvs inst  = Free
+                   | otherwise                       = ReduceMe 
     in
                -- Step 2
     reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
@@ -661,28 +834,45 @@ When we have
        let ?x = R in B
 
 we must discharge all the ?x constraints from B.  We also do an improvement
-step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.  No need to iterate, though.
+step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.  
+
+Actually, the constraints from B might improve the types in ?x. For example
+
+       f :: (?x::Int) => Char -> Char
+       let ?x = 3 in f 'c'
+
+then the constraint (?x::Int) arising from the call to f will 
+force the binding for ?x to be of type Int.
 
 \begin{code}
-tcSimplifyIPs :: [Name]                -- The implicit parameters bound here
+tcSimplifyIPs :: [Inst]                -- The implicit parameters bound here
              -> LIE
              -> TcM (LIE, TcDictBinds)
-tcSimplifyIPs ip_names wanted_lie
-  = simpleReduceLoop doc try_me wanteds        `thenTc` \ (frees, binds, irreds) ->
-       -- The irreducible ones should be a subset of the implicit
-       -- parameters we provided
-    ASSERT( all here_ip irreds )
+tcSimplifyIPs given_ips wanted_lie
+  = simpl_loop given_ips wanteds       `thenTc` \ (frees, binds) ->
     returnTc (mkLIE frees, binds)
-    
   where
-    doc            = text "tcSimplifyIPs" <+> ppr ip_names
-    wanteds = lieToList wanted_lie
-    ip_set  = mkNameSet ip_names
-    here_ip ip = isDict ip && ip `instMentionsIPs` ip_set
-
+    doc             = text "tcSimplifyIPs" <+> ppr ip_names
+    wanteds  = lieToList wanted_lie
+    ip_names = map instName given_ips
+    ip_set   = mkNameSet ip_names
+  
        -- Simplify any methods that mention the implicit parameter
     try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
                | otherwise                     = Free
+
+    simpl_loop givens wanteds
+      = mapNF_Tc zonkInst givens               `thenNF_Tc` \ givens' ->
+        mapNF_Tc zonkInst wanteds              `thenNF_Tc` \ wanteds' ->
+  
+        reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+        if no_improvement then
+           ASSERT( null irreds )
+           returnTc (frees, binds)
+       else
+           simpl_loop givens' (irreds ++ frees)        `thenTc` \ (frees1, binds1) ->
+           returnTc (frees1, binds `AndMonoBinds` binds1)
 \end{code}
 
 
@@ -927,7 +1117,12 @@ reduceContext doc try_me givens wanteds
 tcImprove avails
  =  tcGetInstEnv                               `thenTc` \ inst_env ->
     let
-       preds = predsOfInsts (keysFM avails)
+       preds = [ (pred, pp_loc)
+               | inst <- keysFM avails,
+                 let pp_loc = pprInstLoc (instLoc inst),
+                 pred <- predsOfInst inst,
+                 predHasFDs pred
+               ]
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
                -- It does not have duplicates (good)
@@ -942,10 +1137,14 @@ tcImprove avails
         mapTc_ unify eqns      `thenTc_`
        returnTc False
   where
-    unify (qtvs, t1, t2) = tcInstTyVars (varSetElems qtvs)     `thenNF_Tc` \ (_, _, tenv) ->
-                          unifyTauTy (substTy tenv t1) (substTy tenv t2)
-    ppr_eqn (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) <+>
-                            ppr t1 <+> equals <+> ppr t2
+    unify ((qtvs, t1, t2), doc)
+        = tcAddErrCtxt doc                     $
+          tcInstTyVars (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
+          unifyTauTy (substTy tenv t1) (substTy tenv t2)
+    ppr_eqn ((qtvs, t1, t2), doc)
+       = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
+                                    <+> ppr t1 <+> equals <+> ppr t2,
+               doc]
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -1129,7 +1328,7 @@ add_scs avails dict
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
-    sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
+    sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
 
     add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
       = case lookupFM avails sc_dict of
@@ -1278,10 +1477,10 @@ disambigGroup dicts
       try_default (default_ty : default_tys)
        = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
                                                -- default_tys instead
-         tcSimplifyCheckThetas [] thetas       `thenTc` \ _ ->
+         tcSimplifyCheckThetas [] theta        `thenTc` \ _ ->
          returnTc default_ty
         where
-         thetas = classes `zip` repeat [default_ty]
+         theta = [mkClassPred clas [default_ty] | clas <- classes]
     in
        -- See if any default works, and if so bind the type variable to it
        -- If not, add an AmbigErr
@@ -1364,8 +1563,8 @@ a,b,c are type variables.  This is required for the context of
 instance declarations.
 
 \begin{code}
-tcSimplifyThetas :: ClassContext               -- Wanted
-                -> TcM ClassContext            -- Needed
+tcSimplifyThetas :: ThetaType          -- Wanted
+                -> TcM ThetaType               -- Needed
 
 tcSimplifyThetas wanteds
   = doptsTc Opt_GlasgowExts            `thenNF_Tc` \ glaExts ->
@@ -1376,10 +1575,10 @@ tcSimplifyThetas wanteds
        -- we expect an instance here
        -- For Haskell 98, check that all the constraints are of the form C a,
        -- where a is a type variable
-       bad_guys | glaExts   = [ct | ct@(clas,tys) <- irreds, 
-                                    isEmptyVarSet (tyVarsOfTypes tys)]
-                | otherwise = [ct | ct@(clas,tys) <- irreds, 
-                                    not (all isTyVarTy tys)]
+       bad_guys | glaExts   = [pred | pred <- irreds, 
+                                      isEmptyVarSet (tyVarsOfPred pred)]
+                | otherwise = [pred | pred <- irreds, 
+                                      not (isTyVarClassPred pred)]
     in
     if null bad_guys then
        returnTc irreds
@@ -1393,8 +1592,8 @@ used with \tr{default} declarations.  We are only interested in
 whether it worked or not.
 
 \begin{code}
-tcSimplifyCheckThetas :: ClassContext  -- Given
-                     -> ClassContext   -- Wanted
+tcSimplifyCheckThetas :: ThetaType     -- Given
+                     -> ThetaType      -- Wanted
                      -> TcM ()
 
 tcSimplifyCheckThetas givens wanteds
@@ -1408,23 +1607,23 @@ tcSimplifyCheckThetas givens wanteds
 
 
 \begin{code}
-type AvailsSimple = FiniteMap (Class,[Type]) Bool
+type AvailsSimple = FiniteMap PredType Bool
                    -- True  => irreducible 
                    -- False => given, or can be derived from a given or from an irreducible
 
-reduceSimple :: ClassContext                   -- Given
-            -> ClassContext                    -- Wanted
-            -> NF_TcM ClassContext             -- Irreducible
+reduceSimple :: ThetaType                      -- Given
+            -> ThetaType                       -- Wanted
+            -> NF_TcM ThetaType                -- Irreducible
 
 reduceSimple givens wanteds
   = reduce_simple (0,[]) givens_fm wanteds     `thenNF_Tc` \ givens_fm' ->
-    returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
+    returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
   where
     givens_fm     = foldl addNonIrred emptyFM givens
 
-reduce_simple :: (Int,ClassContext)            -- Stack
+reduce_simple :: (Int,ThetaType)               -- Stack
              -> AvailsSimple
-             -> ClassContext
+             -> ThetaType
              -> NF_TcM AvailsSimple
 
 reduce_simple (n,stack) avails wanteds
@@ -1434,32 +1633,36 @@ reduce_simple (n,stack) avails wanteds
     go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w       `thenNF_Tc` \ avails' ->
                       go avails' ws
 
-reduce_simple_help stack givens wanted@(clas,tys)
+reduce_simple_help stack givens wanted
   | wanted `elemFM` givens
   = returnNF_Tc givens
 
-  | otherwise
+  | Just (clas, tys) <- getClassPredTys_maybe wanted
   = lookupSimpleInst clas tys  `thenNF_Tc` \ maybe_theta ->
-
     case maybe_theta of
       Nothing ->    returnNF_Tc (addSimpleIrred givens wanted)
       Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
 
-addSimpleIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
-addSimpleIrred givens ct@(clas,tys)
-  = addSCs (addToFM givens ct True) ct
+  | otherwise
+  = returnNF_Tc (addSimpleIrred givens wanted)
+
+addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
+addSimpleIrred givens pred
+  = addSCs (addToFM givens pred True) pred
 
-addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
-addNonIrred givens ct@(clas,tys)
-  = addSCs (addToFM givens ct False) ct
+addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
+addNonIrred givens pred
+  = addSCs (addToFM givens pred False) pred
 
-addSCs givens ct@(clas,tys)
- = foldl add givens sc_theta
+addSCs givens pred
+  | not (isClassPred pred) = givens
+  | otherwise             = foldl add givens sc_theta
  where
+   Just (clas,tys) = getClassPredTys_maybe pred
    (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
-   sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
+   sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
 
-   add givens ct@(clas, tys)
+   add givens ct
      = case lookupFM givens ct of
        Nothing    -> -- Add it and its superclasses
                     addSCs (addToFM givens ct False) ct
@@ -1488,8 +1691,8 @@ addTopAmbigErrs dicts
   = mapNF_Tc complain tidy_dicts
   where
     fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
-    (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
-    complain d | not (null (getIPs d))               = addTopIPErr tidy_env d
+    (tidy_env, tidy_dicts) = tidyInsts dicts
+    complain d | any isIPPred (predsOfInst d)        = addTopIPErr tidy_env d
               | not (isTyVarDict d) ||
                 tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
               | otherwise                            = addAmbigErr tidy_env d
@@ -1508,7 +1711,7 @@ addTopInstanceErr tidy_env tidy_dict
 addAmbigErrs dicts
   = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
   where
-    (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
+    (tidy_env, tidy_dicts) = tidyInsts dicts
 
 addAmbigErr tidy_env tidy_dict
   = addInstErrTcM (instLoc tidy_dict)
@@ -1520,26 +1723,14 @@ addAmbigErr tidy_env tidy_dict
 
 warnDefault dicts default_ty
   = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
-    if warn_flag 
-       then mapNF_Tc warn groups  `thenNF_Tc_`  returnNF_Tc ()
-       else returnNF_Tc ()
-
+    tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
   where
        -- Tidy them first
-    (_, tidy_dicts) = mapAccumL tidyInst emptyTidyEnv dicts
-
-       -- Group the dictionaries by source location
-    groups      = equivClasses cmp tidy_dicts
-    i1 `cmp` i2 = get_loc i1 `compare` get_loc i2
-    get_loc i   = case instLoc i of { (_,loc,_) -> loc }
-
-    warn [dict] = tcAddSrcLoc (get_loc dict) $
-                 warnTc True (ptext SLIT("Defaulting") <+> quotes (pprInst dict) <+> 
-                              ptext SLIT("to type") <+> quotes (ppr default_ty))
-
-    warn dicts  = tcAddSrcLoc (get_loc (head dicts)) $
-                 warnTc True (vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty),
-                                    pprInstsInFull dicts])
+    (_, tidy_dicts) = tidyInsts dicts
+    get_loc i = case instLoc i of { (_,loc,_) -> loc }
+    warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> 
+                               quotes (ppr default_ty),
+                     pprInstsInFull tidy_dicts]
 
 -- The error message when we don't find a suitable instance
 -- is complicated by the fact that sometimes this is because
@@ -1570,12 +1761,14 @@ addNoInstanceErr what_doc givens dict
        fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
                    ptext SLIT("to the") <+> what_doc]
     
-       fix2 | isTyVarDict dict || ambig_overlap
+       fix2 | isTyVarDict dict 
+            || not (isClassDict dict)  -- Don't suggest adding instance declarations for implicit parameters
+            || ambig_overlap 
             = empty
             | otherwise
             = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
     
-       (tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
+       (tidy_env, tidy_dict:tidy_givens) = tidyInsts (dict:givens)
     
            -- Checks for the ambiguous case when we have overlapping instances
        ambig_overlap | isClassDict dict
@@ -1589,8 +1782,8 @@ addNoInstanceErr what_doc givens dict
     addInstErrTcM (instLoc dict) (tidy_env, doc)
 
 -- Used for the ...Thetas variants; all top level
-addNoInstErr (c,ts)
-  = addErrTc (ptext SLIT("No instance for") <+> quotes (pprClassPred c ts))
+addNoInstErr pred
+  = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
 
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,