[project @ 2001-12-28 17:25:31 by simonpj]
authorsimonpj <unknown>
Fri, 28 Dec 2001 17:25:32 +0000 (17:25 +0000)
committersimonpj <unknown>
Fri, 28 Dec 2001 17:25:32 +0000 (17:25 +0000)
---------------------
Dealing with deriving
---------------------

I spent a ridiculously long time peering at a bug report whereby
a 'deriving' clause sent GHC 5.02.1 into a loop.  It was all to
do with allowing instances like

instance Foo a b => Baz (T a)

(Notice the 'b' on the left which does not appear on the right.)

I realised that it's hard for the deriving machinery to find a
fixpoint when these sort of instance decls are around.  So I
now constrain *derived* instance decls not to have this form;
all the tyvars on the left must appear on the right.

On the way I commoned up the previously-separate tcSimplify
machinery for 'deriving' and 'default' decls with that for
everything else.   As a result, quite a few files are touched.

I hope I havn't broken anything.

ghc/compiler/typecheck/Inst.lhs
ghc/compiler/typecheck/TcDefaults.lhs
ghc/compiler/typecheck/TcDeriv.lhs
ghc/compiler/typecheck/TcMType.lhs
ghc/compiler/typecheck/TcSimplify.lhs

index c3ae965..23eab62 100644 (file)
@@ -17,7 +17,7 @@ module Inst (
 
        tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, 
        ipNamesOfInst, ipNamesOfInsts, predsOfInst, predsOfInsts,
-       instLoc, getDictClassTys, 
+       instLoc, getDictClassTys, dictPred,
 
        lookupInst, lookupSimpleInst, LookupInstResult(..),
 
@@ -205,6 +205,9 @@ instLoc (Dict _ _         loc) = loc
 instLoc (Method _ _ _ _ _ loc) = loc
 instLoc (LitInst _ _ _    loc) = loc
 
+dictPred (Dict _ pred _ ) = pred
+dictPred inst            = pprPanic "dictPred" (ppr inst)
+
 getDictClassTys (Dict _ pred _) = getClassPredTys pred
 
 predsOfInsts :: [Inst] -> [PredType]
@@ -604,12 +607,16 @@ lookupInst dict@(Dict _ (ClassP clas tys) loc)
                                   Nothing          -> tcInstTyVar tv   `thenNF_Tc` \ tc_tv ->
                                                       returnTc (mkTyVarTy tc_tv)
           in
+               -- It's possible that not all the tyvars are in
+               -- the substitution, tenv. For example:
+               --      instance C X a => D X where ...
+               -- (presumably there's a functional dependency in class C)
+               -- Hence the mk_ty_arg to instantiate any un-substituted tyvars.        
           mapNF_Tc mk_ty_arg tyvars    `thenNF_Tc` \ ty_args ->
           let
-               subst         = mkTyVarSubst tyvars ty_args
-               dfun_rho      = substTy subst rho
-               (theta, _)    = tcSplitRhoTy dfun_rho
-               ty_app        = mkHsTyApp (HsVar dfun_id) ty_args
+               dfun_rho   = substTy (mkTyVarSubst tyvars ty_args) rho
+               (theta, _) = tcSplitRhoTy dfun_rho
+               ty_app     = mkHsTyApp (HsVar dfun_id) ty_args
           in
           if null theta then
                returnNF_Tc (SimpleInst ty_app)
index 66e56ef..6067ea8 100644 (file)
@@ -14,10 +14,10 @@ import RnHsSyn              ( RenamedHsDecl )
 import TcMonad
 import TcEnv           ( tcLookupGlobal_maybe )
 import TcMonoType      ( tcHsType )
-import TcSimplify      ( tcSimplifyCheckThetas )
+import TcSimplify      ( tcSimplifyDefault )
 
 import TysWiredIn      ( integerTy, doubleTy )
-import TcType           ( Type, mkClassPred )
+import TcType           ( Type, mkClassPred, isTauTy )
 import PrelNames       ( numClassName )
 import Outputable
 import HscTypes                ( TyThing(..) )
@@ -49,24 +49,26 @@ tc_defaults [DefaultDecl mono_tys locn]
                -- always sucking in Num
   where
     common_case num_class
-      = tcAddSrcLoc locn $
-       mapTc tcHsType mono_tys `thenTc` \ tau_tys ->
+      = tcAddSrcLoc locn               $
+       tcAddErrCtxt defaultDeclCtxt    $
+       mapTc tc_default_ty mono_tys    `thenTc` \ tau_tys ->
     
                -- Check that all the types are instances of Num
                -- We only care about whether it worked or not
-       tcAddErrCtxt defaultDeclCtxt            $
-       tcSimplifyCheckThetas
-                   [{- Nothing given -}]
-                   [ mkClassPred num_class [ty] | ty <- tau_tys ]      `thenTc_`
+       tcSimplifyDefault [mkClassPred num_class [ty] | ty <- tau_tys]  `thenTc_`
     
        returnTc tau_tys
 
-
 tc_defaults decls@(DefaultDecl _ loc : _) =
     tcAddSrcLoc loc $
     failWithTc (dupDefaultDeclErr decls)
 
 
+tc_default_ty hs_ty 
+ = tcHsType hs_ty                              `thenTc` \ ty ->
+   checkTc (isTauTy ty) (polyDefErr hs_ty)     `thenTc_`
+   returnTc ty
+
 defaultDeclCtxt =  ptext SLIT("when checking that each type in a default declaration")
                    $$ ptext SLIT("is an instance of class Num")
 
@@ -76,5 +78,8 @@ dupDefaultDeclErr (DefaultDecl _ locn1 : dup_things)
       4  (vcat (map pp dup_things))
   where
     pp (DefaultDecl _ locn) = ptext SLIT("here was another default declaration") <+> ppr locn
+
+polyDefErr ty 
+  = hang (ptext SLIT("Illegal polymorphic type in default declaration") <> colon) 4 (ppr ty) 
 \end{code}
 
index 9e54586..de7b2b3 100644 (file)
@@ -23,7 +23,7 @@ import TcEnv          ( tcSetInstEnv, newDFunName, InstInfo(..), pprInstInfo,
 import TcGenDeriv      -- Deriv stuff
 import InstEnv         ( InstEnv, simpleDFunClassTyCon, extendInstEnv )
 import TcMonoType      ( tcHsPred )
-import TcSimplify      ( tcSimplifyThetas )
+import TcSimplify      ( tcSimplifyDeriv )
 
 import RnBinds         ( rnMethodBinds, rnTopMonoBinds )
 import RnEnv           ( bindLocatedLocalsRn )
@@ -47,11 +47,11 @@ import TyCon                ( tyConTyVars, tyConDataCons, tyConArity, newTyConRep,
                        )
 import TcType          ( TcType, ThetaType, mkTyVarTys, mkTyConApp, getClassPredTys_maybe,
                          isUnLiftedType, mkClassPred, tyVarsOfTypes, tcSplitFunTys, 
-                         tcSplitTyConApp_maybe, tcEqTypes )
+                         tcSplitTyConApp_maybe, tcEqTypes, tyVarsOfTheta )
 import Var             ( TyVar, tyVarKind )
 import VarSet          ( mkVarSet, subVarSet )
 import PrelNames
-import Util            ( zipWithEqual, sortLt )
+import Util            ( zipWithEqual, sortLt, eqListBy )
 import ListSetOps      ( removeDups,  assoc )
 import Outputable
 import Maybe           ( isJust )
@@ -318,7 +318,7 @@ makeDerivEqns tycl_decls
     mk_eqn (new_or_data, tycon_name, pred)
       = tcLookupTyCon tycon_name               `thenNF_Tc` \ tycon ->
        tcAddSrcLoc (getSrcLoc tycon)           $
-        tcAddErrCtxt (derivCtxt tycon)         $
+        tcAddErrCtxt (derivCtxt Nothing tycon) $
        tcExtendTyVarEnv (tyConTyVars tycon)    $       -- Deriving preds may (now) mention
                                                        -- the type variables for the type constructor
         tcHsPred pred                          `thenTc` \ pred' ->
@@ -501,36 +501,29 @@ solveDerivEqns inst_env_in orig_eqns
        -- It fails if any iteration fails
     iterateDeriv :: [DerivSoln] ->TcM [DFunId]
     iterateDeriv current_solns
-      = checkNoErrsTc (iterateOnce current_solns)
-                                               `thenTc` \ (new_dfuns, new_solns) ->
+      =        getDOptsTc                              `thenNF_Tc` \ dflags ->
+        let 
+           dfuns    = zipWithEqual "add_solns" mk_deriv_dfun orig_eqns current_solns
+           inst_env = extend_inst_env dflags inst_env_in dfuns
+        in
+        checkNoErrsTc (
+                 -- Extend the inst info from the explicit instance decls
+                 -- with the current set of solutions, and simplify each RHS
+           tcSetInstEnv inst_env $
+           mapTc gen_soln orig_eqns
+       )                               `thenTc` \ new_solns ->
        if (current_solns == new_solns) then
-           returnTc new_dfuns
+           returnTc dfuns
        else
            iterateDeriv new_solns
 
     ------------------------------------------------------------------
-    iterateOnce current_solns
-      =            -- Extend the inst info from the explicit instance decls
-           -- with the current set of solutions, giving a
-       getDOptsTc                              `thenNF_Tc` \ dflags ->
-        let 
-           new_dfuns = zipWithEqual "add_solns" mk_deriv_dfun orig_eqns current_solns
-           inst_env  = extend_inst_env dflags inst_env_in new_dfuns
-           -- the eqns and solns move "in lockstep"; we have the eqns
-           -- because we need the LHS info for addClassInstance.
-        in
-           -- Simplify each RHS
-       tcSetInstEnv inst_env (
-         listTc [ tcAddSrcLoc (getSrcLoc tc)   $
-                  tcAddErrCtxt (derivCtxt tc)  $
-                  tcSimplifyThetas deriv_rhs
-                | (_, _,tc,_,deriv_rhs) <- orig_eqns ]  
-       )                                       `thenTc` \ next_solns ->
-
-           -- Canonicalise the solutions, so they compare nicely
-       let canonicalised_next_solns = [ sortLt (<) next_soln | next_soln <- next_solns ]
-       in
-       returnTc (new_dfuns, canonicalised_next_solns)
+
+    gen_soln (_, clas, tc,tyvars,deriv_rhs)
+      = tcAddSrcLoc (getSrcLoc tc)             $
+       tcAddErrCtxt (derivCtxt (Just clas) tc) $
+       tcSimplifyDeriv tyvars deriv_rhs        `thenTc` \ theta ->
+       returnTc (sortLt (<) theta)     -- Canonicalise before returning the soluction
 \end{code}
 
 \begin{code}
@@ -724,7 +717,12 @@ derivingThingErr clas tys tycon tyvars why
 
 malformedPredErr tycon pred = ptext SLIT("Illegal deriving item") <+> ppr pred
 
-derivCtxt tycon
-  = ptext SLIT("When deriving classes for") <+> quotes (ppr tycon)
+derivCtxt :: Maybe Class -> TyCon -> SDoc
+derivCtxt maybe_cls tycon
+  = ptext SLIT("When deriving") <+> cls <+> ptext SLIT("for type") <+> quotes (ppr tycon)
+  where
+    cls = case maybe_cls of
+           Nothing -> ptext SLIT("instances")
+           Just c  -> ptext SLIT("the") <+> quotes (ppr c) <+> ptext SLIT("instance")
 \end{code}
 
index 07166d8..e50be22 100644 (file)
@@ -27,7 +27,7 @@ module TcMType (
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
   SourceTyCtxt(..), checkValidTheta, 
-  checkValidInstHead, instTypeErr,
+  checkValidInstHead, instTypeErr, checkAmbiguity,
 
   --------------------------------
   -- Zonking
@@ -680,7 +680,8 @@ check_poly_type rank ty
     in
     check_valid_theta SigmaCtxt theta          `thenTc_`
     check_tau_type (decRank rank) False tau    `thenTc_`
-    checkAmbiguity tvs theta tau
+    checkFreeness tvs theta                    `thenTc_`
+    checkAmbiguity tvs theta (tyVarsOfType tau)
 
 ----------------------------------------
 check_arg_type :: Type -> TcM ()
@@ -756,6 +757,13 @@ check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
 ----------------------------------------
 check_note (FTVNote _)  = returnTc ()
 check_note (SynNote ty) = check_tau_type (Rank 0) False ty
+
+----------------------------------------
+forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
+usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
+unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
+ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
+kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 \end{code}
 
 Check for ambiguity
@@ -771,12 +779,6 @@ Then the type
        forall x y. (C x y) => x
 is not ambiguous because x is mentioned and x determines y
 
-NOTE: In addition, GHC insists that at least one type variable
-in each constraint is in V.  So we disallow a type like
-       forall a. Eq b => b -> b
-even in a scope where b is in scope.
-This is the is_free test below.
-
 NB; the ambiguity check is only used for *user* types, not for types
 coming from inteface files.  The latter can legitimately have
 ambiguous types. Example
@@ -795,46 +797,47 @@ don't need to check for ambiguity either, because the test can't fail
 (see is_ambig).
 
 \begin{code}
-checkAmbiguity :: [TyVar] -> ThetaType -> Type -> TcM ()
-checkAmbiguity forall_tyvars theta tau
-  = mapTc_ check_pred theta    `thenTc_`
-    returnTc ()
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+  = mapTc_ complain (filter is_ambig theta)
   where
-    tau_vars         = tyVarsOfType tau
-    extended_tau_vars = grow theta tau_vars
+    complain pred     = addErrTc (ambigErr pred)
+    extended_tau_vars = grow theta tau_tyvars
+    is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
 
-    is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
+    ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
                        not (ct_var `elemVarSet` extended_tau_vars)
+
     is_free ct_var    = not (ct_var `elem` forall_tyvars)
-    
-    check_pred pred = checkTc (not any_ambig)                 (ambigErr pred) `thenTc_`
-                     checkTc (isIPPred pred || not all_free) (freeErr  pred)
-             where 
-               ct_vars   = varSetElems (tyVarsOfPred pred)
-               all_free  = all is_free ct_vars
-               any_ambig = any is_ambig ct_vars
-\end{code}
 
-\begin{code}
 ambigErr pred
   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
         nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
                 ptext SLIT("must be reachable from the type after the '=>'"))]
+\end{code}
+    
+In addition, GHC insists that at least one type variable
+in each constraint is in V.  So we disallow a type like
+       forall a. Eq b => b -> b
+even in a scope where b is in scope.
 
+\begin{code}
+checkFreeness forall_tyvars theta
+  = mapTc_ complain (filter is_free theta)
+  where    
+    is_free pred     =  not (isIPPred pred)
+                    && not (any bound_var (varSetElems (tyVarsOfPred pred)))
+    bound_var ct_var = ct_var `elem` forall_tyvars
+    complain pred    = addErrTc (freeErr pred)
 
 freeErr pred
   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
                   ptext SLIT("are already in scope"),
         nest 4 (ptext SLIT("At least one must be universally quantified here"))
     ]
-
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
-usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
-unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
-ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
-kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Checking a theta or source type}
index 9229fcb..88827cd 100644 (file)
@@ -11,7 +11,7 @@ module TcSimplify (
        tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
 
-       tcSimplifyThetas, tcSimplifyCheckThetas,
+       tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns
     ) where
 
@@ -26,11 +26,11 @@ import TcHsSyn              ( TcExpr, TcId,
 
 import TcMonad
 import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
-                         tyVarsOfInst, predsOfInsts, predsOfInst,
+                         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,13 +40,14 @@ import Inst         ( lookupInst, lookupSimpleInst, LookupInstResult(..),
                        )
 import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars )
+import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
 import TcType          ( TcTyVar, TcTyVarSet, ThetaType, PredType, 
                          mkClassPred, isOverloadedTy, mkTyConApp,
-                         mkTyVarTy, tcGetTyVar, isTyVarClassPred,
+                         mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
                          tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
                          inheritablePred, predHasFDs )
 import Id              ( idType, mkUserLocal )
+import Var             ( TyVar )
 import Name            ( getOccName, getSrcLoc )
 import NameSet         ( NameSet, mkNameSet, elemNameSet )
 import Class           ( classBigSig )
@@ -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}
@@ -1519,26 +1523,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 +1539,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
@@ -1590,7 +1574,6 @@ tcSimplifyTop wanted_lie
     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 +1583,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 +1640,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 +1655,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 +1671,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 +1725,73 @@ 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 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
+         -- Check that the returned dictionaries are all of form (C a b)
+         --    (where a, b are type variables).  
+         -- Unless we have -fallow-undecidable-instances.
+         | not undecidable_ok && not (isTyVarClassPred pred)
+          = addErrTc (noInstErr pred)
+  
+         -- 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.
+         | not (tyVarsOfPred pred `subVarSet` tv_set) 
+         = addErrTc (badDerivedPred pred)
+  
+         | otherwise
+         = returnNF_Tc ()
+
+       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}
 
 
@@ -1979,8 +1938,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,