[project @ 2002-05-23 15:51:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 7177347..c28105a 100644 (file)
@@ -11,47 +11,51 @@ module TcSimplify (
        tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
 
-       tcSimplifyThetas, tcSimplifyCheckThetas,
+       tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns
     ) where
 
 #include "HsVersions.h"
 
+import {-# SOURCE #-} TcUnify( unifyTauTy )
+
 import HsSyn           ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
 import TcHsSyn         ( TcExpr, TcId,
                          TcMonoBinds, TcDictBinds
                        )
 
 import TcMonad
-import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
-                         tyVarsOfInst, predsOfInsts, predsOfInst,
-                         isDict, isClassDict, 
-                         isStdClassTyVarDict, isMethodFor,
-                         instToId, tyVarsOfInsts, 
-                         ipNamesOfInsts, ipNamesOfInst,
+import Inst            ( lookupInst, LookupInstResult(..),
+                         tyVarsOfInst, predsOfInsts, predsOfInst, newDicts,
+                         isDict, isClassDict, isLinearInst, linearInstType,
+                         isStdClassTyVarDict, isMethodFor, isMethod,
+                         instToId, tyVarsOfInsts,  cloneDict,
+                         ipNamesOfInsts, ipNamesOfInst, dictPred,
                          instBindingRequired, instCanBeGeneralised,
-                         newDictsFromOld, 
+                         newDictsFromOld, newMethodAtLoc,
                          getDictClassTys, isTyVarDict,
                          instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
                          Inst, LIE, pprInsts, pprInstsInFull,
                          mkLIE, lieToList
                        )
-import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv )
+import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-
-import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
-import TcType          ( ThetaType, PredType, mkClassPred, isOverloadedTy,
-                         mkTyVarTy, tcGetTyVar, isTyVarClassPred,
-                         tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
-                         inheritablePred, predHasFDs )
-import Id              ( idType )
+import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
+import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
+                         mkClassPred, isOverloadedTy, mkTyConApp,
+                         mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
+                         tyVarsOfPred, isIPPred, isInheritablePred, predHasFDs )
+import Id              ( idType, mkUserLocal )
+import Var             ( TyVar )
+import Name            ( getOccName, getSrcLoc )
 import NameSet         ( NameSet, mkNameSet, elemNameSet )
 import Class           ( classBigSig )
 import FunDeps         ( oclose, grow, improve, pprEquationDoc )
-import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass )
+import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass, 
+                         splitName, fstName, sndName )
 
 import Subst           ( mkTopTyVarSubst, substTheta, substTy )
-import TysWiredIn      ( unitTy )
+import TysWiredIn      ( unitTy, pairTyCon )
 import VarSet
 import FiniteMap
 import Outputable
@@ -631,7 +635,7 @@ The net effect of [NO TYVARS]
 isFreeWhenInferring :: TyVarSet -> Inst        -> Bool
 isFreeWhenInferring qtvs inst
   =  isFreeWrtTyVars qtvs inst                 -- Constrains no quantified vars
-  && all inheritablePred (predsOfInst inst)    -- And no implicit parameter involved
+  && all isInheritablePred (predsOfInst inst)  -- And no implicit parameter involved
                                                -- (see "Notes on implicit parameters")
 
 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
@@ -666,9 +670,10 @@ tcSimplifyCheck
 
 -- tcSimplifyCheck is used when checking expression type signatures,
 -- class decls, instance decls etc.
--- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
--- It's important that we can float out non-inheritable predicates
--- Example:            (?x :: Int) is ok!
+--
+-- NB: tcSimplifyCheck does not consult the
+--     global type variables in the environment; so you don't
+--     need to worry about setting them before calling tcSimplifyCheck
 tcSimplifyCheck doc qtvs givens wanted_lie
   = tcSimplCheck doc get_qtvs
                 givens wanted_lie      `thenTc` \ (qtvs', frees, binds) ->
@@ -1016,6 +1021,9 @@ data WhatToDo
 
  | Free                          -- Return as free
 
+reduceMe :: Inst -> WhatToDo
+reduceMe inst = ReduceMe
+
 data WantSCs = NoSCs | AddSCs  -- Tells whether we should add the superclasses
                                -- of a predicate when adding it to the avails
 \end{code}
@@ -1023,17 +1031,16 @@ data WantSCs = NoSCs | AddSCs   -- Tells whether we should add the superclasses
 
 
 \begin{code}
-type RedState = (Avails,       -- What's available
-                [Inst])        -- Insts for which try_me returned Free
-
 type Avails = FiniteMap Inst Avail
 
 data Avail
-  = Irred              -- Used for irreducible dictionaries,
+  = IsFree             -- Used for free Insts
+  | Irred              -- Used for irreducible dictionaries,
                        -- which are going to be lambda bound
 
-  | BoundTo TcId       -- Used for dictionaries for which we have a binding
+  | Given TcId                 -- Used for dictionaries for which we have a binding
                        -- e.g. those "given" in a signature
+         Bool          -- True <=> actually consumed (splittable IPs only)
 
   | NoRhs              -- Used for Insts like (CCallable f)
                        -- where no witness is required.
@@ -1042,16 +1049,31 @@ data Avail
        TcExpr          -- The RHS
        [Inst]          -- Insts free in the RHS; we need these too
 
-pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+  | Linear             -- Splittable Insts only.
+       Int             -- The Int is always 2 or more; indicates how
+                       -- many copies are required
+       Inst            -- The splitter
+       Avail           -- Where the "master copy" is
+
+  | LinRhss            -- Splittable Insts only; this is used only internally
+                       --      by extractResults, where a Linear 
+                       --      is turned into an LinRhss
+       [TcExpr]        -- A supply of suitable RHSs
+
+pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
                        | (inst,avail) <- fmToList avails ]
 
 instance Outputable Avail where
     ppr = pprAvail
 
-pprAvail NoRhs       = text "<no rhs>"
-pprAvail Irred       = text "Irred"
-pprAvail (BoundTo x)  = text "Bound to" <+> ppr x
-pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
+pprAvail NoRhs         = text "<no rhs>"
+pprAvail IsFree                = text "Free"
+pprAvail Irred         = text "Irred"
+pprAvail (Given x b)           = text "Given" <+> ppr x <+> 
+                         if b then text "(used)" else empty
+pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
+pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
 \end{code}
 
 Extracting the bindings from a bunch of Avails.
@@ -1061,41 +1083,135 @@ dependency analyser can sort them out later
 
 The loop startes
 \begin{code}
-bindsAndIrreds :: Avails
+extractResults :: Avails
               -> [Inst]                -- Wanted
-              -> (TcDictBinds,         -- Bindings
-                  [Inst])              -- Irreducible ones
+              -> NF_TcM (TcDictBinds,  -- Bindings
+                         [Inst],       -- Irreducible ones
+                         [Inst])       -- Free ones
 
-bindsAndIrreds avails wanteds
-  = go avails EmptyMonoBinds [] wanteds
+extractResults avails wanteds
+  = go avails EmptyMonoBinds [] [] wanteds
   where
-    go avails binds irreds [] = (binds, irreds)
+    go avails binds irreds frees [] 
+      = returnNF_Tc (binds, irreds, frees)
 
-    go avails binds irreds (w:ws)
+    go avails binds irreds frees (w:ws)
       = case lookupFM avails w of
-         Nothing    -> -- Free guys come out here
-                       -- (If we didn't do addFree we could use this as the
-                       --  criterion for free-ness, and pick up the free ones here too)
-                       go avails binds irreds ws
+         Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
+                       go avails binds irreds frees ws
 
-         Just NoRhs -> go avails binds irreds ws
+         Just NoRhs  -> go avails               binds irreds     frees     ws
+         Just IsFree -> go (add_free avails w)  binds irreds     (w:frees) ws
+         Just Irred  -> go (add_given avails w) binds (w:irreds) frees     ws
 
-         Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
-
-         Just (BoundTo id) -> go avails new_binds irreds ws
+         Just (Given id _) -> go avails new_binds irreds frees ws
                            where
-                               -- For implicit parameters, all occurrences share the same
-                               -- Id, so there is no need for synonym bindings
-                              new_binds | new_id == id = binds
-                                        | otherwise    = addBind binds new_id (HsVar id)
-                              new_id   = instToId w
+                              new_binds | id == instToId w = binds
+                                        | otherwise        = addBind binds w (HsVar id)
+               -- The sought Id can be one of the givens, via a superclass chain
+               -- and then we definitely don't want to generate an x=x binding!
 
-         Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
+         Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
                             where
-                               id       = instToId w
-                               avails'  = addToFM avails w (BoundTo id)
-
-addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
+                               new_binds = addBind binds w rhs
+
+         Just (Linear n split_inst avail)      -- Transform Linear --> LinRhss
+           -> get_root irreds frees avail w            `thenNF_Tc` \ (irreds', frees', root_id) ->
+              split n (instToId split_inst) root_id w  `thenNF_Tc` \ (binds', rhss) ->
+              go (addToFM avails w (LinRhss rhss))
+                 (binds `AndMonoBinds` binds')
+                 irreds' frees' (split_inst : w : ws)
+
+         Just (LinRhss (rhs:rhss))             -- Consume one of the Rhss
+               -> go new_avails new_binds irreds frees ws
+               where           
+                  new_binds  = addBind binds w rhs
+                  new_avails = addToFM avails w (LinRhss rhss)
+
+    get_root irreds frees (Given id _) w = returnNF_Tc (irreds, frees, id)
+    get_root irreds frees Irred               w = cloneDict w  `thenNF_Tc` \ w' ->
+                                          returnNF_Tc (w':irreds, frees, instToId w')
+    get_root irreds frees IsFree       w = cloneDict w `thenNF_Tc` \ w' ->
+                                          returnNF_Tc (irreds, w':frees, instToId w')
+
+    add_given avails w 
+       | instBindingRequired w = addToFM avails w (Given (instToId w) True)
+       | otherwise             = addToFM avails w NoRhs
+       -- NB: make sure that CCallable/CReturnable use NoRhs rather
+       --      than Given, else we end up with bogus bindings.
+
+    add_free avails w | isMethod w = avails
+                     | otherwise  = add_given avails w
+       -- NB: Hack alert!  
+       -- Do *not* replace Free by Given if it's a method.
+       -- The following situation shows why this is bad:
+       --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
+       -- From an application (truncate f i) we get
+       --      t1 = truncate at f
+       --      t2 = t1 at i
+       -- If we have also have a second occurrence of truncate, we get
+       --      t3 = truncate at f
+       --      t4 = t3 at i
+       -- When simplifying with i,f free, we might still notice that
+       --   t1=t3; but alas, the binding for t2 (which mentions t1)
+       --   will continue to float out!
+       -- (split n i a) returns: n rhss
+       --                        auxiliary bindings
+       --                        1 or 0 insts to add to irreds
+
+
+split :: Int -> TcId -> TcId -> Inst 
+      -> NF_TcM (TcDictBinds, [TcExpr])
+-- (split n split_id root_id wanted) returns
+--     * a list of 'n' expressions, all of which witness 'avail'
+--     * a bunch of auxiliary bindings to support these expressions
+--     * one or zero insts needed to witness the whole lot
+--       (maybe be zero if the initial Inst is a Given)
+--
+-- NB: 'wanted' is just a template
+
+split n split_id root_id wanted
+  = go n
+  where
+    ty      = linearInstType wanted
+    pair_ty = mkTyConApp pairTyCon [ty,ty]
+    id      = instToId wanted
+    occ     = getOccName id
+    loc     = getSrcLoc id
+
+    go 1 = returnNF_Tc (EmptyMonoBinds, [HsVar root_id])
+
+    go n = go ((n+1) `div` 2)          `thenNF_Tc` \ (binds1, rhss) ->
+          expand n rhss                `thenNF_Tc` \ (binds2, rhss') ->
+          returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss')
+
+       -- (expand n rhss) 
+       -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
+       --  e.g.  expand 3 [rhs1, rhs2]
+       --        = ( { x = split rhs1 },
+       --            [fst x, snd x, rhs2] )
+    expand n rhss
+       | n `rem` 2 == 0 = go rhss      -- n is even
+       | otherwise      = go (tail rhss)       `thenNF_Tc` \ (binds', rhss') ->
+                          returnNF_Tc (binds', head rhss : rhss')
+       where
+         go rhss = mapAndUnzipNF_Tc do_one rhss        `thenNF_Tc` \ (binds', rhss') ->
+                   returnNF_Tc (andMonoBindList binds', concat rhss')
+
+         do_one rhs = tcGetUnique                      `thenNF_Tc` \ uniq -> 
+                      tcLookupGlobalId fstName         `thenNF_Tc` \ fst_id ->
+                      tcLookupGlobalId sndName         `thenNF_Tc` \ snd_id ->
+                      let 
+                         x = mkUserLocal occ uniq pair_ty loc
+                      in
+                      returnNF_Tc (VarMonoBind x (mk_app split_id rhs),
+                                   [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
+
+mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
+
+mk_app id rhs = HsApp (HsVar id) rhs
+
+addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
 \end{code}
 
 
@@ -1152,15 +1268,17 @@ reduceContext doc try_me givens wanteds
             ]))                                        `thenNF_Tc_`
 
         -- Build the Avail mapping from "givens"
-    foldlNF_Tc addGiven (emptyFM, []) givens           `thenNF_Tc` \ init_state ->
+    foldlNF_Tc addGiven emptyFM givens                 `thenNF_Tc` \ init_state ->
 
         -- Do the real work
-    reduceList (0,[]) try_me wanteds init_state                `thenNF_Tc` \ state@(avails, frees) ->
+    reduceList (0,[]) try_me wanteds init_state                `thenNF_Tc` \ avails ->
 
        -- Do improvement, using everything in avails
        -- In particular, avails includes all superclasses of everything
     tcImprove avails                                   `thenTc` \ no_improvement ->
 
+    extractResults avails wanteds                      `thenNF_Tc` \ (binds, irreds, frees) ->
+
     traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             doc,
@@ -1172,10 +1290,8 @@ reduceContext doc try_me givens wanteds
             text "no_improvement =" <+> ppr no_improvement,
             text "----------------------"
             ]))                                        `thenNF_Tc_`
-     let
-       (binds, irreds) = bindsAndIrreds avails wanteds
-     in
-     returnTc (no_improvement, frees, binds, irreds)
+
+    returnTc (no_improvement, frees, binds, irreds)
 
 tcImprove avails
  =  tcGetInstEnv                               `thenTc` \ inst_env ->
@@ -1201,8 +1317,8 @@ tcImprove avails
        returnTc False
   where
     unify ((qtvs, t1, t2), doc)
-        = tcAddErrCtxt doc                     $
-          tcInstTyVars (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
+        = tcAddErrCtxt doc                             $
+          tcInstTyVars VanillaTv (varSetElems qtvs)    `thenNF_Tc` \ (_, _, tenv) ->
           unifyTauTy (substTy tenv t1) (substTy tenv t2)
 \end{code}
 
@@ -1213,8 +1329,8 @@ reduceList :: (Int,[Inst])                -- Stack (for err msgs)
                                        -- along with its depth
                   -> (Inst -> WhatToDo)
                   -> [Inst]
-                  -> RedState
-                  -> TcM RedState
+                  -> Avails
+                  -> TcM Avails
 \end{code}
 
 @reduce@ is passed
@@ -1224,10 +1340,10 @@ reduceList :: (Int,[Inst])              -- Stack (for err msgs)
                  Free         return this in "frees"
 
      wanteds:  The list of insts to reduce
-     state:    An accumulating parameter of type RedState
+     state:    An accumulating parameter of type Avails
                that contains the state of the algorithm
 
-  It returns a RedState.
+  It returns a Avails.
 
 The (n,stack) pair is just used for error reporting.
 n is always the depth of the stack.
@@ -1255,8 +1371,12 @@ reduceList (n,stack) try_me wanteds state
     -- Base case: we're done!
 reduce stack try_me wanted state
     -- It's the same as an existing inst, or a superclass thereof
-  | isAvailable state wanted
-  = returnTc state
+  | Just avail <- isAvailable state wanted
+  = if isLinearInst wanted then
+       addLinearAvailable state avail wanted   `thenNF_Tc` \ (state', wanteds') ->
+       reduceList stack try_me wanteds' state'
+    else
+       returnTc state          -- No op for non-linear things
 
   | otherwise
   = case try_me wanted of {
@@ -1293,95 +1413,102 @@ reduce stack try_me wanted state
 
 
 \begin{code}
-isAvailable :: RedState -> Inst -> Bool
-isAvailable (avails, _) wanted = wanted `elemFM` avails
-       -- NB: the Ord instance of Inst compares by the class/type info
+-------------------------
+isAvailable :: Avails -> Inst -> Maybe Avail
+isAvailable avails wanted = lookupFM avails wanted
+       -- NB 1: the Ord instance of Inst compares by the class/type info
        -- *not* by unique.  So
        --      d1::C Int ==  d2::C Int
 
+addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
+addLinearAvailable avails avail wanted
+       -- avails currently maps [wanted -> avail]
+       -- Extend avails to reflect a neeed for an extra copy of avail
+
+  | Just avail' <- split_avail avail
+  = returnNF_Tc (addToFM avails wanted avail', [])
+
+  | otherwise
+  = tcLookupGlobalId splitName                 `thenNF_Tc` \ split_id ->
+    newMethodAtLoc (instLoc wanted) split_id 
+                  [linearInstType wanted]      `thenNF_Tc` \ (split_inst,_) ->
+    returnNF_Tc (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
+
+  where
+    split_avail :: Avail -> Maybe Avail
+       -- (Just av) if there's a modified version of avail that
+       --           we can use to replace avail in avails
+       -- Nothing   if there isn't, so we need to create a Linear
+    split_avail (Linear n i a)             = Just (Linear (n+1) i a)
+    split_avail (Given id used) | not used  = Just (Given id True)
+                               | otherwise = Nothing
+    split_avail Irred                      = Nothing
+    split_avail IsFree                     = Nothing
+    split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
+                 
 -------------------------
-addFree :: RedState -> Inst -> NF_TcM RedState
+addFree :: Avails -> Inst -> NF_TcM Avails
        -- When an Inst is tossed upstairs as 'free' we nevertheless add it
        -- to avails, so that any other equal Insts will be commoned up right
        -- here rather than also being tossed upstairs.  This is really just
        -- an optimisation, and perhaps it is more trouble that it is worth,
        -- as the following comments show!
        --
-       -- NB1: do *not* add superclasses.  If we have
+       -- NB: do *not* add superclasses.  If we have
        --      df::Floating a
        --      dn::Num a
        -- but a is not bound here, then we *don't* want to derive
        -- dn from df here lest we lose sharing.
        --
-       -- NB2: do *not* add the Inst to avails at all if it's a method.
-       -- The following situation shows why this is bad:
-       --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
-       -- From an application (truncate f i) we get
-       --      t1 = truncate at f
-       --      t2 = t1 at i
-       -- If we have also have a second occurrence of truncate, we get
-       --      t3 = truncate at f
-       --      t4 = t3 at i
-       -- When simplifying with i,f free, we might still notice that
-       --   t1=t3; but alas, the binding for t2 (which mentions t1)
-       --   will continue to float out!
-       -- Solution: never put methods in avail till they are captured
-       -- in which case addFree isn't used
-       --
-       -- NB3: make sure that CCallable/CReturnable use NoRhs rather
-       --      than BoundTo, else we end up with bogus bindings.
-       --      c.f. instBindingRequired in addWanted
-addFree (avails, frees) free
-  | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
-  | otherwise   = returnNF_Tc (avails,                   free:frees)
-  where
-    avail | instBindingRequired free = BoundTo (instToId free)
-         | otherwise                = NoRhs
-
-addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
-addWanted state@(avails, frees) wanted rhs_expr wanteds
--- Do *not* add superclasses as well.  Here's an example of why not
---     class Eq a => Foo a b
---     instance Eq a => Foo [a] a
--- If we are reducing
---     (Foo [t] t)
--- we'll first deduce that it holds (via the instance decl).  We
--- must not then overwrite the Eq t constraint with a superclass selection!
---     ToDo: this isn't entirely unsatisfactory, because
---           we may also lose some entirely-legitimate sharing this way
-
-  = ASSERT( not (isAvailable state wanted) )
-    returnNF_Tc (addToFM avails wanted avail, frees)
+addFree avails free = returnNF_Tc (addToFM avails free IsFree)
+
+addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
+addWanted avails wanted rhs_expr wanteds
+  = ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
+    addAvailAndSCs avails wanted avail
   where
     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
          | otherwise                  = ASSERT( null wanteds ) NoRhs
 
-addGiven :: RedState -> Inst -> NF_TcM RedState
-addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
-
-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
-
-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)
-
----------------------
-add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
-add_avail_and_scs avails wanted avail
-  = add_scs (addToFM avails wanted avail) wanted
-
-add_scs :: Avails -> Inst -> NF_TcM Avails
+addGiven :: Avails -> Inst -> NF_TcM Avails
+addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
+       -- No ASSERT( not (given `elemFM` avails) ) because in an instance
+       -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
+       -- so the assert isn't true
+
+addIrred :: WantSCs -> Avails -> Inst -> NF_TcM Avails
+addIrred NoSCs  avails irred = returnNF_Tc (addToFM avails irred Irred)
+addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
+                              addAvailAndSCs avails irred Irred
+
+addAvailAndSCs :: Avails -> Inst -> Avail -> NF_TcM Avails
+addAvailAndSCs avails inst avail
+  | not (isClassDict inst) = returnNF_Tc avails1
+  | otherwise             = addSCs is_loop avails1 inst 
+  where
+    avails1 = addToFM avails inst avail
+    is_loop inst = inst `elem` deps    -- Note: this compares by *type*, not by Unique
+    deps         = findAllDeps avails avail
+
+findAllDeps :: Avails -> Avail -> [Inst]
+-- Find all the Insts that this one depends on
+-- See Note [SUPERCLASS-LOOP]
+findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
+findAllDeps avails other       = []
+
+find_all_deps_help :: Avails -> Inst -> [Inst]
+find_all_deps_help avails inst
+  = case lookupFM avails inst of
+       Just avail -> findAllDeps avails avail
+       Nothing    -> []
+
+addSCs :: (Inst -> Bool) -> Avails -> Inst -> NF_TcM Avails
        -- Add all the superclasses of the Inst to Avails
+       -- The first param says "dont do this because the original thing
+       --      depends on this one, so you'd build a loop"
        -- Invariant: the Inst is already in Avails.
 
-add_scs avails dict
-  | not (isClassDict dict)
-  = returnNF_Tc avails
-
-  | otherwise  -- It is a dictionary
+addSCs is_loop avails dict
   = newDictsFromOld dict sc_theta'     `thenNF_Tc` \ sc_dicts ->
     foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
   where
@@ -1391,14 +1518,21 @@ add_scs avails dict
 
     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            -> add_avail_and_scs avails sc_dict avail
+         Just (Given _ _) -> returnNF_Tc avails        -- Given is cheaper than
+                                                       --   a superclass selection
+         Just other | is_loop sc_dict -> returnNF_Tc avails    -- See Note [SUPERCLASS-LOOP]
+                    | otherwise       -> returnNF_Tc avails'   -- SCs already added
+
+         Nothing -> addSCs is_loop avails' sc_dict
       where
        sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
        avail      = Rhs sc_sel_rhs [dict]
+       avails'    = addToFM avails sc_dict avail
 \end{code}
 
-Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
+Note [SUPERCLASS-LOOP]: Checking for loops
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have to be careful here.  If we are *given* d1:Ord a,
 and want to deduce (d2:C [a]) where
 
        class Ord a => C a where
@@ -1407,8 +1541,27 @@ and want to deduce (d2:C [a]) where
 Then we'll use the instance decl to deduce C [a] and then add the
 superclasses of C [a] to avails.  But we must not overwrite the binding
 for d1:Ord a (which is given) with a superclass selection or we'll just
-build a loop!  Hence looking for BoundTo.  Crudely, BoundTo is cheaper
-than a selection.
+build a loop! 
+
+Here's another example 
+       class Eq b => Foo a b
+       instance Eq a => Foo [a] a
+If we are reducing
+       (Foo [t] t)
+
+we'll first deduce that it holds (via the instance decl).  We must not
+then overwrite the Eq t constraint with a superclass selection!
+
+At first I had a gross hack, whereby I simply did not add superclass constraints
+in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
+becuase it lost legitimate superclass sharing, and it still didn't do the job:
+I found a very obscure program (now tcrun021) in which improvement meant the
+simplifier got two bites a the cherry... so something seemed to be an Irred
+first time, but reducible next time.
+
+Now we implement the Right Solution, which is to check for loops directly 
+when adding superclasses.  It's a bit like the occurs check in unification.
+
 
 
 %************************************************************************
@@ -1418,26 +1571,6 @@ than a selection.
 %************************************************************************
 
 
-If a dictionary constrains a type variable which is
-       * not mentioned in the environment
-       * and not mentioned in the type of the expression
-then it is ambiguous. No further information will arise to instantiate
-the type variable; nor will it be generalised and turned into an extra
-parameter to a function.
-
-It is an error for this to occur, except that Haskell provided for
-certain rules to be applied in the special case of numeric types.
-Specifically, if
-       * at least one of its classes is a numeric class, and
-       * all of its classes are numeric or standard
-then the type variable can be defaulted to the first type in the
-default-type list which is an instance of all the offending classes.
-
-So here is the function which does the work.  It takes the ambiguous
-dictionaries and either resolves them (producing bindings) or
-complains.  It works by splitting the dictionary list by type
-variable, and using @disambigOne@ to do the real business.
-
 @tcSimplifyTop@ is called once per module to simplify all the constant
 and ambiguous Insts.
 
@@ -1454,7 +1587,7 @@ It's OK: the final zonking stage should zap y to (), which is fine.
 \begin{code}
 tcSimplifyTop :: LIE -> TcM TcDictBinds
 tcSimplifyTop wanted_lie
-  = simpleReduceLoop (text "tcSimplTop") try_me wanteds        `thenTc` \ (frees, binds, irreds) ->
+  = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds      `thenTc` \ (frees, binds, irreds) ->
     ASSERT( null frees )
 
     let
@@ -1476,20 +1609,29 @@ tcSimplifyTop wanted_lie
                -- Collect together all the bad guys
        bad_guys = non_stds ++ concat std_bads
     in
-       -- Disambiguate the ones that look feasible
-    mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
 
-       -- And complain about the ones that don't
+    ifErrsTc (returnTc []) (
+       -- Don't check for ambiguous things
+       -- if there has been an error; errors often
+       -- give rise to spurious ambiguous Insts
+       
+    
+       -- And complain about the ones that don't fall under
+       -- the Haskell rules for disambiguation
        -- This group includes both non-existent instances
        --      e.g. Num (IO a) and Eq (Int -> Int)
        -- and ambiguous dictionaries
        --      e.g. Num a
-    addTopAmbigErrs bad_guys           `thenNF_Tc_`
+        addTopAmbigErrs bad_guys       `thenNF_Tc_`
+
+       -- Disambiguate the ones that look feasible
+        mapTc disambigGroup std_oks
+    )                                  `thenTc` \ binds_ambig ->
+
 
     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
   where
     wanteds    = lieToList wanted_lie
-    try_me inst        = ReduceMe
 
     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
@@ -1499,6 +1641,26 @@ get_clas d = case getDictClassTys d of
                   (clas, [ty]) -> clas
 \end{code}
 
+If a dictionary constrains a type variable which is
+       * not mentioned in the environment
+       * and not mentioned in the type of the expression
+then it is ambiguous. No further information will arise to instantiate
+the type variable; nor will it be generalised and turned into an extra
+parameter to a function.
+
+It is an error for this to occur, except that Haskell provided for
+certain rules to be applied in the special case of numeric types.
+Specifically, if
+       * at least one of its classes is a numeric class, and
+       * all of its classes are numeric or standard
+then the type variable can be defaulted to the first type in the
+default-type list which is an instance of all the offending classes.
+
+So here is the function which does the work.  It takes the ambiguous
+dictionaries and either resolves them (producing bindings) or
+complains.  It works by splitting the dictionary list by type
+variable, and using @disambigOne@ to do the real business.
+
 @disambigOne@ assumes that its arguments dictionaries constrain all
 the same type variable.
 
@@ -1536,7 +1698,7 @@ disambigGroup dicts
       try_default (default_ty : default_tys)
        = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
                                                -- default_tys instead
-         tcSimplifyCheckThetas [] theta        `thenTc` \ _ ->
+         tcSimplifyDefault theta               `thenTc` \ _ ->
          returnTc default_ty
         where
          theta = [mkClassPred clas [default_ty] | clas <- classes]
@@ -1551,7 +1713,7 @@ disambigGroup dicts
        -- Bind the type variable and reduce the context, for real this time
     unifyTauTy chosen_default_ty (mkTyVarTy tyvar)     `thenTc_`
     simpleReduceLoop (text "disambig" <+> ppr dicts)
-                    try_me dicts                       `thenTc` \ (frees, binds, ambigs) ->
+                    reduceMe dicts                     `thenTc` \ (frees, binds, ambigs) ->
     WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
     warnDefault dicts chosen_default_ty                        `thenTc_`
     returnTc binds
@@ -1567,7 +1729,6 @@ disambigGroup dicts
     returnTc EmptyMonoBinds
 
   where
-    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}
@@ -1622,116 +1783,83 @@ a,b,c are type variables.  This is required for the context of
 instance declarations.
 
 \begin{code}
-tcSimplifyThetas :: ThetaType          -- Wanted
-                -> TcM ThetaType               -- Needed
-
-tcSimplifyThetas wanteds
-  = doptsTc Opt_GlasgowExts            `thenNF_Tc` \ glaExts ->
-    reduceSimple [] wanteds            `thenNF_Tc` \ irreds ->
+tcSimplifyDeriv :: [TyVar]     
+               -> ThetaType            -- Wanted
+               -> TcM ThetaType        -- Needed
+
+tcSimplifyDeriv tyvars theta
+  = tcInstTyVars VanillaTv tyvars                      `thenNF_Tc` \ (tvs, _, tenv) ->
+       -- The main loop may do unification, and that may crash if 
+       -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
+       -- ToDo: what if two of them do get unified?
+    newDicts DataDeclOrigin (substTheta tenv theta)    `thenNF_Tc` \ wanteds ->
+    simpleReduceLoop doc reduceMe wanteds              `thenTc` \ (frees, _, irreds) ->
+    ASSERT( null frees )                       -- reduceMe never returns Free
+
+    doptsTc Opt_AllowUndecidableInstances              `thenNF_Tc` \ undecidable_ok ->
     let
-       -- For multi-param Haskell, check that the returned dictionaries
-       -- don't have any of the form (C Int Bool) for which
-       -- 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   = [pred | pred <- irreds,
-                                      isEmptyVarSet (tyVarsOfPred pred)]
-                | otherwise = [pred | pred <- irreds,
-                                      not (isTyVarClassPred pred)]
+       tv_set      = mkVarSet tvs
+       simpl_theta = map dictPred irreds       -- reduceMe squashes all non-dicts
+
+       check_pred pred
+         | isEmptyVarSet pred_tyvars   -- Things like (Eq T) should be rejected
+         = addErrTc (noInstErr pred)
+
+         | not undecidable_ok && not (isTyVarClassPred pred)
+         -- Check that the returned dictionaries are all of form (C a b)
+         --    (where a, b are type variables).  
+         -- We allow this if we had -fallow-undecidable-instances,
+         -- but note that risks non-termination in the 'deriving' context-inference
+         -- fixpoint loop.   It is useful for situations like
+         --    data Min h a = E | M a (h a)
+         -- which gives the instance decl
+         --    instance (Eq a, Eq (h a)) => Eq (Min h a)
+          = addErrTc (noInstErr pred)
+  
+         | not (pred_tyvars `subVarSet` tv_set) 
+         -- Check for a bizarre corner case, when the derived instance decl should
+         -- have form  instance C a b => D (T a) where ...
+         -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
+         -- of problems; in particular, it's hard to compare solutions for
+         -- equality when finding the fixpoint.  So I just rule it out for now.
+         = addErrTc (badDerivedPred pred)
+  
+         | otherwise
+         = returnNF_Tc ()
+         where
+           pred_tyvars = tyVarsOfPred pred
+
+       rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
+               -- This reverse-mapping is a Royal Pain, 
+               -- but the result should mention TyVars not TcTyVars
     in
-    if null bad_guys then
-       returnTc irreds
-    else
-       mapNF_Tc addNoInstErr bad_guys          `thenNF_Tc_`
-       failTc
+   
+    mapNF_Tc check_pred simpl_theta            `thenNF_Tc_`
+    checkAmbiguity tvs simpl_theta tv_set      `thenTc_`
+    returnTc (substTheta rev_env simpl_theta)
+  where
+    doc    = ptext SLIT("deriving classes for a data type")
 \end{code}
 
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+@tcSimplifyDefault@ just checks class-type constraints, essentially;
 used with \tr{default} declarations.  We are only interested in
 whether it worked or not.
 
 \begin{code}
-tcSimplifyCheckThetas :: ThetaType     -- Given
-                     -> ThetaType      -- Wanted
-                     -> TcM ()
-
-tcSimplifyCheckThetas givens wanteds
-  = reduceSimple givens wanteds    `thenNF_Tc` \ irreds ->
+tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
+                 -> TcM ()
+
+tcSimplifyDefault theta
+  = newDicts DataDeclOrigin theta              `thenNF_Tc` \ wanteds ->
+    simpleReduceLoop doc reduceMe wanteds      `thenTc` \ (frees, _, irreds) ->
+    ASSERT( null frees )       -- try_me never returns Free
+    mapNF_Tc (addErrTc . noInstErr) irreds     `thenNF_Tc_`
     if null irreds then
-       returnTc ()
+       returnTc ()
     else
-       mapNF_Tc addNoInstErr irreds            `thenNF_Tc_`
-       failTc
-\end{code}
-
-
-\begin{code}
-type AvailsSimple = FiniteMap PredType Bool
-                   -- True  => irreducible
-                   -- False => given, or can be derived from a given or from an 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 [pred | (pred,True) <- fmToList givens_fm']
+       failTc
   where
-    givens_fm     = foldl addNonIrred emptyFM givens
-
-reduce_simple :: (Int,ThetaType)               -- Stack
-             -> AvailsSimple
-             -> ThetaType
-             -> NF_TcM AvailsSimple
-
-reduce_simple (n,stack) avails wanteds
-  = go avails wanteds
-  where
-    go avails []     = returnNF_Tc avails
-    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
-  | wanted `elemFM` givens
-  = returnNF_Tc givens
-
-  | 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
-
-  | otherwise
-  = returnNF_Tc (addSimpleIrred givens wanted)
-
-addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
-addSimpleIrred givens pred
-  = addSCs (addToFM givens pred True) pred
-
-addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
-addNonIrred givens pred
-  = addSCs (addToFM givens pred False) pred
-
-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 = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
-
-   add givens ct
-     = case lookupFM givens ct of
-       Nothing    -> -- Add it and its superclasses
-                    addSCs (addToFM givens ct False) ct
-
-       Just True  -> -- Set its flag to False; superclasses already done
-                    addToFM givens ct False
-
-       Just False -> -- Already done
-                    givens
-
+    doc = ptext SLIT("default declaration")
 \end{code}
 
 
@@ -1813,16 +1941,17 @@ warnDefault dicts default_ty
                      pprInstsInFull tidy_dicts]
 
 complainCheck doc givens irreds
-  = mapNF_Tc zonkInst given_dicts                                `thenNF_Tc` \ givens' ->
+  = mapNF_Tc zonkInst given_dicts_and_ips                        `thenNF_Tc` \ givens' ->
     mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds)  `thenNF_Tc_`
     returnNF_Tc ()
   where
-    given_dicts = filter isDict givens
+    given_dicts_and_ips = filter (not . isMethod) givens
        -- Filter out methods, which are only added to
        -- the given set as an optimisation
 
 addNoInstanceErrs what_doc givens dicts
-  = tcGetInstEnv       `thenNF_Tc` \ inst_env ->
+  = getDOptsTc         `thenNF_Tc` \ dflags ->
+    tcGetInstEnv       `thenNF_Tc` \ inst_env ->
     let
        (tidy_env1, tidy_givens) = tidyInsts givens
        (tidy_env2, tidy_dicts)  = tidyMoreInsts tidy_env1 dicts
@@ -1867,7 +1996,7 @@ addNoInstanceErrs what_doc givens dicts
        ambig_overlap = any ambig_overlap1 dicts
        ambig_overlap1 dict 
                | isClassDict dict
-               = case lookupInstEnv inst_env clas tys of
+               = case lookupInstEnv dflags inst_env clas tys of
                            NoMatch ambig -> ambig
                            other         -> False
                | otherwise = False
@@ -1877,8 +2006,12 @@ addNoInstanceErrs what_doc givens dicts
     addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
 
 -- Used for the ...Thetas variants; all top level
-addNoInstErr pred
-  = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
+noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
+
+badDerivedPred pred
+  = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
+         ptext SLIT("type variables that are not data type parameters"),
+         nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
 
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,