[project @ 2001-05-03 09:32:48 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index e81409a..85762b0 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,17 +24,16 @@ 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, plusLIE, isEmptyLIE,
-                         lieToList 
+                         mkLIE, lieToList 
                        )
 import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
@@ -42,22 +43,23 @@ 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            ( 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}
@@ -232,7 +234,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)
 
@@ -280,7 +282,7 @@ 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)
 
 
@@ -322,6 +324,15 @@ URK!  Let's not do this. So this is illegal:
        f :: Int -> Int
        f x = x + ?y
 
+There's a nasty corner case when the monomorphism restriction bites:
+
+       f = x + ?y
+
+The argument above suggests that we must generalise over the ?y parameter, 
+but the monomorphism restriction says that we can't.  The current 
+implementation chooses to let the monomorphism restriction 'win' in this
+case, but it's not clear what the Right Thing is.
+
 BOTTOM LINE: you *must* quantify over implicit parameters.
 
 
@@ -395,7 +406,7 @@ tcSimplifyInfer doc tau_tvs wanted_lie
        -- Check for non-generalisable insts
     mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)  `thenTc_`
 
-    returnTc (qtvs, frees, binds, map instToId irreds)
+    returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
 
 inferLoop doc tau_tvs wanteds
   =    -- Step 1
@@ -409,21 +420,29 @@ inferLoop doc tau_tvs wanteds
        try_me inst     
          | isFree qtvs inst  = Free
          | isClassDict inst  = DontReduceUnlessConstant        -- Dicts
-         | otherwise         = ReduceMe AddToIrreds            -- Lits and Methods
+         | otherwise         = ReduceMe                        -- Lits and Methods
     in
                -- Step 2
     reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
-           returnTc (varSetElems qtvs, frees, binds, irreds)
+       returnTc (varSetElems qtvs, frees, binds, irreds)
     else
-               -- We start again with irreds, not wanteds
-               -- Using an instance decl might have introduced a fresh type variable
-               -- which might have been unified, so we'd get an infinite loop
-               -- if we started again with wanteds!  See example [LOOP]
-           inferLoop doc tau_tvs irreds        `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
-           returnTc (qtvs1, frees1 `plusLIE` frees, binds `AndMonoBinds` binds1, irreds1)
+       -- If improvement did some unification, we go round again.  There
+       -- are two subtleties:
+       --   a) We start again with irreds, not wanteds
+       --      Using an instance decl might have introduced a fresh type variable
+       --      which might have been unified, so we'd get an infinite loop
+       --      if we started again with wanteds!  See example [LOOP]
+       --
+       --   b) It's also essential to re-process frees, because unification
+       --      might mean that a type variable that looked free isn't now.
+       --
+       -- Hence the (irreds ++ frees)
+
+       inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+       returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}     
 
 Example [LOOP]
@@ -446,7 +465,7 @@ 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
+  && all inheritablePred (predsOfInst inst)            -- And no implicit parameter involved
                                                        -- (see "Notes on implicit parameters")
 \end{code}
 
@@ -458,7 +477,7 @@ isFree qtvs inst
 %************************************************************************
 
 @tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over.
+we are going to quantify over.  For example, a class or instance declaration.
 
 \begin{code}
 tcSimplifyCheck
@@ -470,34 +489,46 @@ tcSimplifyCheck
                 TcDictBinds)   -- Bindings
 
 tcSimplifyCheck doc qtvs givens wanted_lie
-  = checkLoop doc qtvs givens (lieToList wanted_lie)   `thenTc` \ (frees, binds, irreds) ->
+  = checkLoop doc qtvs givens (lieToList wanted_lie) try `thenTc` \ (frees, binds, irreds) ->
 
        -- Complain about any irreducible ones
     complainCheck doc givens irreds            `thenNF_Tc_`
 
        -- Done
-    returnTc (frees, binds)
+    returnTc (mkLIE frees, binds)
+  where
+       -- When checking against a given signature we always reduce
+       -- until we find a match against something given, or can't reduce
+    try qtvs inst | isFree qtvs inst  = Free
+                 | otherwise         = ReduceMe 
 
-checkLoop doc qtvs givens wanteds
-  =    -- Step 1
+tcSimplifyRestricted doc qtvs givens wanted_lie
+  = checkLoop doc qtvs givens (lieToList wanted_lie) try `thenTc` \ (frees, binds, irreds) ->
+
+       -- Complain about any irreducible ones
+    complainCheck doc givens irreds            `thenNF_Tc_`
+
+       -- Done
+    returnTc (mkLIE frees, binds)
+  where
+    try qtvs inst | not (tyVarsOfInst inst `intersectsVarSet` qtvs) = Free
+                 | otherwise                                       = ReduceMe
+
+checkLoop doc qtvs givens wanteds try_me
+  =            -- Step 1
     zonkTcTyVarsAndFV qtvs             `thenNF_Tc` \ qtvs' ->
     mapNF_Tc zonkInst givens           `thenNF_Tc` \ givens' ->
     mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
-    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
-    in
+
                -- Step 2
-    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+    reduceContext doc (try_me qtvs') givens' wanteds'          `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
-           returnTc (frees, binds, irreds)
+       returnTc (frees, binds, irreds)
     else
-           checkLoop doc qtvs givens irreds    `thenTc` \ (frees1, binds1, irreds1) ->
-           returnTc (frees `plusLIE` frees1, binds `AndMonoBinds` binds1, irreds1)
+       checkLoop doc qtvs givens' (irreds ++ frees) try_me     `thenTc` \ (frees1, binds1, irreds1) ->
+       returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
 
 complainCheck doc givens irreds
   = mapNF_Tc zonkInst given_dicts                      `thenNF_Tc` \ givens' ->
@@ -519,6 +550,8 @@ complainCheck doc givens irreds
 
 @tcSimplifyInferCheck@ is used when we know the consraints 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.
 
 \begin{code}
 tcSimplifyInferCheck
@@ -537,7 +570,7 @@ tcSimplifyInferCheck doc tau_tvs givens wanted
     complainCheck doc givens irreds            `thenNF_Tc_`
 
        -- Done
-    returnTc (qtvs, frees, binds)
+    returnTc (qtvs, mkLIE frees, binds)
 
 inferCheckLoop doc tau_tvs givens wanteds
   =    -- Step 1
@@ -564,21 +597,20 @@ 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
+                   | otherwise         = ReduceMe 
     in
                -- Step 2
     reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
-           returnTc (varSetElems qtvs, frees, binds, irreds)
+       returnTc (varSetElems qtvs, frees, binds, irreds)
     else
-           inferCheckLoop doc tau_tvs givens wanteds   `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
-           returnTc (qtvs1, frees1 `plusLIE` frees, binds `AndMonoBinds` binds1, irreds1)
+       inferCheckLoop doc tau_tvs givens' (irreds ++ frees)    `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+       returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{tcSimplifyToDicts}
@@ -606,13 +638,31 @@ 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
   = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) ->
        -- Since try_me doesn't look at types, we don't need to 
        -- do any zonking, so it's safe to call reduceContext directly
-    ASSERT( isEmptyLIE frees )
+    ASSERT( null frees )
     returnTc (irreds, binds)
 
   where
@@ -620,8 +670,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}
 
 
@@ -635,28 +685,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 )
-    returnTc (frees, binds)
-    
+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}
 
 
@@ -696,7 +763,7 @@ bindInstsOfLocalFuns init_lie local_ids
   | otherwise
   = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) -> 
     ASSERT( null irreds )
-    returnTc (frees, binds)
+    returnTc (mkLIE frees, binds)
   where
     doc                     = text "bindInsts" <+> ppr local_ids
     wanteds         = lieToList init_lie
@@ -708,7 +775,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}
 
@@ -723,23 +790,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}
 
 
@@ -809,15 +875,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}
 
 
@@ -837,7 +903,7 @@ The "given" set is always empty.
 simpleReduceLoop :: SDoc
                 -> (Inst -> WhatToDo)          -- What to do, *not* based on the quantified type variables
                 -> [Inst]                      -- Wanted
-                -> TcM (LIE,                   -- Free
+                -> TcM ([Inst],                -- Free
                         TcDictBinds,
                         [Inst])                -- Irreducible
 
@@ -847,8 +913,8 @@ simpleReduceLoop doc try_me wanteds
     if no_improvement then
        returnTc (frees, binds, irreds)
     else
-       simpleReduceLoop doc try_me irreds      `thenTc` \ (frees1, binds1, irreds1) ->
-       returnTc (frees `plusLIE` frees1, binds `AndMonoBinds` binds1, irreds1)
+       simpleReduceLoop doc try_me (irreds ++ frees)   `thenTc` \ (frees1, binds1, irreds1) ->
+       returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}     
 
 
@@ -859,7 +925,7 @@ reduceContext :: SDoc
              -> [Inst]                 -- Given
              -> [Inst]                 -- Wanted
              -> NF_TcM (Bool,          -- True <=> improve step did no unification
-                        LIE,           -- Free
+                        [Inst],        -- Free
                         TcDictBinds,   -- Dictionary bindings
                         [Inst])        -- Irreducible
 
@@ -897,12 +963,17 @@ reduceContext doc try_me givens wanteds
      let
        (binds, irreds) = bindsAndIrreds avails wanteds
      in
-     returnTc (no_improvement, mkLIE frees, binds, irreds)
+     returnTc (no_improvement, frees, binds, irreds)
 
 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)
@@ -917,10 +988,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.
@@ -978,17 +1053,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' -> 
@@ -996,9 +1071,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
@@ -1075,41 +1149,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]
@@ -1172,7 +1247,7 @@ It's OK: the final zonking stage should zap y to (), which is fine.
 tcSimplifyTop :: LIE -> TcM TcDictBinds
 tcSimplifyTop wanted_lie
   = simpleReduceLoop (text "tcSimplTop") try_me wanteds        `thenTc` \ (frees, binds, irreds) ->
-    ASSERT( isEmptyLIE frees )
+    ASSERT( null frees )
 
     let
                -- All the non-std ones are definite errors
@@ -1197,12 +1272,16 @@ tcSimplifyTop wanted_lie
     mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
 
        -- And complain about the ones that don't
+       -- This group includes both non-existent instances 
+       --      e.g. Num (IO a) and Eq (Int -> Int)
+       -- and ambiguous dictionaries
+       --      e.g. Num a
     addTopAmbigErrs bad_guys           `thenNF_Tc_`
 
     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
 
@@ -1249,14 +1328,15 @@ 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
-    recoverTc (addAmbigErrs dicts `thenNF_Tc_` returnTc EmptyMonoBinds)        $
+    recoverTc (addAmbigErrs dicts                      `thenNF_Tc_` 
+              returnTc EmptyMonoBinds) $
 
     try_default default_tys                    `thenTc` \ chosen_default_ty ->
 
@@ -1264,7 +1344,7 @@ disambigGroup dicts
     unifyTauTy chosen_default_ty (mkTyVarTy tyvar)     `thenTc_`
     simpleReduceLoop (text "disambig" <+> ppr dicts)
                     try_me dicts                       `thenTc` \ (frees, binds, ambigs) ->
-    WARN( not (isEmptyLIE frees && null ambigs), ppr frees $$ ppr ambigs )
+    WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
     warnDefault dicts chosen_default_ty                        `thenTc_`
     returnTc binds
 
@@ -1279,7 +1359,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}
@@ -1334,8 +1414,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 ->
@@ -1346,10 +1426,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
@@ -1363,8 +1443,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
@@ -1378,23 +1458,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
@@ -1404,32 +1484,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
@@ -1458,9 +1542,10 @@ 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
-              | tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr 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
 
 addTopIPErr tidy_env tidy_dict
@@ -1477,7 +1562,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)
@@ -1489,26 +1574,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
@@ -1544,7 +1617,7 @@ addNoInstanceErr what_doc givens dict
             | 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
@@ -1558,8 +1631,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,