[project @ 2001-05-24 13:59:09 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 7af5b97..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 AddToIrreds            -- 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 AddToIrreds
+       -- 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 AddToIrreds
+       try_me inst | isFreeAndInheritable qtvs inst  = Free
+                   | otherwise                       = ReduceMe 
     in
                -- Step 2
     reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
@@ -614,6 +787,24 @@ and we want to end up with
 But that means that we must simplify the Method for f to (f Int dNumInt)! 
 So tcSimplifyToDicts squeezes out all Methods.
 
+IMPORTANT NOTE:  we *don't* want to do superclass commoning up.  Consider
+
+       fromIntegral :: (Integral a, Num b) => a -> b
+       {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
+
+Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont* 
+want to get
+
+       forall dIntegralInt.
+       fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
+
+because the scsel will mess up matching.  Instead we want
+
+       forall dIntegralInt, dNumInt.
+       fromIntegral Int Int dIntegralInt dNumInt = id Int
+
+Hence "DontReduce NoSCs"
+
 \begin{code}
 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
 tcSimplifyToDicts wanted_lie
@@ -628,8 +819,8 @@ tcSimplifyToDicts wanted_lie
     wanteds = lieToList wanted_lie
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
-    try_me inst        | isDict inst = DontReduce
-               | otherwise   = ReduceMe AddToIrreds
+    try_me inst        | isDict inst = DontReduce NoSCs
+               | otherwise   = ReduceMe
 \end{code}
 
 
@@ -643,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 AddToIrreds
+    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}
 
 
@@ -716,7 +924,7 @@ bindInstsOfLocalFuns init_lie local_ids
                                                -- so it's worth building a set, so that 
                                                -- lookup (in isMethodFor) is faster
 
-    try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
+    try_me inst | isMethodFor overloaded_set inst = ReduceMe
                | otherwise                       = Free
 \end{code}
 
@@ -731,23 +939,22 @@ The main control over context reduction is here
 
 \begin{code}
 data WhatToDo 
- = ReduceMe              -- Try to reduce this
-       NoInstanceAction  -- What to do if there's no such instance
+ = ReduceMe            -- 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.
+                       -- It might be quite legitimate such as (Eq a)!
 
- | DontReduce                  -- Return as irreducible 
+ | DontReduce WantSCs          -- Return as irreducible 
 
  | DontReduceUnlessConstant    -- Return as irreducible unless it can
                                -- be reduced to a constant in one step
 
  | Free                          -- Return as free
 
-data NoInstanceAction
-  = Stop               -- Fail; no error message
-                       -- (Only used when tautology checking.)
-
-  | AddToIrreds                -- Just add the inst to the irreductible ones; don't 
-                       -- produce an error message of any kind.
-                       -- It might be quite legitimate such as (Eq a)!
+data WantSCs = NoSCs | AddSCs  -- Tells whether we should add the superclasses
+                               -- of a predicate when adding it to the avails
 \end{code}
 
 
@@ -817,15 +1024,15 @@ bindsAndIrreds avails wanteds
                                -- For implicit parameters, all occurrences share the same
                                -- Id, so there is no need for synonym bindings
                               new_binds | new_id == id = binds
-                                        | otherwise    = binds `AndMonoBinds` new_bind
-                              new_bind = VarMonoBind new_id (HsVar id)
+                                        | otherwise    = addBind binds new_id (HsVar id)
                               new_id   = instToId w
 
-         Just (Rhs rhs ws') -> go avails' (binds `AndMonoBinds` new_bind) irreds (ws' ++ ws)
+         Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
                             where
                                id       = instToId w
                                avails'  = addToFM avails w (BoundTo id)
-                               new_bind = VarMonoBind id rhs
+
+addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
 \end{code}
 
 
@@ -910,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)
@@ -925,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.
@@ -986,17 +1202,17 @@ reduce stack try_me wanted state
   | otherwise
   = case try_me wanted of {
 
-      DontReduce -> addIrred state wanted
+      DontReduce want_scs -> addIrred want_scs state wanted
 
     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
                                     -- First, see if the inst can be reduced to a constant in one step
-       try_simple addIrred
+       try_simple (addIrred AddSCs)    -- Assume want superclasses
 
     ; Free ->  -- It's free so just chuck it upstairs
                -- First, see if the inst can be reduced to a constant in one step
        try_simple addFree
 
-    ; ReduceMe no_instance_action ->   -- It should be reduced
+    ; ReduceMe ->              -- It should be reduced
        lookupInst wanted             `thenNF_Tc` \ lookup_result ->
        case lookup_result of
            GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' -> 
@@ -1004,9 +1220,8 @@ reduce stack try_me wanted state
            SimpleInst rhs       -> addWanted state wanted rhs []
 
            NoInstance ->    -- No such instance! 
-                   case no_instance_action of
-                       Stop        -> failTc           
-                       AddToIrreds -> addIrred state wanted
+                            -- Add it and its superclasses
+                            addIrred AddSCs state wanted
 
     }
   where
@@ -1083,41 +1298,42 @@ addWanted state@(avails, frees) wanted rhs_expr wanteds
          | otherwise                  = ASSERT( null wanteds ) NoRhs
 
 addGiven :: RedState -> Inst -> NF_TcM RedState
-addGiven state given = add_avail state given (BoundTo (instToId given))
+addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
 
-addIrred :: RedState -> Inst -> NF_TcM RedState
-addIrred state irred = add_avail state irred Irred
+addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
+addIrred NoSCs  (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
+addIrred AddSCs state         irred = addAvailAndSCs state irred Irred
 
-add_avail :: RedState -> Inst -> Avail -> NF_TcM RedState
-add_avail (avails, frees) wanted avail
-  = addAvail avails wanted avail       `thenNF_Tc` \ avails' ->
+addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
+addAvailAndSCs (avails, frees) wanted avail
+  = add_avail_and_scs avails wanted avail      `thenNF_Tc` \ avails' ->
     returnNF_Tc (avails', frees)
 
 ---------------------
-addAvail :: Avails -> Inst -> Avail -> NF_TcM Avails
-addAvail avails wanted avail
-  = addSuperClasses (addToFM avails wanted avail) wanted
+add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
+add_avail_and_scs avails wanted avail
+  = add_scs (addToFM avails wanted avail) wanted
 
-addSuperClasses :: Avails -> Inst -> NF_TcM Avails
+add_scs :: Avails -> Inst -> NF_TcM Avails
        -- Add all the superclasses of the Inst to Avails
        -- Invariant: the Inst is already in Avails.
 
-addSuperClasses avails dict
+add_scs avails dict
   | not (isClassDict dict)
   = returnNF_Tc avails
 
   | otherwise  -- It is a dictionary
   = newDictsFromOld dict sc_theta'     `thenNF_Tc` \ sc_dicts ->
-    foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_dicts sc_sels)
+    foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
   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
          Just (BoundTo _) -> returnNF_Tc avails        -- See Note [SUPER] below
-         other            -> addAvail avails sc_dict avail
+         other            -> add_avail_and_scs avails sc_dict avail
       where
        sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
        avail      = Rhs sc_sel_rhs [dict]
@@ -1214,7 +1430,7 @@ tcSimplifyTop wanted_lie
     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
   where
     wanteds    = lieToList wanted_lie
-    try_me inst        = ReduceMe AddToIrreds
+    try_me inst        = ReduceMe
 
     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
@@ -1261,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
@@ -1292,7 +1508,7 @@ disambigGroup dicts
     returnTc EmptyMonoBinds
 
   where
-    try_me inst = ReduceMe AddToIrreds         -- This reduce should not fail
+    try_me inst = ReduceMe                     -- This reduce should not fail
     tyvar       = get_tv (head dicts)          -- Should be non-empty
     classes     = map get_clas dicts
 \end{code}
@@ -1347,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 ->
@@ -1359,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
@@ -1376,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
@@ -1391,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
@@ -1417,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
@@ -1471,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
@@ -1491,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)
@@ -1503,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
@@ -1553,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
@@ -1572,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,