[project @ 2002-05-23 15:51:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 8af9924..c28105a 100644 (file)
@@ -11,7 +11,7 @@ module TcSimplify (
        tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
 
-       tcSimplifyThetas, tcSimplifyCheckThetas,
+       tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns
     ) where
 
@@ -25,12 +25,12 @@ import TcHsSyn              ( TcExpr, TcId,
                        )
 
 import TcMonad
-import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
-                         tyVarsOfInst, predsOfInsts, predsOfInst,
+import Inst            ( lookupInst, LookupInstResult(..),
+                         tyVarsOfInst, predsOfInsts, predsOfInst, newDicts,
                          isDict, isClassDict, isLinearInst, linearInstType,
                          isStdClassTyVarDict, isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
-                         ipNamesOfInsts, ipNamesOfInst,
+                         ipNamesOfInsts, ipNamesOfInst, dictPred,
                          instBindingRequired, instCanBeGeneralised,
                          newDictsFromOld, newMethodAtLoc,
                          getDictClassTys, isTyVarDict,
@@ -40,19 +40,19 @@ import Inst         ( lookupInst, lookupSimpleInst, LookupInstResult(..),
                        )
 import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars )
-import TcType          ( TcTyVar, TcTyVarSet, ThetaType, PredType, 
+import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
+import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
                          mkClassPred, isOverloadedTy, mkTyConApp,
-                         mkTyVarTy, tcGetTyVar, isTyVarClassPred,
-                         tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
-                         inheritablePred, predHasFDs )
+                         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, 
-                         splitIdName, fstIdName, sndIdName )
+                         splitName, fstName, sndName )
 
 import Subst           ( mkTopTyVarSubst, substTheta, substTy )
 import TysWiredIn      ( unitTy, pairTyCon )
@@ -635,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
@@ -670,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) ->
@@ -1020,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}
@@ -1056,7 +1060,7 @@ data Avail
                        --      is turned into an LinRhss
        [TcExpr]        -- A supply of suitable RHSs
 
-pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
                        | (inst,avail) <- fmToList avails ]
 
 instance Outputable Avail where
@@ -1111,18 +1115,24 @@ extractResults avails wanteds
                             where
                                new_binds = addBind binds w rhs
 
-         Just (LinRhss (rhs:rhss))     -- Consume one of the Rhss
+         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)
 
-         Just (Linear n split_inst avail)
-           -> split n (instToId split_inst) avail w    `thenNF_Tc` \ (binds', (rhs:rhss), irreds') ->
-              go (addToFM avails w (LinRhss rhss))
-                 (binds `AndMonoBinds` addBind binds' w rhs)
-                 (irreds' ++ irreds) frees (split_inst:ws)
-
+    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)
@@ -1150,30 +1160,30 @@ extractResults avails wanteds
        --                        1 or 0 insts to add to irreds
 
 
-split :: Int -> TcId -> Avail -> Inst 
-      -> NF_TcM (TcDictBinds, [TcExpr], [Inst])
--- (split n split_id avail wanted) returns
+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)
-split n split_id avail wanted
+--
+-- NB: 'wanted' is just a template
+
+split n split_id root_id wanted
   = go n
   where
-    ty  = linearInstType wanted
+    ty      = linearInstType wanted
     pair_ty = mkTyConApp pairTyCon [ty,ty]
-    id  = instToId wanted
-    occ = getOccName id
-    loc = getSrcLoc id
+    id      = instToId wanted
+    occ     = getOccName id
+    loc     = getSrcLoc id
 
-    go 1 = case avail of
-            Given id _ -> returnNF_Tc (EmptyMonoBinds, [HsVar id], [])
-            Irred      -> cloneDict wanted             `thenNF_Tc` \ w' ->
-                          returnNF_Tc (EmptyMonoBinds, [HsVar (instToId w')], [w'])
+    go 1 = returnNF_Tc (EmptyMonoBinds, [HsVar root_id])
 
-    go n = go ((n+1) `div` 2)          `thenNF_Tc` \ (binds1, rhss, irred) ->
+    go n = go ((n+1) `div` 2)          `thenNF_Tc` \ (binds1, rhss) ->
           expand n rhss                `thenNF_Tc` \ (binds2, rhss') ->
-          returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss', irred)
+          returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss')
 
        -- (expand n rhss) 
        -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
@@ -1189,8 +1199,8 @@ split n split_id avail wanted
                    returnNF_Tc (andMonoBindList binds', concat rhss')
 
          do_one rhs = tcGetUnique                      `thenNF_Tc` \ uniq -> 
-                      tcLookupGlobalId fstIdName       `thenNF_Tc` \ fst_id -> 
-                      tcLookupGlobalId sndIdName       `thenNF_Tc` \ snd_id -> 
+                      tcLookupGlobalId fstName         `thenNF_Tc` \ fst_id ->
+                      tcLookupGlobalId sndName         `thenNF_Tc` \ snd_id ->
                       let 
                          x = mkUserLocal occ uniq pair_ty loc
                       in
@@ -1307,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}
 
@@ -1412,23 +1422,30 @@ isAvailable avails wanted = lookupFM avails wanted
 
 addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
 addLinearAvailable avails avail wanted
-  | need_split avail
-  = tcLookupGlobalId splitIdName               `thenNF_Tc` \ split_id ->
+       -- 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])
 
-  | otherwise
-  = returnNF_Tc (addToFM avails wanted avail', [])
   where
-    avail' = case avail of
-               Given id _   -> Given id True
-               Linear n i a -> Linear (n+1) i a 
-
-    need_split Irred         = True
-    need_split (Given _ used) = used
-    need_split (Linear _ _ _) = False
-
+    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 :: Avails -> Inst -> NF_TcM Avails
        -- When an Inst is tossed upstairs as 'free' we nevertheless add it
@@ -1437,7 +1454,7 @@ addFree :: Avails -> Inst -> NF_TcM Avails
        -- 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
@@ -1447,42 +1464,51 @@ addFree avails free = returnNF_Tc (addToFM avails free IsFree)
 
 addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
 addWanted avails 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 (wanted `elemFM` avails) )
-    returnNF_Tc (addToFM avails wanted avail)
+  = 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 :: 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  state irred = returnNF_Tc (addToFM state irred Irred)
-addIrred AddSCs state irred = addAvailAndSCs state irred Irred
+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 wanted avail
-  = add_scs (addToFM avails wanted avail) wanted
-
-add_scs :: Avails -> Inst -> 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
@@ -1492,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 (Given _ _) -> returnNF_Tc avails        -- See Note [SUPER] below
-         other            -> addAvailAndSCs 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
@@ -1508,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 Given.  Crudely, Given 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.
+
 
 
 %************************************************************************
@@ -1519,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.
 
@@ -1555,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
@@ -1577,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
 
@@ -1600,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.
 
@@ -1637,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]
@@ -1652,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
@@ -1668,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}
@@ -1723,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']
-  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
+       failTc
   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}
 
 
@@ -1923,7 +1950,8 @@ complainCheck doc givens irreds
        -- 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
@@ -1968,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
@@ -1978,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,