Implement auto-specialisation of imported Ids
[ghc-hetmet.git] / compiler / typecheck / TcDeriv.lhs
index fcd3fab..b994a27 100644 (file)
@@ -16,10 +16,12 @@ import DynFlags
 import Generics
 import TcRnMonad
 import TcEnv
-import TcGenDeriv      -- Deriv stuff
+import TcClassDcl( tcAddDeclCtxt )     -- Small helper
+import TcGenDeriv                      -- Deriv stuff
 import InstEnv
 import Inst
 import TcHsType
+import TcMType
 import TcSimplify
 
 import RnBinds
@@ -28,6 +30,7 @@ import HscTypes
 
 import Class
 import Type
+import Coercion
 import ErrUtils
 import MkId
 import DataCon
@@ -44,15 +47,89 @@ import SrcLoc
 import Util
 import ListSetOps
 import Outputable
+import FastString
 import Bag
+
+import Control.Monad
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection[TcDeriv-intro]{Introduction to how we do deriving}
+               Overview
 %*                                                                     *
 %************************************************************************
 
+Overall plan
+~~~~~~~~~~~~
+1.  Convert the decls (i.e. data/newtype deriving clauses, 
+    plus standalone deriving) to [EarlyDerivSpec]
+
+2.  Infer the missing contexts for the Left DerivSpecs
+
+3.  Add the derived bindings, generating InstInfos
+
+
+\begin{code}
+-- DerivSpec is purely  local to this module
+data DerivSpec  = DS { ds_loc     :: SrcSpan 
+                    , ds_orig    :: CtOrigin 
+                    , ds_name    :: Name
+                    , ds_tvs     :: [TyVar] 
+                    , ds_theta   :: ThetaType
+                    , ds_cls     :: Class
+                    , ds_tys     :: [Type]
+                    , ds_tc      :: TyCon
+                    , ds_tc_args :: [Type]
+                    , ds_newtype :: Bool }
+       -- This spec implies a dfun declaration of the form
+       --       df :: forall tvs. theta => C tys
+       -- The Name is the name for the DFun we'll build
+       -- The tyvars bind all the variables in the theta
+       -- For type families, the tycon in 
+       --       in ds_tys is the *family* tycon
+       --       in ds_tc, ds_tc_args is the *representation* tycon
+       -- For non-family tycons, both are the same
+
+       -- ds_newtype = True  <=> Newtype deriving
+       --              False <=> Vanilla deriving
+\end{code}
+
+Example:
+
+     newtype instance T [a] = MkT (Tree a) deriving( C s )
+==>  
+     axiom T [a] = :RTList a
+     axiom :RTList a = Tree a
+
+     DS { ds_tvs = [a,s], ds_cls = C, ds_tys = [s, T [a]]
+        , ds_tc = :RTList, ds_tc_args = [a]
+        , ds_newtype = True }
+
+\begin{code}
+type DerivContext = Maybe ThetaType
+   -- Nothing   <=> Vanilla deriving; infer the context of the instance decl
+   -- Just theta <=> Standalone deriving: context supplied by programmer
+
+type EarlyDerivSpec = Either DerivSpec DerivSpec
+       -- Left  ds => the context for the instance should be inferred
+       --             In this case ds_theta is the list of all the 
+       --                constraints needed, such as (Eq [a], Eq a)
+       --                The inference process is to reduce this to a 
+       --                simpler form (e.g. Eq a)
+       -- 
+       -- Right ds => the exact context for the instance is supplied 
+       --             by the programmer; it is ds_theta
+
+pprDerivSpec :: DerivSpec -> SDoc
+pprDerivSpec (DS { ds_loc = l, ds_name = n, ds_tvs = tvs, 
+                  ds_cls = c, ds_tys = tys, ds_theta = rhs })
+  = parens (hsep [ppr l, ppr n, ppr tvs, ppr c, ppr tys]
+           <+> equals <+> ppr rhs)
+\end{code}
+
+
+Inferring missing contexts 
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
        data T a b = C1 (Foo a) (Bar b)
@@ -131,26 +208,9 @@ this by simplifying the RHS to a form in which
 
 So, here are the synonyms for the ``equation'' structures:
 
-\begin{code}
-type DerivEqn = (SrcSpan, InstOrigin, Name, Class, TyCon, [TyVar], DerivRhs)
-               -- The Name is the name for the DFun we'll build
-               -- The tyvars bind all the variables in the RHS
-               -- For family indexes, the tycon is the representation tycon
-
-pprDerivEqn :: DerivEqn -> SDoc
-pprDerivEqn (l, _, n, c, tc, tvs, rhs)
-  = parens (hsep [ppr l, ppr n, ppr c, ppr origTc, ppr tys] <+> equals <+>
-           ppr rhs)
-  where
-    (origTc, tys) = tyConOrigHead tc
-
-type DerivRhs  = ThetaType
-type DerivSoln = DerivRhs
-\end{code}
 
-
-[Data decl contexts] A note about contexts on data decls
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Data decl contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
        data (RealFloat a) => Complex a = !a :+ !a deriving( Read )
@@ -177,8 +237,8 @@ pattern matching against a constructor from a data type with a context
 gives rise to the constraints for that context -- or at least the thinned
 version.  So now all classes are "offending".
 
-[Newtype deriving]
-~~~~~~~~~~~~~~~~~~
+Note [Newtype deriving]
+~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
     class C a b
     instance C [a] Char
@@ -191,7 +251,36 @@ And then translate it to:
     instance C [a] Char => C [a] T where ...
     
        
+Note [Newtype deriving superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(See also Trac #1220 for an interesting exchange on newtype
+deriving and superclasses.)
 
+The 'tys' here come from the partial application in the deriving
+clause. The last arg is the new instance type.
+
+We must pass the superclasses; the newtype might be an instance
+of them in a different way than the representation type
+E.g.           newtype Foo a = Foo a deriving( Show, Num, Eq )
+Then the Show instance is not done via isomorphism; it shows
+       Foo 3 as "Foo 3"
+The Num instance is derived via isomorphism, but the Show superclass
+dictionary must the Show instance for Foo, *not* the Show dictionary
+gotten from the Num dictionary. So we must build a whole new dictionary
+not just use the Num one.  The instance we want is something like:
+     instance (Num a, Show (Foo a), Eq (Foo a)) => Num (Foo a) where
+       (+) = ((+)@a)
+       ...etc...
+There may be a coercion needed which we get from the tycon for the newtype
+when the dict is constructed in TcInstDcls.tcInstDecl2
+
+
+Note [Unused constructors and deriving clauses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See Trac #3221.  Consider
+   data T = T1 | T2 deriving( Show )
+Are T1 and T2 unused?  Well, no: the deriving clause expands to mention
+both of them.  So we gather defs/uses from deriving just like anything else.
 
 %************************************************************************
 %*                                                                     *
@@ -200,257 +289,807 @@ And then translate it to:
 %************************************************************************
 
 \begin{code}
-tcDeriving  :: [LTyClDecl Name]        -- All type constructors
+tcDeriving  :: [LTyClDecl Name]  -- All type constructors
+            -> [LInstDecl Name]  -- All instance declarations
             -> [LDerivDecl Name] -- All stand-alone deriving declarations
-           -> TcM ([InstInfo],         -- The generated "instance decls"
-                   HsValBinds Name)    -- Extra generated top-level bindings
+           -> TcM ([InstInfo Name],    -- The generated "instance decls"
+                   HsValBinds Name,    -- Extra generated top-level bindings
+                    DefUses)
 
-tcDeriving tycl_decls deriv_decls
-  = recoverM (returnM ([], emptyValBindsOut)) $
+tcDeriving tycl_decls inst_decls deriv_decls
+  = recoverM (return ([], emptyValBindsOut, emptyDUs)) $
     do {       -- Fish the "deriving"-related information out of the TcEnv
-               -- and make the necessary "equations".
-         overlap_flag <- getOverlapFlag
-       ; (ordinary_eqns, newtype_inst_info) 
-            <- makeDerivEqns overlap_flag tycl_decls deriv_decls
-
-       ; (ordinary_inst_info, deriv_binds) 
-               <- extendLocalInstEnv (map iSpec newtype_inst_info)  $
-                  deriveOrdinaryStuff overlap_flag ordinary_eqns
-               -- Add the newtype-derived instances to the inst env
-               -- before tacking the "ordinary" ones
-
-       ; let inst_info = newtype_inst_info ++ ordinary_inst_info
-
-       -- If we are compiling a hs-boot file, 
-       -- don't generate any derived bindings
-       ; is_boot <- tcIsHsBoot
-       ; if is_boot then
-               return (inst_info, emptyValBindsOut)
-         else do
-       {
-
-       -- Generate the generic to/from functions from each type declaration
-       ; gen_binds <- mkGenericBinds tycl_decls
-
-       -- Rename these extra bindings, discarding warnings about unused bindings etc
-       -- Set -fglasgow exts so that we can have type signatures in patterns,
-       -- which is used in the generic binds
-       ; rn_binds
-               <- discardWarnings $ setOptM Opt_GlasgowExts $ do
-                       { (rn_deriv, _dus1) <- rnTopBinds (ValBindsIn deriv_binds [])
-                       ; (rn_gen, dus_gen) <- rnTopBinds (ValBindsIn gen_binds   [])
-                       ; keepAliveSetTc (duDefs dus_gen)       -- Mark these guys to
-                                                               -- be kept alive
-                       ; return (rn_deriv `plusHsValBinds` rn_gen) }
+               -- And make the necessary "equations".
+         is_boot <- tcIsHsBoot
+       ; traceTc "tcDeriving" (ppr is_boot)
+       ; early_specs <- makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
+
+       ; overlap_flag <- getOverlapFlag
+       ; let (infer_specs, given_specs) = splitEithers early_specs
+       ; insts1 <- mapM (genInst True overlap_flag) given_specs
 
+       ; final_specs <- extendLocalInstEnv (map (iSpec . fst) insts1) $
+                        inferInstanceContexts overlap_flag infer_specs
+
+       ; insts2 <- mapM (genInst False overlap_flag) final_specs
+
+                -- Generate the generic to/from functions from each type declaration
+       ; gen_binds <- mkGenericBinds is_boot tycl_decls
+       ; (inst_info, rn_binds, rn_dus) <- renameDeriv is_boot gen_binds (insts1 ++ insts2)
 
        ; dflags <- getDOpts
-       ; ioToTcRn (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances" 
-                  (ddump_deriving inst_info rn_binds))
+       ; liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
+                (ddump_deriving inst_info rn_binds))
 
-       ; returnM (inst_info, rn_binds)
-       }}
+       ; return (inst_info, rn_binds, rn_dus) }
   where
-    ddump_deriving :: [InstInfo] -> HsValBinds Name -> SDoc
+    ddump_deriving :: [InstInfo Name] -> HsValBinds Name -> SDoc
     ddump_deriving inst_infos extra_binds
       = vcat (map pprInstInfoDetails inst_infos) $$ ppr extra_binds
 
+renameDeriv :: Bool -> LHsBinds RdrName
+           -> [(InstInfo RdrName, DerivAuxBinds)]
+           -> TcM ([InstInfo Name], HsValBinds Name, DefUses)
+renameDeriv is_boot gen_binds insts
+  | is_boot    -- If we are compiling a hs-boot file, don't generate any derived bindings
+               -- The inst-info bindings will all be empty, but it's easier to
+               -- just use rn_inst_info to change the type appropriately
+  = do { (rn_inst_infos, fvs) <- mapAndUnzipM rn_inst_info inst_infos  
+       ; return (rn_inst_infos, emptyValBindsOut, usesOnly (plusFVs fvs)) }
+
+  | otherwise
+  = discardWarnings $   -- Discard warnings about unused bindings etc
+    do { (rn_gen, dus_gen) <- setOptM Opt_ScopedTypeVariables $  -- Type signatures in patterns 
+                                                                 -- are used in the generic binds
+                              rnTopBinds (ValBindsIn gen_binds [])
+       ; keepAliveSetTc (duDefs dus_gen)       -- Mark these guys to be kept alive
+
+               -- Generate and rename any extra not-one-inst-decl-specific binds, 
+               -- notably "con2tag" and/or "tag2con" functions.  
+               -- Bring those names into scope before renaming the instances themselves
+       ; loc <- getSrcSpanM    -- Generic loc for shared bindings
+       ; let (aux_binds, aux_sigs) = unzip $ map (genAuxBind loc) $ 
+                                     rm_dups [] $ concat deriv_aux_binds
+              aux_val_binds = ValBindsIn (listToBag aux_binds) aux_sigs
+       ; rn_aux_lhs <- rnTopBindsLHS emptyFsEnv aux_val_binds
+       ; bindLocalNames (collectHsValBinders rn_aux_lhs) $ 
+    do { (rn_aux, dus_aux) <- rnTopBindsRHS rn_aux_lhs
+       ; (rn_inst_infos, fvs_insts) <- mapAndUnzipM rn_inst_info inst_infos
+       ; return (rn_inst_infos, rn_aux `plusHsValBinds` rn_gen,
+                  dus_gen `plusDU` dus_aux `plusDU` usesOnly (plusFVs fvs_insts)) } }
+
+  where
+    (inst_infos, deriv_aux_binds) = unzip insts
+    
+       -- Remove duplicate requests for auxilliary bindings
+    rm_dups acc [] = acc
+    rm_dups acc (b:bs) | any (isDupAux b) acc = rm_dups acc bs
+                      | otherwise            = rm_dups (b:acc) bs
+
+
+    rn_inst_info :: InstInfo RdrName -> TcM (InstInfo Name, FreeVars)
+    rn_inst_info info@(InstInfo { iBinds = NewTypeDerived coi tc })
+       = return ( info { iBinds = NewTypeDerived coi tc }
+                 , mkFVs (map dataConName (tyConDataCons tc)))
+         -- See Note [Newtype deriving and unused constructors]
+
+    rn_inst_info (InstInfo { iSpec = inst, iBinds = VanillaInst binds sigs standalone_deriv })
+       =       -- Bring the right type variables into 
+               -- scope (yuk), and rename the method binds
+          ASSERT( null sigs )
+          bindLocalNames (map Var.varName tyvars) $
+          do { (rn_binds, fvs) <- rnMethodBinds clas_nm (\_ -> []) [] binds
+             ; let binds' = VanillaInst rn_binds [] standalone_deriv
+             ; return (InstInfo { iSpec = inst, iBinds = binds' }, fvs) }
+       where
+         (tyvars,_, clas,_) = instanceHead inst
+         clas_nm            = className clas
+
 -----------------------------------------
-deriveOrdinaryStuff overlap_flag []    -- Short cut
-  = returnM ([], emptyLHsBinds)
+mkGenericBinds :: Bool -> [LTyClDecl Name] -> TcM (LHsBinds RdrName)
+mkGenericBinds is_boot tycl_decls
+  | is_boot 
+  = return emptyBag
+  | otherwise
+  = do { tcs <- mapM tcLookupTyCon [ tcdName d 
+                                   | L _ d <- tycl_decls, isDataDecl d ]
+       ; return (unionManyBags [ mkTyConGenericBinds tc
+                               | tc <- tcs, tyConHasGenerics tc ]) }
+               -- We are only interested in the data type declarations,
+               -- and then only in the ones whose 'has-generics' flag is on
+               -- The predicate tyConHasGenerics finds both of these
+\end{code}
 
-deriveOrdinaryStuff overlap_flag eqns
-  = do {       -- Take the equation list and solve it, to deliver a list of
-               -- solutions, a.k.a. the contexts for the instance decls
-               -- required for the corresponding equations.
-         inst_specs <- solveDerivEqns overlap_flag eqns
+Note [Newtype deriving and unused constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this (see Trac #1954):
 
-       -- Generate the InstInfo for each dfun, 
-       -- plus any auxiliary bindings it needs
-       ; (inst_infos, aux_binds_s) <- mapAndUnzipM genInst inst_specs
+  module Bug(P) where
+  newtype P a = MkP (IO a) deriving Monad
 
-       -- Generate any extra not-one-inst-decl-specific binds, 
-       -- notably "con2tag" and/or "tag2con" functions.  
-       ; extra_binds <- genTaggeryBinds inst_infos
+If you compile with -fwarn-unused-binds you do not expect the warning
+"Defined but not used: data consructor MkP". Yet the newtype deriving
+code does not explicitly mention MkP, but it should behave as if you
+had written
+  instance Monad P where
+     return x = MkP (return x)
+     ...etc...
 
-       -- Done
-       ; returnM (map fst inst_infos, 
-                  unionManyBags (extra_binds : aux_binds_s))
-   }
+So we want to signal a user of the data constructor 'MkP'.  That's
+what we do in rn_inst_info, and it's the only reason we have the TyCon
+stored in NewTypeDerived.
 
------------------------------------------
-mkGenericBinds tycl_decls
-  = do { tcs <- mapM tcLookupTyCon 
-                       [ tc_name | 
-                         L _ (TyData { tcdLName = L _ tc_name }) <- tycl_decls]
-               -- We are only interested in the data type declarations
-       ; return (unionManyBags [ mkTyConGenericBinds tc | 
-                                 tc <- tcs, tyConHasGenerics tc ]) }
-               -- And then only in the ones whose 'has-generics' flag is on
+
+%************************************************************************
+%*                                                                     *
+               From HsSyn to DerivSpec
+%*                                                                     *
+%************************************************************************
+
+@makeDerivSpecs@ fishes around to find the info about needed derived instances.
+
+\begin{code}
+makeDerivSpecs :: Bool 
+              -> [LTyClDecl Name] 
+               -> [LInstDecl Name]
+              -> [LDerivDecl Name] 
+              -> TcM [EarlyDerivSpec]
+
+makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
+  | is_boot    -- No 'deriving' at all in hs-boot files
+  = do { mapM_ add_deriv_err deriv_locs 
+       ; return [] }
+  | otherwise
+  = do { eqns1 <- mapAndRecoverM deriveTyData all_tydata
+       ; eqns2 <- mapAndRecoverM deriveStandalone deriv_decls
+       ; return (eqns1 ++ eqns2) }
+  where
+    extractTyDataPreds decls
+      = [(p, d) | d@(L _ (TyData {tcdDerivs = Just preds})) <- decls, p <- preds]
+
+    all_tydata :: [(LHsType Name, LTyClDecl Name)]
+       -- Derived predicate paired with its data type declaration
+    all_tydata = extractTyDataPreds (instDeclATs inst_decls ++ tycl_decls)
+
+    deriv_locs = map (getLoc . snd) all_tydata
+                ++ map getLoc deriv_decls
+
+    add_deriv_err loc = setSrcSpan loc $
+                       addErr (hang (ptext (sLit "Deriving not permitted in hs-boot file"))
+                                  2 (ptext (sLit "Use an instance declaration instead")))
+
+------------------------------------------------------------------
+deriveStandalone :: LDerivDecl Name -> TcM EarlyDerivSpec
+-- Standalone deriving declarations
+--  e.g.   deriving instance Show a => Show (T a)
+-- Rather like tcLocalInstDecl
+deriveStandalone (L loc (DerivDecl deriv_ty))
+  = setSrcSpan loc                   $
+    addErrCtxt (standaloneCtxt deriv_ty)  $
+    do { traceTc "Standalone deriving decl for" (ppr deriv_ty)
+       ; (tvs, theta, tau) <- tcHsInstHead deriv_ty
+       ; traceTc "Standalone deriving;" $ vcat
+              [ text "tvs:" <+> ppr tvs
+              , text "theta:" <+> ppr theta
+              , text "tau:" <+> ppr tau ]
+       ; (cls, inst_tys) <- checkValidInstance deriv_ty tvs theta tau
+               -- C.f. TcInstDcls.tcLocalInstDecl1
+
+       ; let cls_tys = take (length inst_tys - 1) inst_tys
+             inst_ty = last inst_tys
+       ; traceTc "Standalone deriving:" $ vcat
+              [ text "class:" <+> ppr cls
+              , text "class types:" <+> ppr cls_tys
+              , text "type:" <+> ppr inst_ty ]
+       ; mkEqnHelp StandAloneDerivOrigin tvs cls cls_tys inst_ty
+                   (Just theta) }
+
+------------------------------------------------------------------
+deriveTyData :: (LHsType Name, LTyClDecl Name) -> TcM EarlyDerivSpec
+deriveTyData (L loc deriv_pred, L _ decl@(TyData { tcdLName = L _ tycon_name, 
+                                                  tcdTyVars = tv_names, 
+                                                  tcdTyPats = ty_pats }))
+  = setSrcSpan loc     $       -- Use the location of the 'deriving' item
+    tcAddDeclCtxt decl $
+    do { (tvs, tc, tc_args) <- get_lhs ty_pats
+       ; tcExtendTyVarEnv tvs $        -- Deriving preds may (now) mention
+                                       -- the type variables for the type constructor
+
+    do { (deriv_tvs, cls, cls_tys) <- tcHsDeriv deriv_pred
+               -- The "deriv_pred" is a LHsType to take account of the fact that for
+               -- newtype deriving we allow deriving (forall a. C [a]).
+
+       -- Given data T a b c = ... deriving( C d ),
+       -- we want to drop type variables from T so that (C d (T a)) is well-kinded
+       ; let cls_tyvars = classTyVars cls
+             kind = tyVarKind (last cls_tyvars)
+             (arg_kinds, _) = splitKindFunTys kind
+             n_args_to_drop = length arg_kinds 
+             n_args_to_keep = tyConArity tc - n_args_to_drop
+             args_to_drop   = drop n_args_to_keep tc_args
+             inst_ty        = mkTyConApp tc (take n_args_to_keep tc_args)
+             inst_ty_kind   = typeKind inst_ty
+             dropped_tvs    = mkVarSet (mapCatMaybes getTyVar_maybe args_to_drop)
+             univ_tvs       = (mkVarSet tvs `extendVarSetList` deriv_tvs)
+                                       `minusVarSet` dropped_tvs
+       -- Check that the result really is well-kinded
+       ; checkTc (n_args_to_keep >= 0 && (inst_ty_kind `eqKind` kind))
+                 (derivingKindErr tc cls cls_tys kind)
+
+       ; checkTc (sizeVarSet dropped_tvs == n_args_to_drop &&           -- (a)
+                  tyVarsOfTypes (inst_ty:cls_tys) `subVarSet` univ_tvs) -- (b)
+                 (derivingEtaErr cls cls_tys inst_ty)
+               -- Check that 
+               --  (a) The data type can be eta-reduced; eg reject:
+               --              data instance T a a = ... deriving( Monad )
+               --  (b) The type class args do not mention any of the dropped type
+               --      variables 
+               --              newtype T a s = ... deriving( ST s )
+
+       -- Type families can't be partially applied
+       -- e.g.   newtype instance T Int a = MkT [a] deriving( Monad )
+       -- Note [Deriving, type families, and partial applications]
+       ; checkTc (not (isFamilyTyCon tc) || n_args_to_drop == 0)
+                 (typeFamilyPapErr tc cls cls_tys inst_ty)
+
+       ; mkEqnHelp DerivOrigin (varSetElems univ_tvs) cls cls_tys inst_ty Nothing } }
+  where
+       -- Tiresomely we must figure out the "lhs", which is awkward for type families
+       -- E.g.   data T a b = .. deriving( Eq )
+       --          Here, the lhs is (T a b)
+       --        data instance TF Int b = ... deriving( Eq )
+       --          Here, the lhs is (TF Int b)
+       -- But if we just look up the tycon_name, we get is the *family*
+       -- tycon, but not pattern types -- they are in the *rep* tycon.
+    get_lhs Nothing     = do { tc <- tcLookupTyCon tycon_name
+                            ; let tvs = tyConTyVars tc
+                            ; return (tvs, tc, mkTyVarTys tvs) }
+    get_lhs (Just pats) = do { let hs_app = nlHsTyConApp tycon_name pats
+                            ; (tvs, tc_app) <- tcHsQuantifiedType tv_names hs_app
+                            ; let (tc, tc_args) = tcSplitTyConApp tc_app
+                            ; return (tvs, tc, tc_args) }
+
+deriveTyData _other
+  = panic "derivTyData"        -- Caller ensures that only TyData can happen
+\end{code}
+
+Note [Deriving, type families, and partial applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When there are no type families, it's quite easy:
+
+    newtype S a = MkS [a]
+    -- :CoS :: S  ~ [] -- Eta-reduced
+
+    instance Eq [a] => Eq (S a)        -- by coercion sym (Eq (:CoS a)) : Eq [a] ~ Eq (S a)
+    instance Monad [] => Monad S       -- by coercion sym (Monad :CoS)  : Monad [] ~ Monad S 
+
+When type familes are involved it's trickier:
+
+    data family T a b
+    newtype instance T Int a = MkT [a] deriving( Eq, Monad )
+    -- :RT is the representation type for (T Int a)
+    --  :CoF:R1T a :: T Int a ~ :RT a  -- Not eta reduced
+    --  :Co:R1T    :: :RT ~ []         -- Eta-reduced
+
+    instance Eq [a] => Eq (T Int a)    -- easy by coercion
+    instance Monad [] => Monad (T Int) -- only if we can eta reduce???
+
+The "???" bit is that we don't build the :CoF thing in eta-reduced form
+Henc the current typeFamilyPapErr, even though the instance makes sense.
+After all, we can write it out
+    instance Monad [] => Monad (T Int) -- only if we can eta reduce???
+      return x = MkT [x]
+      ... etc ...      
+
+\begin{code}
+mkEqnHelp :: CtOrigin -> [TyVar] -> Class -> [Type] -> Type
+          -> DerivContext      -- Just    => context supplied (standalone deriving)
+                               -- Nothing => context inferred (deriving on data decl)
+          -> TcRn EarlyDerivSpec
+-- Make the EarlyDerivSpec for an instance
+--     forall tvs. theta => cls (tys ++ [ty])
+-- where the 'theta' is optional (that's the Maybe part)
+-- Assumes that this declaration is well-kinded
+
+mkEqnHelp orig tvs cls cls_tys tc_app mtheta
+  | Just (tycon, tc_args) <- tcSplitTyConApp_maybe tc_app
+  , isAlgTyCon tycon   -- Check for functions, primitive types etc
+  = do { (rep_tc, rep_tc_args) <- tcLookupDataFamInst tycon tc_args
+                 -- Be careful to test rep_tc here: in the case of families, 
+                 -- we want to check the instance tycon, not the family tycon
+
+       -- For standalone deriving (mtheta /= Nothing), 
+       -- check that all the data constructors are in scope.
+       -- No need for this when deriving Typeable, becuase we don't need
+       -- the constructors for that.
+       ; rdr_env <- getGlobalRdrEnv
+       ; let hidden_data_cons = isAbstractTyCon rep_tc || any not_in_scope (tyConDataCons rep_tc)
+             not_in_scope dc  = null (lookupGRE_Name rdr_env (dataConName dc))
+       ; checkTc (isNothing mtheta || 
+                  not hidden_data_cons ||
+                  className cls `elem` typeableClassNames) 
+                 (derivingHiddenErr tycon)
+
+       ; dflags <- getDOpts
+       ; if isDataTyCon rep_tc then
+               mkDataTypeEqn orig dflags tvs cls cls_tys
+                             tycon tc_args rep_tc rep_tc_args mtheta
+         else
+               mkNewTypeEqn orig dflags tvs cls cls_tys 
+                            tycon tc_args rep_tc rep_tc_args mtheta }
+  | otherwise
+  = failWithTc (derivingThingErr False cls cls_tys tc_app
+              (ptext (sLit "The last argument of the instance must be a data or newtype application")))
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[TcDeriv-eqns]{Forming the equations}
+               Deriving data types
 %*                                                                     *
 %************************************************************************
 
-@makeDerivEqns@ fishes around to find the info about needed derived
-instances.  Complicating factors:
-\begin{itemize}
-\item
-We can only derive @Enum@ if the data type is an enumeration
-type (all nullary data constructors).
+\begin{code}
+mkDataTypeEqn :: CtOrigin
+              -> DynFlags
+              -> [Var]                  -- Universally quantified type variables in the instance
+              -> Class                  -- Class for which we need to derive an instance
+              -> [Type]                 -- Other parameters to the class except the last
+              -> TyCon                  -- Type constructor for which the instance is requested 
+                                       --    (last parameter to the type class)
+              -> [Type]                 -- Parameters to the type constructor
+              -> TyCon                  -- rep of the above (for type families)
+              -> [Type]                 -- rep of the above
+              -> DerivContext        -- Context of the instance, for standalone deriving
+              -> TcRn EarlyDerivSpec    -- Return 'Nothing' if error
+
+mkDataTypeEqn orig dflags tvs cls cls_tys
+              tycon tc_args rep_tc rep_tc_args mtheta
+  = case checkSideConditions dflags mtheta cls cls_tys rep_tc of
+       -- NB: pass the *representation* tycon to checkSideConditions
+       CanDerive               -> go_for_it
+       NonDerivableClass       -> bale_out (nonStdErr cls)
+       DerivableClassError msg -> bale_out msg
+  where
+    go_for_it    = mk_data_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
+    bale_out msg = failWithTc (derivingThingErr False cls cls_tys (mkTyConApp tycon tc_args) msg)
 
-\item
-We can only derive @Ix@ if the data type is an enumeration {\em
-or} has just one data constructor (e.g., tuples).
-\end{itemize}
+mk_data_eqn, mk_typeable_eqn
+   :: CtOrigin -> [TyVar] -> Class 
+   -> TyCon -> [TcType] -> TyCon -> [TcType] -> DerivContext
+   -> TcM EarlyDerivSpec
+mk_data_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
+  | getName cls `elem` typeableClassNames
+  = mk_typeable_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
 
-[See Appendix~E in the Haskell~1.2 report.] This code here deals w/
-all those.
+  | otherwise
+  = do { dfun_name <- new_dfun_name cls tycon
+       ; loc <- getSrcSpanM
+       ; let inst_tys = [mkTyConApp tycon tc_args]
+             inferred_constraints = inferConstraints tvs cls inst_tys rep_tc rep_tc_args
+             spec = DS { ds_loc = loc, ds_orig = orig
+                       , ds_name = dfun_name, ds_tvs = tvs 
+                       , ds_cls = cls, ds_tys = inst_tys
+                       , ds_tc = rep_tc, ds_tc_args = rep_tc_args
+                       , ds_theta =  mtheta `orElse` inferred_constraints
+                       , ds_newtype = False }
+
+       ; return (if isJust mtheta then Right spec      -- Specified context
+                                  else Left spec) }    -- Infer context
+
+mk_typeable_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
+       -- The Typeable class is special in several ways
+       --        data T a b = ... deriving( Typeable )
+       -- gives
+       --        instance Typeable2 T where ...
+       -- Notice that:
+       -- 1. There are no constraints in the instance
+       -- 2. There are no type variables either
+       -- 3. The actual class we want to generate isn't necessarily
+       --      Typeable; it depends on the arity of the type
+  | isNothing mtheta   -- deriving on a data type decl
+  = do { checkTc (cls `hasKey` typeableClassKey)
+                 (ptext (sLit "Use deriving( Typeable ) on a data type declaration"))
+       ; real_cls <- tcLookupClass (typeableClassNames !! tyConArity tycon)
+       ; mk_typeable_eqn orig tvs real_cls tycon [] rep_tc [] (Just []) }
+
+  | otherwise          -- standaone deriving
+  = do { checkTc (null tc_args)
+                 (ptext (sLit "Derived typeable instance must be of form (Typeable") 
+                       <> int (tyConArity tycon) <+> ppr tycon <> rparen)
+       ; dfun_name <- new_dfun_name cls tycon
+       ; loc <- getSrcSpanM
+       ; return (Right $
+                 DS { ds_loc = loc, ds_orig = orig, ds_name = dfun_name, ds_tvs = []
+                    , ds_cls = cls, ds_tys = [mkTyConApp tycon []]
+                    , ds_tc = rep_tc, ds_tc_args = rep_tc_args
+                    , ds_theta = mtheta `orElse` [], ds_newtype = False })  }
+
+
+inferConstraints :: [TyVar] -> Class -> [TcType] -> TyCon -> [TcType] -> ThetaType
+-- Generate a sufficiently large set of constraints that typechecking the
+-- generated method definitions should succeed.   This set will be simplified
+-- before being used in the instance declaration
+inferConstraints _ cls inst_tys rep_tc rep_tc_args
+  = ASSERT2( equalLength rep_tc_tvs all_rep_tc_args, ppr cls <+> ppr rep_tc )
+    stupid_constraints ++ extra_constraints
+    ++ sc_constraints ++ con_arg_constraints
+  where
+       -- Constraints arising from the arguments of each constructor
+    con_arg_constraints
+      = [ mkClassPred cls [arg_ty] 
+        | data_con <- tyConDataCons rep_tc,
+          arg_ty   <- ASSERT( isVanillaDataCon data_con )
+                       get_constrained_tys $
+                       dataConInstOrigArgTys data_con all_rep_tc_args,
+          not (isUnLiftedType arg_ty) ]
+               -- No constraints for unlifted types
+               -- Where they are legal we generate specilised function calls
+
+               -- For functor-like classes, two things are different
+               -- (a) We recurse over argument types to generate constraints
+               --     See Functor examples in TcGenDeriv
+               -- (b) The rep_tc_args will be one short
+    is_functor_like = getUnique cls `elem` functorLikeClassKeys
+
+    get_constrained_tys :: [Type] -> [Type]
+    get_constrained_tys tys 
+       | is_functor_like = concatMap (deepSubtypesContaining last_tv) tys
+       | otherwise       = tys
+
+    rep_tc_tvs = tyConTyVars rep_tc
+    last_tv = last rep_tc_tvs
+    all_rep_tc_args | is_functor_like = rep_tc_args ++ [mkTyVarTy last_tv]
+                   | otherwise       = rep_tc_args
+
+       -- Constraints arising from superclasses
+       -- See Note [Superclasses of derived instance]
+    sc_constraints = substTheta (zipOpenTvSubst (classTyVars cls) inst_tys)
+                               (classSCTheta cls)
+
+       -- Stupid constraints
+    stupid_constraints = substTheta subst (tyConStupidTheta rep_tc)
+    subst = zipTopTvSubst rep_tc_tvs all_rep_tc_args
+             
+       -- Extra Data constraints
+       -- The Data class (only) requires that for 
+       --    instance (...) => Data (T t1 t2) 
+       -- IF   t1:*, t2:*
+       -- THEN (Data t1, Data t2) are among the (...) constraints
+       -- Reason: when the IF holds, we generate a method
+       --             dataCast2 f = gcast2 f
+       --         and we need the Data constraints to typecheck the method
+    extra_constraints 
+      | cls `hasKey` dataClassKey
+      , all (isLiftedTypeKind . typeKind) rep_tc_args 
+      = [mkClassPred cls [ty] | ty <- rep_tc_args]
+      | otherwise 
+      = []
 
-Note [Newtype deriving superclasses]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The 'tys' here come from the partial application in the deriving
-clause. The last arg is the new instance type.
+------------------------------------------------------------------
+-- Check side conditions that dis-allow derivability for particular classes
+-- This is *apart* from the newtype-deriving mechanism
+--
+-- Here we get the representation tycon in case of family instances as it has
+-- the data constructors - but we need to be careful to fall back to the
+-- family tycon (with indexes) in error messages.
+
+data DerivStatus = CanDerive
+                | DerivableClassError SDoc     -- Standard class, but can't do it
+                | NonDerivableClass            -- Non-standard class
+
+checkSideConditions :: DynFlags -> DerivContext -> Class -> [TcType] -> TyCon -> DerivStatus
+checkSideConditions dflags mtheta cls cls_tys rep_tc
+  | Just cond <- sideConditions mtheta cls
+  = case (cond (dflags, rep_tc)) of
+       Just err -> DerivableClassError err     -- Class-specific error
+       Nothing  | null cls_tys -> CanDerive    -- All derivable classes are unary, so
+                                               -- cls_tys (the type args other than last) 
+                                               -- should be null
+                | otherwise    -> DerivableClassError ty_args_why      -- e.g. deriving( Eq s )
+  | otherwise = NonDerivableClass      -- Not a standard class
+  where
+    ty_args_why        = quotes (ppr (mkClassPred cls cls_tys)) <+> ptext (sLit "is not a class")
+
+nonStdErr :: Class -> SDoc
+nonStdErr cls = quotes (ppr cls) <+> ptext (sLit "is not a derivable class")
+
+sideConditions :: DerivContext -> Class -> Maybe Condition
+sideConditions mtheta cls
+  | cls_key == eqClassKey                 = Just cond_std
+  | cls_key == ordClassKey                = Just cond_std
+  | cls_key == showClassKey               = Just cond_std
+  | cls_key == readClassKey               = Just (cond_std `andCond` cond_noUnliftedArgs)
+  | cls_key == enumClassKey               = Just (cond_std `andCond` cond_isEnumeration)
+  | cls_key == ixClassKey                 = Just (cond_std `andCond` cond_enumOrProduct)
+  | cls_key == boundedClassKey            = Just (cond_std `andCond` cond_enumOrProduct)
+  | cls_key == dataClassKey               = Just (checkFlag Opt_DeriveDataTypeable `andCond` 
+                                           cond_std `andCond` cond_noUnliftedArgs)
+  | cls_key == functorClassKey            = Just (checkFlag Opt_DeriveFunctor `andCond`
+                                          cond_functorOK True)  -- NB: no cond_std!
+  | cls_key == foldableClassKey           = Just (checkFlag Opt_DeriveFoldable `andCond`
+                                          cond_functorOK False) -- Functor/Fold/Trav works ok for rank-n types
+  | cls_key == traversableClassKey = Just (checkFlag Opt_DeriveTraversable `andCond`
+                                          cond_functorOK False)
+  | getName cls `elem` typeableClassNames = Just (checkFlag Opt_DeriveDataTypeable `andCond` cond_typeableOK)
+  | otherwise = Nothing
+  where
+    cls_key = getUnique cls
+    cond_std = cond_stdOK mtheta
 
-We must pass the superclasses; the newtype might be an instance
-of them in a different way than the representation type
-E.g.           newtype Foo a = Foo a deriving( Show, Num, Eq )
-Then the Show instance is not done via isomorphism; it shows
-       Foo 3 as "Foo 3"
-The Num instance is derived via isomorphism, but the Show superclass
-dictionary must the Show instance for Foo, *not* the Show dictionary
-gotten from the Num dictionary. So we must build a whole new dictionary
-not just use the Num one.  The instance we want is something like:
-     instance (Num a, Show (Foo a), Eq (Foo a)) => Num (Foo a) where
-       (+) = ((+)@a)
-       ...etc...
-There may be a coercion needed which we get from the tycon for the newtype
-when the dict is constructed in TcInstDcls.tcInstDecl2
+type Condition = (DynFlags, TyCon) -> Maybe SDoc
+       -- first Bool is whether or not we are allowed to derive Data and Typeable
+       -- second Bool is whether or not we are allowed to derive Functor
+       -- TyCon is the *representation* tycon if the 
+       --      data type is an indexed one
+       -- Nothing => OK
+
+orCond :: Condition -> Condition -> Condition
+orCond c1 c2 tc 
+  = case c1 tc of
+       Nothing -> Nothing          -- c1 succeeds
+       Just x  -> case c2 tc of    -- c1 fails
+                    Nothing -> Nothing
+                    Just y  -> Just (x $$ ptext (sLit "  and") $$ y)
+                                   -- Both fail
 
+andCond :: Condition -> Condition -> Condition
+andCond c1 c2 tc = case c1 tc of
+                    Nothing -> c2 tc   -- c1 succeeds
+                    Just x  -> Just x  -- c1 fails
 
-\begin{code}
-type DerivSpec = (SrcSpan,             -- location of the deriving clause
-                 InstOrigin,           -- deriving at data decl or standalone?
-                 NewOrData,            -- newtype or data type
-                 Name,                 -- Type constructor for which we derive
-                 [LHsTyVarBndr Name],  -- Type variables
-                 Maybe [LHsType Name], -- Type indexes if indexed type
-                 LHsType Name)         -- Class instance to be generated
-
-makeDerivEqns :: OverlapFlag
-             -> [LTyClDecl Name] 
-             -> [LDerivDecl Name] 
-             -> TcM ([DerivEqn],       -- Ordinary derivings
-                     [InstInfo])       -- Special newtype derivings
-
-makeDerivEqns overlap_flag tycl_decls deriv_decls
-  = do derive_top_level <- mapM top_level_deriv deriv_decls
-       (maybe_ordinaries, maybe_newtypes) 
-           <- mapAndUnzipM mk_eqn (derive_data ++ catMaybes derive_top_level)
-       return (catMaybes maybe_ordinaries, catMaybes maybe_newtypes)
+cond_stdOK :: DerivContext -> Condition
+cond_stdOK (Just _) _
+  = Nothing    -- Don't check these conservative conditions for
+               -- standalone deriving; just generate the code
+               -- and let the typechecker handle the result
+cond_stdOK Nothing (_, rep_tc)
+  | null data_cons      = Just (no_cons_why rep_tc $$ suggestion)
+  | not (null con_whys) = Just (vcat con_whys $$ suggestion)
+  | otherwise          = Nothing
   where
-    ------------------------------------------------------------------
-    -- Deriving clauses at data declarations
-    derive_data :: [DerivSpec]
-    derive_data = [ (loc, DerivOrigin, nd, tycon, tyVars, tyPats, pred) 
-                  | L loc (TyData { tcdND = nd, tcdLName = L _ tycon, 
-                                    tcdTyVars = tyVars, tcdTyPats = tyPats,
-                                    tcdDerivs = Just preds }) <- tycl_decls,
-                    pred <- preds ]
-
-    -- Standalone deriving declarations
-    top_level_deriv :: LDerivDecl Name -> TcM (Maybe DerivSpec)
-    top_level_deriv d@(L loc (DerivDecl inst ty_name)) = 
-      recoverM (returnM Nothing) $ setSrcSpan loc $ 
-        do tycon <- tcLookupLocatedTyCon ty_name
-           let new_or_data = if isNewTyCon tycon then NewType else DataType
-          let tyVars = [ noLoc $ KindedTyVar (tyVarName tv) (tyVarKind tv)
-                       | tv <- tyConTyVars tycon]           -- Yuk!!!
-           traceTc (text "Stand-alone deriving:" <+> 
-                   ppr (new_or_data, unLoc ty_name, inst))
-           return $ Just (loc, StandAloneDerivOrigin, new_or_data, 
-                         unLoc ty_name, tyVars, Nothing, inst)
+    suggestion  = ptext (sLit "Possible fix: use a standalone deriving declaration instead")
+    data_cons   = tyConDataCons rep_tc
+    con_whys = mapCatMaybes check_con data_cons
+
+    check_con :: DataCon -> Maybe SDoc
+    check_con con 
+      | isVanillaDataCon con
+      , all isTauTy (dataConOrigArgTys con) = Nothing
+      | otherwise = Just (badCon con (ptext (sLit "does not have a Haskell-98 type")))
+  
+no_cons_why :: TyCon -> SDoc
+no_cons_why rep_tc = quotes (pprSourceTyCon rep_tc) <+> 
+                    ptext (sLit "has no data constructors")
+
+cond_enumOrProduct :: Condition
+cond_enumOrProduct = cond_isEnumeration `orCond` 
+                      (cond_isProduct `andCond` cond_noUnliftedArgs)
+
+cond_noUnliftedArgs :: Condition
+-- For some classes (eg Eq, Ord) we allow unlifted arg types
+-- by generating specilaised code.  For others (eg Data) we don't.
+cond_noUnliftedArgs (_, tc)
+  | null bad_cons = Nothing
+  | otherwise     = Just why
+  where
+    bad_cons = [ con | con <- tyConDataCons tc
+                    , any isUnLiftedType (dataConOrigArgTys con) ]
+    why = badCon (head bad_cons) (ptext (sLit "has arguments of unlifted type"))
 
-    ------------------------------------------------------------------
-    -- Derive equation/inst info for one deriving clause (data or standalone)
-    mk_eqn :: DerivSpec -> TcM (Maybe DerivEqn, Maybe InstInfo)
-       -- We swizzle the datacons out of the tycon to make the rest of the
-       -- equation.  We can't get the tyvars out of the constructor in case
-       -- of family instances, as we already need to them to lookup the
-       -- representation tycon (only that has the right set of type
-       -- variables, the type variables of the family constructor are
-       -- different).
-       --
-       -- The "deriv_ty" is a LHsType to take account of the fact that for
-       -- newtype deriving we allow deriving (forall a. C [a]).
-
-    mk_eqn (loc, orig, new_or_data, tycon_name, tyvars, mb_tys, hs_deriv_ty)
-      = setSrcSpan loc                            $
-        addErrCtxt (derivCtxt tycon_name mb_tys)  $
-        do { named_tycon <- tcLookupTyCon tycon_name
-
-            -- Enable deriving preds to mention the type variables in the
-            -- instance type
-           ; tcTyVarBndrs tyvars $ \tvs -> do 
-           { traceTc (text "TcDeriv.mk_eqn: tyvars:" <+> ppr tvs)
-
-             -- Lookup representation tycon in case of a family instance
-            -- NB: We already need the type variables in scope here for the
-            --     call to `dsHsType'.
-          ; tycon <- case mb_tys of
-                       Nothing    -> return named_tycon
-                       Just hsTys -> do
-                                       tys <- mapM dsHsType hsTys
-                                       tcLookupFamInst named_tycon tys
-
-          ; (deriv_tvs, clas, tys) <- tcHsDeriv hs_deriv_ty
-          ; gla_exts <- doptM Opt_GlasgowExts
-           ; mk_eqn_help loc orig gla_exts new_or_data tycon deriv_tvs clas tys
-          }}
+cond_isEnumeration :: Condition
+cond_isEnumeration (_, rep_tc)
+  | isEnumerationTyCon rep_tc   = Nothing
+  | otherwise                  = Just why
+  where
+    why = sep [ quotes (pprSourceTyCon rep_tc) <+> 
+                 ptext (sLit "is not an enumeration type")
+              , nest 2 $ ptext (sLit "(an enumeration consists of one or more nullary constructors)") ]
+                 -- See Note [Enumeration types] in TyCon
 
-    ------------------------------------------------------------------
-    -- data/newtype T a = ... deriving( C t1 t2 )
-    --   leads to a call to mk_eqn_help with
-    --         tycon = T, deriv_tvs = ftv(t1,t2), clas = C, tys = [t1,t2]
+cond_isProduct :: Condition
+cond_isProduct (_, rep_tc)
+  | isProductTyCon rep_tc = Nothing
+  | otherwise            = Just why
+  where
+    why = quotes (pprSourceTyCon rep_tc) <+> 
+         ptext (sLit "does not have precisely one constructor")
+
+cond_typeableOK :: Condition
+-- OK for Typeable class
+-- Currently: (a) args all of kind *
+--           (b) 7 or fewer args
+cond_typeableOK (_, rep_tc)
+  | tyConArity rep_tc > 7      = Just too_many
+  | not (all (isSubArgTypeKind . tyVarKind) (tyConTyVars rep_tc)) 
+                                = Just bad_kind
+  | isFamInstTyCon rep_tc      = Just fam_inst  -- no Typable for family insts
+  | otherwise                  = Nothing
+  where
+    too_many = quotes (pprSourceTyCon rep_tc) <+> 
+              ptext (sLit "has too many arguments")
+    bad_kind = quotes (pprSourceTyCon rep_tc) <+> 
+              ptext (sLit "has arguments of kind other than `*'")
+    fam_inst = quotes (pprSourceTyCon rep_tc) <+> 
+              ptext (sLit "is a type family")
+
+
+functorLikeClassKeys :: [Unique]
+functorLikeClassKeys = [functorClassKey, foldableClassKey, traversableClassKey]
+
+cond_functorOK :: Bool -> Condition
+-- OK for Functor/Foldable/Traversable class
+-- Currently: (a) at least one argument
+--            (b) don't use argument contravariantly
+--            (c) don't use argument in the wrong place, e.g. data T a = T (X a a)
+--            (d) optionally: don't use function types
+--            (e) no "stupid context" on data type
+cond_functorOK allowFunctions (dflags, rep_tc) 
+  | not (xopt Opt_DeriveFunctor dflags)
+  = Just (ptext (sLit "You need -XDeriveFunctor to derive an instance for this class"))
+
+  | null tc_tvs
+  = Just (ptext (sLit "Data type") <+> quotes (ppr rep_tc) 
+          <+> ptext (sLit "has no parameters"))
+
+  | not (null bad_stupid_theta)
+  = Just (ptext (sLit "Data type") <+> quotes (ppr rep_tc) 
+          <+> ptext (sLit "has a class context") <+> pprTheta bad_stupid_theta)
+
+  | otherwise
+  = msum (map check_con data_cons)     -- msum picks the first 'Just', if any
+  where
+    tc_tvs            = tyConTyVars rep_tc
+    Just (_, last_tv) = snocView tc_tvs
+    bad_stupid_theta  = filter is_bad (tyConStupidTheta rep_tc)
+    is_bad pred       = last_tv `elemVarSet` tyVarsOfPred pred
+
+    data_cons = tyConDataCons rep_tc
+    check_con con = msum (check_vanilla con : foldDataConArgs (ft_check con) con)
+
+    check_vanilla :: DataCon -> Maybe SDoc
+    check_vanilla con | isVanillaDataCon con = Nothing
+                     | otherwise            = Just (badCon con existential)
+
+    ft_check :: DataCon -> FFoldType (Maybe SDoc)
+    ft_check con = FT { ft_triv = Nothing, ft_var = Nothing
+                      , ft_co_var = Just (badCon con covariant)
+                     , ft_fun = \x y -> if allowFunctions then x `mplus` y 
+                                                           else Just (badCon con functions)
+                      , ft_tup = \_ xs  -> msum xs
+                      , ft_ty_app = \_ x   -> x
+                      , ft_bad_app = Just (badCon con wrong_arg)
+                      , ft_forall = \_ x   -> x }
+                    
+    existential = ptext (sLit "has existential arguments")
+    covariant  = ptext (sLit "uses the type variable in a function argument")
+    functions  = ptext (sLit "contains function types")
+    wrong_arg  = ptext (sLit "uses the type variable in an argument other than the last")
+
+checkFlag :: ExtensionFlag -> Condition
+checkFlag flag (dflags, _)
+  | xopt flag dflags = Nothing
+  | otherwise        = Just why
+  where
+    why = ptext (sLit "You need -X") <> text flag_str 
+          <+> ptext (sLit "to derive an instance for this class")
+    flag_str = case [ s | (s, f, _) <- xFlags, f==flag ] of
+                 [s]   -> s
+                 other -> pprPanic "checkFlag" (ppr other)
+
+std_class_via_iso :: Class -> Bool
+-- These standard classes can be derived for a newtype
+-- using the isomorphism trick *even if no -XGeneralizedNewtypeDeriving
+-- because giving so gives the same results as generating the boilerplate
+std_class_via_iso clas 
+  = classKey clas `elem` [eqClassKey, ordClassKey, ixClassKey, boundedClassKey]
+       -- Not Read/Show because they respect the type
+       -- Not Enum, because newtypes are never in Enum
+
+
+non_iso_class :: Class -> Bool
+-- *Never* derive Read,Show,Typeable,Data by isomorphism,
+-- even with -XGeneralizedNewtypeDeriving
+non_iso_class cls 
+  = classKey cls `elem` ([readClassKey, showClassKey, dataClassKey] ++
+                        typeableClassKeys)
+
+typeableClassKeys :: [Unique]
+typeableClassKeys = map getUnique typeableClassNames
+
+new_dfun_name :: Class -> TyCon -> TcM Name
+new_dfun_name clas tycon       -- Just a simple wrapper
+  = do { loc <- getSrcSpanM    -- The location of the instance decl, not of the tycon
+       ; newDFunName clas [mkTyConApp tycon []] loc }
+       -- The type passed to newDFunName is only used to generate
+       -- a suitable string; hence the empty type arg list
+
+badCon :: DataCon -> SDoc -> SDoc
+badCon con msg = ptext (sLit "Constructor") <+> quotes (ppr con) <+> msg
+\end{code}
+
+Note [Superclasses of derived instance] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In general, a derived instance decl needs the superclasses of the derived
+class too.  So if we have
+       data T a = ...deriving( Ord )
+then the initial context for Ord (T a) should include Eq (T a).  Often this is 
+redundant; we'll also generate an Ord constraint for each constructor argument,
+and that will probably generate enough constraints to make the Eq (T a) constraint 
+be satisfied too.  But not always; consider:
+
+ data S a = S
+ instance Eq (S a)
+ instance Ord (S a)
+
+ data T a = MkT (S a) deriving( Ord )
+ instance Num a => Eq (T a)
+
+The derived instance for (Ord (T a)) must have a (Num a) constraint!
+Similarly consider:
+       data T a = MkT deriving( Data, Typeable )
+Here there *is* no argument field, but we must nevertheless generate
+a context for the Data instances:
+       instance Typable a => Data (T a) where ...
+
+
+%************************************************************************
+%*                                                                     *
+               Deriving newtypes
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+mkNewTypeEqn :: CtOrigin -> DynFlags -> [Var] -> Class
+             -> [Type] -> TyCon -> [Type] -> TyCon -> [Type]
+             -> DerivContext
+             -> TcRn EarlyDerivSpec
+mkNewTypeEqn orig dflags tvs
+             cls cls_tys tycon tc_args rep_tycon rep_tc_args mtheta
+-- Want: instance (...) => cls (cls_tys ++ [tycon tc_args]) where ...
+  | can_derive_via_isomorphism && (newtype_deriving || std_class_via_iso cls)
+  = do { traceTc "newtype deriving:" (ppr tycon <+> ppr rep_tys <+> ppr all_preds)
+       ; dfun_name <- new_dfun_name cls tycon
+       ; loc <- getSrcSpanM
+       ; let spec = DS { ds_loc = loc, ds_orig = orig
+                       , ds_name = dfun_name, ds_tvs = varSetElems dfun_tvs 
+                       , ds_cls = cls, ds_tys = inst_tys
+                       , ds_tc = rep_tycon, ds_tc_args = rep_tc_args
+                       , ds_theta =  mtheta `orElse` all_preds
+                       , ds_newtype = True }
+       ; return (if isJust mtheta then Right spec
+                                  else Left spec) }
+
+  | otherwise
+  = case checkSideConditions dflags mtheta cls cls_tys rep_tycon of
+      CanDerive -> go_for_it   -- Use the standard H98 method
+      DerivableClassError msg  -- Error with standard class
+        | can_derive_via_isomorphism -> bale_out (msg $$ suggest_nd)
+        | otherwise                  -> bale_out msg
+      NonDerivableClass        -- Must use newtype deriving
+       | newtype_deriving           -> bale_out cant_derive_err  -- Too hard, even with newtype deriving
+        | can_derive_via_isomorphism -> bale_out (non_std $$ suggest_nd) -- Try newtype deriving!
+       | otherwise                  -> bale_out non_std
+  where
+        newtype_deriving = xopt Opt_GeneralizedNewtypeDeriving dflags
+        go_for_it        = mk_data_eqn orig tvs cls tycon tc_args rep_tycon rep_tc_args mtheta
+       bale_out msg     = failWithTc (derivingThingErr newtype_deriving cls cls_tys inst_ty msg)
+
+       non_std    = nonStdErr cls
+        suggest_nd = ptext (sLit "Try -XGeneralizedNewtypeDeriving for GHC's newtype-deriving extension")
 
-    mk_eqn_help loc orig gla_exts DataType tycon deriv_tvs clas tys
-      | Just err <- checkSideConditions gla_exts tycon deriv_tvs clas tys
-      = bale_out (derivingThingErr clas tys origTyCon ttys err)
-      | otherwise 
-      = do { eqn <- mkDataTypeEqn loc orig tycon clas
-          ; returnM (Just eqn, Nothing) }
-      where
-        (origTyCon, ttys) = tyConOrigHead tycon
-
-    mk_eqn_help loc orig gla_exts NewType tycon deriv_tvs clas tys
-      | can_derive_via_isomorphism && (gla_exts || std_class_via_iso clas)
-      =        do { traceTc (text "newtype deriving:" <+> ppr tycon <+> ppr rep_tys)
-          ;    -- Go ahead and use the isomorphism
-            dfun_name <- new_dfun_name clas tycon
-          ; return (Nothing, Just (InstInfo { iSpec  = mk_inst_spec dfun_name,
-                                              iBinds = NewTypeDerived ntd_info })) }
-      | std_class gla_exts clas
-      = mk_eqn_help loc orig gla_exts DataType tycon deriv_tvs clas tys        -- Go via bale-out route
-
-      | otherwise                              -- Non-standard instance
-      = bale_out (if gla_exts then     
-                       cant_derive_err -- Too hard
-                 else
-                       non_std_err)    -- Just complain about being a non-std instance
-      where
        -- Here is the plan for newtype derivings.  We see
        --        newtype T a1...an = MkT (t ak+1...an) deriving (.., C s1 .. sm, ...)
        -- where t is a type,
-       --       ak+1...an is a suffix of a1..an
+       --       ak+1...an is a suffix of a1..an, and are all tyars
        --       ak+1...an do not occur free in t, nor in the s1..sm
        --       (C s1 ... sm) is a  *partial applications* of class C 
        --                      with the last parameter missing
        --       (T a1 .. ak) matches the kind of C's last argument
        --              (and hence so does t)
+       -- The latter kind-check has been done by deriveTyData already,
+       -- and tc_args are already trimmed
        --
        -- We generate the instance
        --       instance forall ({a1..ak} u fvs(s1..sm)).
@@ -470,57 +1109,38 @@ makeDerivEqns overlap_flag tycl_decls deriv_decls
        -- We generate the instance
        --      instance Monad (ST s) => Monad (T s) where 
 
-       clas_tyvars = classTyVars clas
-       kind = tyVarKind (last clas_tyvars)
-               -- Kind of the thing we want to instance
-               --   e.g. argument kind of Monad, *->*
-
-       (arg_kinds, _) = splitKindFunTys kind
-       n_args_to_drop = length arg_kinds       
-               -- Want to drop 1 arg from (T s a) and (ST s a)
-               -- to get       instance Monad (ST s) => Monad (T s)
-
-       -- Note [newtype representation]
-       -- Need newTyConRhs *not* newTyConRep to get the representation 
-       -- type, because the latter looks through all intermediate newtypes
-       -- For example
+       nt_eta_arity = length (fst (newTyConEtadRhs rep_tycon))
+               -- For newtype T a b = MkT (S a a b), the TyCon machinery already
+               -- eta-reduces the representation type, so we know that
+               --      T a ~ S a a
+               -- That's convenient here, because we may have to apply
+               -- it to fewer than its original complement of arguments
+
+       -- Note [Newtype representation]
+       -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+       -- Need newTyConRhs (*not* a recursive representation finder) 
+       -- to get the representation type. For example
        --      newtype B = MkB Int
        --      newtype A = MkA B deriving( Num )
        -- We want the Num instance of B, *not* the Num instance of Int,
        -- when making the Num instance of A!
-        (tc_tvs, rep_ty)      = newTyConRhs tycon
-       (rep_fn, rep_ty_args) = tcSplitAppTys rep_ty
-
-       n_tyvars_to_keep = tyConArity tycon - n_args_to_drop
-       tyvars_to_drop   = drop n_tyvars_to_keep tc_tvs
-       tyvars_to_keep   = take n_tyvars_to_keep tc_tvs
-
-       n_args_to_keep = length rep_ty_args - n_args_to_drop
-       args_to_drop   = drop n_args_to_keep rep_ty_args
-       args_to_keep   = take n_args_to_keep rep_ty_args
-
-       rep_fn'  = mkAppTys rep_fn args_to_keep
-       rep_tys  = tys ++ [rep_fn']
-       rep_pred = mkClassPred clas rep_tys
+       rep_inst_ty = newTyConInstRhs rep_tycon rep_tc_args
+       rep_tys     = cls_tys ++ [rep_inst_ty]
+       rep_pred    = mkClassPred cls rep_tys
                -- rep_pred is the representation dictionary, from where
                -- we are gong to get all the methods for the newtype
                -- dictionary 
 
-        -- To account for newtype family instance, we need to get the family
-        -- tycon and its index types when costructing the type at which we
-        -- construct the class instance.  The dropped class parameters must of
-        -- course all be variables (not more complex indexes).
-       --
-       origHead = let
-                     (origTyCon, tyArgs) = tyConOrigHead tycon
-                   in mkTyConApp origTyCon (take n_tyvars_to_keep tyArgs)
 
-        -- Next we figure out what superclass dictionaries to use
-        -- See Note [Newtype deriving superclasses] above
+    -- Next we figure out what superclass dictionaries to use
+    -- See Note [Newtype deriving superclasses] above
 
-       inst_tys = tys ++ [origHead]
-       sc_theta = substTheta (zipOpenTvSubst clas_tyvars inst_tys)
-                             (classSCTheta clas)
+       cls_tyvars = classTyVars cls
+       dfun_tvs = tyVarsOfTypes inst_tys
+       inst_ty = mkTyConApp tycon tc_args
+       inst_tys = cls_tys ++ [inst_ty]
+       sc_theta = substTheta (zipOpenTvSubst cls_tyvars inst_tys)
+                             (classSCTheta cls)
 
                -- If there are no tyvars, there's no need
                -- to abstract over the dictionaries we need
@@ -529,234 +1149,60 @@ makeDerivEqns overlap_flag tycl_decls deriv_decls
                --              instance C T
                -- rather than
                --              instance C Int => C T
-       dict_tvs = deriv_tvs ++ tyvars_to_keep
        all_preds = rep_pred : sc_theta         -- NB: rep_pred comes first
-       (dict_args, ntd_info) | null dict_tvs = ([], Just all_preds)
-                             | otherwise     = (all_preds, Nothing)
-
-               -- Finally! Here's where we build the dictionary Id
-       mk_inst_spec dfun_name = mkLocalInstance dfun overlap_flag
-         where
-           dfun = mkDictFunId dfun_name dict_tvs dict_args clas inst_tys
 
        -------------------------------------------------------------------
        --  Figuring out whether we can only do this newtype-deriving thing
 
-       right_arity = length tys + 1 == classArity clas
-
-               -- Never derive Read,Show,Typeable,Data this way 
-       non_iso_classes = [readClassKey, showClassKey, typeableClassKey, dataClassKey]
        can_derive_via_isomorphism
-          =  not (getUnique clas `elem` non_iso_classes)
-          && right_arity                       -- Well kinded;
-                                               -- eg not: newtype T ... deriving( ST )
-                                               --      because ST needs *2* type params
-          && n_tyvars_to_keep >= 0             -- Type constructor has right kind:
-                                               -- eg not: newtype T = T Int deriving( Monad )
-          && n_args_to_keep   >= 0             -- Rep type has right kind: 
-                                               -- eg not: newtype T a = T Int deriving( Monad )
-          && eta_ok                            -- Eta reduction works
-          && not (isRecursiveTyCon tycon)      -- Does not work for recursive tycons:
-                                               --      newtype A = MkA [A]
-                                               -- Don't want
-                                               --      instance Eq [A] => Eq A !!
-                       -- Here's a recursive newtype that's actually OK
-                       --      newtype S1 = S1 [T1 ()]
-                       --      newtype T1 a = T1 (StateT S1 IO a ) deriving( Monad )
-                       -- It's currently rejected.  Oh well.
-                       -- In fact we generate an instance decl that has method of form
-                       --      meth @ instTy = meth @ repTy
-                       -- (no coerce's).  We'd need a coerce if we wanted to handle
-                       -- recursive newtypes too
-
-       -- Check that eta reduction is OK
-       --      (a) the dropped-off args are identical
-       --      (b) the remaining type args do not mention any of teh dropped
-       --          type variables 
-       --      (c) the type class args do not mention any of teh dropped type
-       --          variables 
-       --      (d) in case of newtype family instances, the eta-dropped
-       --          arguments must be type variables (not more complex indexes)
-       dropped_tvs = mkVarSet tyvars_to_drop
-       eta_ok = (args_to_drop `tcEqTypes` mkTyVarTys tyvars_to_drop)
-             && (tyVarsOfType rep_fn' `disjointVarSet` dropped_tvs)
-             && (tyVarsOfTypes tys    `disjointVarSet` dropped_tvs)
-             && droppedIndexesAreVariables
-
-        droppedIndexesAreVariables = 
-         case tyConFamInst_maybe tycon of
-           Nothing                 -> True
-           Just (famTyCon, tyIdxs) -> 
-             all isTyVarTy $ drop (tyConArity famTyCon - n_args_to_drop) tyIdxs
-
-       cant_derive_err = derivingThingErr clas tys tycon (mkTyVarTys tyvars_to_keep)
-                               (vcat [ptext SLIT("even with cunning newtype deriving:"),
-                                       if isRecursiveTyCon tycon then
-                                         ptext SLIT("the newtype is recursive")
-                                       else empty,
-                                       if not right_arity then 
-                                         quotes (ppr (mkClassPred clas tys)) <+> ptext SLIT("does not have arity 1")
-                                       else empty,
-                                       if not (n_tyvars_to_keep >= 0) then 
-                                         ptext SLIT("the type constructor has wrong kind")
-                                       else if not (n_args_to_keep >= 0) then
-                                         ptext SLIT("the representation type has wrong kind")
-                                       else if not eta_ok then 
-                                         ptext SLIT("the eta-reduction property does not hold")
-                                       else empty
-                                     ])
-
-       non_std_err = derivingThingErr clas tys tycon (mkTyVarTys tyvars_to_keep)
-                               (vcat [non_std_why clas,
-                                      ptext SLIT("Try -fglasgow-exts for GHC's newtype-deriving extension")])
-
-    bale_out err = addErrTc err `thenM_` returnM (Nothing, Nothing) 
-
-std_class gla_exts clas 
-  =  key `elem` derivableClassKeys
-  || (gla_exts && (key == typeableClassKey || key == dataClassKey))
-  where
-     key = classKey clas
-    
-std_class_via_iso clas -- These standard classes can be derived for a newtype
-                       -- using the isomorphism trick *even if no -fglasgow-exts*
-  = classKey clas `elem`  [eqClassKey, ordClassKey, ixClassKey, boundedClassKey]
-       -- Not Read/Show because they respect the type
-       -- Not Enum, becuase newtypes are never in Enum
-
-
-new_dfun_name clas tycon       -- Just a simple wrapper
-  = newDFunName clas [mkTyConApp tycon []] (getSrcLoc tycon)
-       -- The type passed to newDFunName is only used to generate
-       -- a suitable string; hence the empty type arg list
-
-------------------------------------------------------------------
-mkDataTypeEqn :: SrcSpan -> InstOrigin -> TyCon -> Class -> TcM DerivEqn
-mkDataTypeEqn loc orig tycon clas
-  | clas `hasKey` typeableClassKey
-  =    -- The Typeable class is special in several ways
-       --        data T a b = ... deriving( Typeable )
-       -- gives
-       --        instance Typeable2 T where ...
-       -- Notice that:
-       -- 1. There are no constraints in the instance
-       -- 2. There are no type variables either
-       -- 3. The actual class we want to generate isn't necessarily
-       --      Typeable; it depends on the arity of the type
-    do { real_clas <- tcLookupClass (typeableClassNames !! tyConArity tycon)
-       ; dfun_name <- new_dfun_name real_clas tycon
-       ; return (loc, orig, dfun_name, real_clas, tycon, [], []) }
+          =  not (non_iso_class cls)
+          && arity_ok
+          && eta_ok
+          && ats_ok
+--        && not (isRecursiveTyCon tycon)      -- Note [Recursive newtypes]
 
-  | otherwise
-  = do { dfun_name <- new_dfun_name clas tycon
-       ; return (loc, orig, dfun_name, clas, tycon, tyvars, constraints)
-       }
-  where
-    tyvars            = tyConTyVars tycon
-    constraints       = extra_constraints ++ ordinary_constraints
-    extra_constraints = tyConStupidTheta tycon
-        -- "extra_constraints": see note [Data decl contexts] above
+       arity_ok = length cls_tys + 1 == classArity cls
+               -- Well kinded; eg not: newtype T ... deriving( ST )
+               --                      because ST needs *2* type params
 
-    ordinary_constraints
-      = [ mkClassPred clas [arg_ty] 
-        | data_con <- tyConDataCons tycon,
-          arg_ty <- dataConInstOrigArgTys data_con (mkTyVarTys tyvars),
-          not (isUnLiftedType arg_ty)  -- No constraints for unlifted types?
-        ]
-
-
-------------------------------------------------------------------
--- Check side conditions that dis-allow derivability for particular classes
--- This is *apart* from the newtype-deriving mechanism
-
-checkSideConditions :: Bool -> TyCon -> [TyVar] -> Class -> [TcType] -> Maybe SDoc
-checkSideConditions gla_exts tycon deriv_tvs clas tys
-  | notNull deriv_tvs || notNull tys   
-  = Just ty_args_why   -- e.g. deriving( Foo s )
-  | otherwise
-  = case [cond | (key,cond) <- sideConditions, key == getUnique clas] of
-       []     -> Just (non_std_why clas)
-       [cond] -> cond (gla_exts, tycon)
-       other  -> pprPanic "checkSideConditions" (ppr clas)
-  where
-    ty_args_why        = quotes (ppr (mkClassPred clas tys)) <+> ptext SLIT("is not a class")
-
-non_std_why clas = quotes (ppr clas) <+> ptext SLIT("is not a derivable class")
-
-sideConditions :: [(Unique, Condition)]
-sideConditions
-  = [  (eqClassKey,       cond_std),
-       (ordClassKey,      cond_std),
-       (readClassKey,     cond_std),
-       (showClassKey,     cond_std),
-       (enumClassKey,     cond_std `andCond` cond_isEnumeration),
-       (ixClassKey,       cond_std `andCond` (cond_isEnumeration `orCond` cond_isProduct)),
-       (boundedClassKey,  cond_std `andCond` (cond_isEnumeration `orCond` cond_isProduct)),
-       (typeableClassKey, cond_glaExts `andCond` cond_typeableOK),
-       (dataClassKey,     cond_glaExts `andCond` cond_std)
-    ]
-
-type Condition = (Bool, TyCon) -> Maybe SDoc   -- Nothing => OK
-
-orCond :: Condition -> Condition -> Condition
-orCond c1 c2 tc 
-  = case c1 tc of
-       Nothing -> Nothing              -- c1 succeeds
-       Just x  -> case c2 tc of        -- c1 fails
-                    Nothing -> Nothing
-                    Just y  -> Just (x $$ ptext SLIT("  and") $$ y)
-                                       -- Both fail
-
-andCond c1 c2 tc = case c1 tc of
-                    Nothing -> c2 tc   -- c1 succeeds
-                    Just x  -> Just x  -- c1 fails
+       -- Check that eta reduction is OK
+       eta_ok = nt_eta_arity <= length rep_tc_args
+               -- The newtype can be eta-reduced to match the number
+               --     of type argument actually supplied
+               --        newtype T a b = MkT (S [a] b) deriving( Monad )
+               --     Here the 'b' must be the same in the rep type (S [a] b)
+               --     And the [a] must not mention 'b'.  That's all handled
+               --     by nt_eta_rity.
+
+       ats_ok = null (classATs cls)    
+              -- No associated types for the class, because we don't 
+              -- currently generate type 'instance' decls; and cannot do
+              -- so for 'data' instance decls
+                                        
+       cant_derive_err
+          = vcat [ ppUnless arity_ok arity_msg
+                 , ppUnless eta_ok eta_msg
+                 , ppUnless ats_ok ats_msg ]
+        arity_msg = quotes (ppr (mkClassPred cls cls_tys)) <+> ptext (sLit "does not have arity 1")
+       eta_msg   = ptext (sLit "cannot eta-reduce the representation type enough")
+       ats_msg   = ptext (sLit "the class has associated types")
+\end{code}
 
-cond_std :: Condition
-cond_std (gla_exts, tycon)
-  | any (not . isVanillaDataCon) data_cons = Just existential_why     
-  | null data_cons                        = Just no_cons_why
-  | otherwise                             = Nothing
-  where
-    data_cons       = tyConDataCons tycon
-    no_cons_why            = quotes (ppr tycon) <+> ptext SLIT("has no data constructors")
-    existential_why = quotes (ppr tycon) <+> ptext SLIT("has non-Haskell-98 constructor(s)")
-  
-cond_isEnumeration :: Condition
-cond_isEnumeration (gla_exts, tycon)
-  | isEnumerationTyCon tycon = Nothing
-  | otherwise               = Just why
-  where
-    why = quotes (ppr tycon) <+> ptext SLIT("has non-nullary constructors")
+Note [Recursive newtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Newtype deriving works fine, even if the newtype is recursive.
+e.g.   newtype S1 = S1 [T1 ()]
+       newtype T1 a = T1 (StateT S1 IO a ) deriving( Monad )
+Remember, too, that type families are curretly (conservatively) given
+a recursive flag, so this also allows newtype deriving to work
+for type famillies.
 
-cond_isProduct :: Condition
-cond_isProduct (gla_exts, tycon)
-  | isProductTyCon tycon = Nothing
-  | otherwise           = Just why
-  where
-    why = quotes (ppr tycon) <+> ptext SLIT("has more than one constructor")
+We used to exclude recursive types, because we had a rather simple
+minded way of generating the instance decl:
+   newtype A = MkA [A]
+   instance Eq [A] => Eq A     -- Makes typechecker loop!
+But now we require a simple context, so it's ok.
 
-cond_typeableOK :: Condition
--- OK for Typeable class
--- Currently: (a) args all of kind *
---           (b) 7 or fewer args
-cond_typeableOK (gla_exts, tycon)
-  | tyConArity tycon > 7       = Just too_many
-  | not (all (isSubArgTypeKind . tyVarKind) (tyConTyVars tycon)) 
-                                = Just bad_kind
-  | isFamInstTyCon tycon       = Just fam_inst  -- no Typable for family insts
-  | otherwise                  = Nothing
-  where
-    too_many = quotes (ppr tycon) <+> ptext SLIT("has too many arguments")
-    bad_kind = quotes (ppr tycon) <+> 
-              ptext SLIT("has arguments of kind other than `*'")
-    fam_inst = quotes (ppr tycon) <+> ptext SLIT("is a type family")
-
-cond_glaExts :: Condition
-cond_glaExts (gla_exts, tycon) | gla_exts  = Nothing
-                              | otherwise = Just why
-  where
-    why  = ptext SLIT("You need -fglasgow-exts to derive an instance for this class")
-\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -779,69 +1225,88 @@ ordered by sorting on type varible, tv, (major key) and then class, k,
 \end{itemize}
 
 \begin{code}
-solveDerivEqns :: OverlapFlag
-              -> [DerivEqn]
-              -> TcM [Instance]-- Solns in same order as eqns.
-                               -- This bunch is Absolutely minimal...
+inferInstanceContexts :: OverlapFlag -> [DerivSpec] -> TcM [DerivSpec]
+
+inferInstanceContexts _ [] = return []
 
-solveDerivEqns overlap_flag orig_eqns
-  = iterateDeriv 1 initial_solutions
+inferInstanceContexts oflag infer_specs
+  = do { traceTc "inferInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
+       ; iterate_deriv 1 initial_solutions }
   where
+    ------------------------------------------------------------------
        -- The initial solutions for the equations claim that each
        -- instance has an empty context; this solution is certainly
        -- in canonical form.
-    initial_solutions :: [DerivSoln]
-    initial_solutions = [ [] | _ <- orig_eqns ]
+    initial_solutions :: [ThetaType]
+    initial_solutions = [ [] | _ <- infer_specs ]
 
     ------------------------------------------------------------------
-       -- iterateDeriv calculates the next batch of solutions,
+       -- iterate_deriv calculates the next batch of solutions,
        -- compares it with the current one; finishes if they are the
        -- same, otherwise recurses with the new solutions.
        -- It fails if any iteration fails
-    iterateDeriv :: Int -> [DerivSoln] -> TcM [Instance]
-    iterateDeriv n current_solns
+    iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec]
+    iterate_deriv n current_solns
       | n > 20         -- Looks as if we are in an infinite loop
-               -- This can happen if we have -fallow-undecidable-instances
+               -- This can happen if we have -XUndecidableInstances
                -- (See TcSimplify.tcSimplifyDeriv.)
       = pprPanic "solveDerivEqns: probable loop" 
-                (vcat (map pprDerivEqn orig_eqns) $$ ppr current_solns)
+                (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns)
       | otherwise
-      =        let 
-           inst_specs = zipWithEqual "add_solns" mk_inst_spec 
-                                     orig_eqns current_solns
-        in
-        checkNoErrs (
-                 -- Extend the inst info from the explicit instance decls
+      =        do {      -- Extend the inst info from the explicit instance decls
                  -- with the current set of solutions, and simplify each RHS
-           extendLocalInstEnv inst_specs $
-           mappM gen_soln orig_eqns
-       )                               `thenM` \ new_solns ->
-       if (current_solns == new_solns) then
-           returnM inst_specs
-       else
-           iterateDeriv (n+1) new_solns
+            let inst_specs = zipWithEqual "add_solns" (mkInstance oflag)
+                                          current_solns infer_specs
+          ; new_solns <- checkNoErrs $
+                         extendLocalInstEnv inst_specs $
+                         mapM gen_soln infer_specs
+
+          ; if (current_solns == new_solns) then
+               return [ spec { ds_theta = soln } 
+                       | (spec, soln) <- zip infer_specs current_solns ]
+            else
+               iterate_deriv (n+1) new_solns }
 
     ------------------------------------------------------------------
-    gen_soln :: DerivEqn -> TcM [PredType]
-    gen_soln (loc, orig, _, clas, tc, tyvars, deriv_rhs)
+    gen_soln :: DerivSpec  -> TcM [PredType]
+    gen_soln (DS { ds_loc = loc, ds_orig = orig, ds_tvs = tyvars 
+                , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
       = setSrcSpan loc $
-       do { let inst_tys = [origHead]
-          ; theta <- addErrCtxt (derivInstCtxt1 clas inst_tys) $
-                     tcSimplifyDeriv orig tc tyvars deriv_rhs
+       addErrCtxt (derivInstCtxt clas inst_tys) $ 
+       do {      -- 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.  Moreover, simplifyDeriv
+                 -- has an assert failure because it finds a TyVar when it expects
+                 -- only TcTyVars.  So I just rule it out for now.  I'm not 
+                 -- even sure how it can arise.
+                 
+          ; let tv_set = mkVarSet tyvars
+                weird_preds = [pred | pred <- deriv_rhs
+                                     , not (tyVarsOfPred pred `subVarSet` tv_set)]  
+          ; mapM_ (addErrTc . badDerivedPred) weird_preds      
+
+           ; theta <- simplifyDeriv orig tyvars deriv_rhs
+               -- checkValidInstance tyvars theta clas inst_tys
+               -- Not necessary; see Note [Exotic derived instance contexts]
+               --                in TcSimplify
+               
+           ; traceTc "TcDeriv" (ppr deriv_rhs $$ ppr theta)
                -- Claim: the result instance declaration is guaranteed valid
                -- Hence no need to call:
                --   checkValidInstance tyvars theta clas inst_tys
           ; return (sortLe (<=) theta) }       -- Canonicalise before returning the solution
-      where
-         origHead = uncurry mkTyConApp (tyConOrigHead tc)      
 
-    ------------------------------------------------------------------
-    mk_inst_spec :: DerivEqn -> DerivSoln -> Instance
-    mk_inst_spec (loc, orig, dfun_name, clas, tycon, tyvars, _) theta
-       = mkLocalInstance dfun overlap_flag
-       where
-         dfun     = mkDictFunId dfun_name tyvars theta clas [origHead]
-         origHead = uncurry mkTyConApp (tyConOrigHead tycon)
+------------------------------------------------------------------
+mkInstance :: OverlapFlag -> ThetaType -> DerivSpec -> Instance
+mkInstance overlap_flag theta
+           (DS { ds_name = dfun_name
+               , ds_tvs = tyvars, ds_cls = clas, ds_tys = tys })
+  = mkLocalInstance dfun overlap_flag
+  where
+    dfun = mkDictFunId dfun_name tyvars theta clas tys
+
 
 extendLocalInstEnv :: [Instance] -> TcM a -> TcM a
 -- Add new locally-defined instances; don't bother to check
@@ -853,6 +1318,7 @@ extendLocalInstEnv dfuns thing_inside
       ; setGblEnv env' thing_inside }
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection[TcDeriv-normal-binds]{Bindings for the various classes}
@@ -923,60 +1389,70 @@ the renamer.  What a great hack!
 -- Representation tycons differ from the tycon in the instance signature in
 -- case of instances for indexed families.
 --
-genInst :: Instance -> TcM ((InstInfo, TyCon), LHsBinds RdrName)
-genInst spec
-  = do { fix_env <- getFixityEnv
-       ; let
-           (tyvars,_,clas,[ty])    = instanceHead spec
-           clas_nm                 = className clas
-           (visible_tycon, tyArgs) = tcSplitTyConApp ty 
+genInst :: Bool        -- True <=> standalone deriving
+       -> OverlapFlag
+        -> DerivSpec -> TcM (InstInfo RdrName, DerivAuxBinds)
+genInst standalone_deriv oflag spec
+  | ds_newtype spec
+  = return (InstInfo { iSpec  = mkInstance oflag (ds_theta spec) spec
+                    , iBinds = NewTypeDerived co rep_tycon }, [])
+
+  | otherwise
+  = do { let loc  = getSrcSpan (ds_name spec)
+             inst = mkInstance oflag (ds_theta spec) spec
+             clas = ds_cls spec
 
           -- In case of a family instance, we need to use the representation
-          -- tycon (after all it has the data constructors)
-        ; tycon <- if isOpenTyCon visible_tycon
-                  then tcLookupFamInst visible_tycon tyArgs
-                  else return visible_tycon
-       ; let (meth_binds, aux_binds) = genDerivBinds clas fix_env tycon
-
-       -- Bring the right type variables into 
-       -- scope, and rename the method binds
-       -- It's a bit yukky that we return *renamed* InstInfo, but
-       -- *non-renamed* auxiliary bindings
-       ; (rn_meth_binds, _fvs) <- discardWarnings $ 
-                                  bindLocalNames (map Var.varName tyvars) $
-                                  rnMethodBinds clas_nm (\n -> []) [] meth_binds
-
-       -- Build the InstInfo
-       ; return ((InstInfo { iSpec = spec, 
-                             iBinds = VanillaInst rn_meth_binds [] }, tycon),
-                 aux_binds)
+          -- tycon (after all, it has the data constructors)
+       ; fix_env <- getFixityEnv
+       ; let (meth_binds, aux_binds) = genDerivBinds loc fix_env clas rep_tycon
+             binds = VanillaInst meth_binds [] standalone_deriv
+       ; return (InstInfo { iSpec = inst, iBinds = binds }, aux_binds)
         }
-
-genDerivBinds clas fix_env tycon
+  where
+    rep_tycon   = ds_tc spec
+    rep_tc_args = ds_tc_args spec
+    co1 = case tyConFamilyCoercion_maybe rep_tycon of
+             Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
+             Nothing     -> id_co
+             -- Not a family => rep_tycon = main tycon
+    co2 = case newTyConCo_maybe rep_tycon of
+             Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
+              Nothing     -> id_co  -- The newtype is transparent; no need for a cast
+    co = co1 `mkTransCoI` co2
+    id_co = IdCo (mkTyConApp rep_tycon rep_tc_args)
+
+-- Example: newtype instance N [a] = N1 (Tree a) 
+--          deriving instance Eq b => Eq (N [(b,b)])
+-- From the instance, we get an implicit newtype R1:N a = N1 (Tree a)
+-- When dealing with the deriving clause
+--    co1 : N [(b,b)] ~ R1:N (b,b)
+--    co2 : R1:N (b,b) ~ Tree (b,b)
+--    co  : N [(b,b)] ~ Tree (b,b)
+
+genDerivBinds :: SrcSpan -> FixityEnv -> Class -> TyCon -> (LHsBinds RdrName, DerivAuxBinds)
+genDerivBinds loc fix_env clas tycon
   | className clas `elem` typeableClassNames
-  = (gen_Typeable_binds tycon, emptyLHsBinds)
+  = (gen_Typeable_binds loc tycon, [])
 
   | otherwise
   = case assocMaybe gen_list (getUnique clas) of
-       Just gen_fn -> gen_fn fix_env tycon
+       Just gen_fn -> gen_fn loc tycon
        Nothing     -> pprPanic "genDerivBinds: bad derived class" (ppr clas)
   where
-    gen_list :: [(Unique, FixityEnv -> TyCon -> (LHsBinds RdrName, LHsBinds RdrName))]
-    gen_list = [(eqClassKey,      no_aux_binds (ignore_fix_env gen_Eq_binds))
-              ,(ordClassKey,     no_aux_binds (ignore_fix_env gen_Ord_binds))
-              ,(enumClassKey,    no_aux_binds (ignore_fix_env gen_Enum_binds))
-              ,(boundedClassKey, no_aux_binds (ignore_fix_env gen_Bounded_binds))
-              ,(ixClassKey,      no_aux_binds (ignore_fix_env gen_Ix_binds))
-              ,(typeableClassKey,no_aux_binds (ignore_fix_env gen_Typeable_binds))
-              ,(showClassKey,    no_aux_binds gen_Show_binds)
-              ,(readClassKey,    no_aux_binds gen_Read_binds)
-              ,(dataClassKey,    gen_Data_binds)
+    gen_list :: [(Unique, SrcSpan -> TyCon -> (LHsBinds RdrName, DerivAuxBinds))]
+    gen_list = [(eqClassKey,       gen_Eq_binds)
+              ,(ordClassKey,      gen_Ord_binds)
+              ,(enumClassKey,     gen_Enum_binds)
+              ,(boundedClassKey,  gen_Bounded_binds)
+              ,(ixClassKey,       gen_Ix_binds)
+              ,(showClassKey,     gen_Show_binds fix_env)
+              ,(readClassKey,     gen_Read_binds fix_env)
+              ,(dataClassKey,     gen_Data_binds)
+              ,(functorClassKey,  gen_Functor_binds)
+              ,(foldableClassKey, gen_Foldable_binds)
+              ,(traversableClassKey, gen_Traversable_binds)
               ]
-
-      -- no_aux_binds is used for generators that don't 
-      -- need to produce any auxiliary bindings
-    no_aux_binds f fix_env tc = (f fix_env tc, emptyLHsBinds)
-    ignore_fix_env f fix_env tc = f tc
 \end{code}
 
 
@@ -986,97 +1462,52 @@ genDerivBinds clas fix_env tycon
 %*                                                                     *
 %************************************************************************
 
-
-data Foo ... = ...
-
-con2tag_Foo :: Foo ... -> Int#
-tag2con_Foo :: Int -> Foo ...  -- easier if Int, not Int#
-maxtag_Foo  :: Int             -- ditto (NB: not unlifted)
-
-
-We have a @con2tag@ function for a tycon if:
-\begin{itemize}
-\item
-We're deriving @Eq@ and the tycon has nullary data constructors.
-
-\item
-Or: we're deriving @Ord@ (unless single-constructor), @Enum@, @Ix@
-(enum type only????)
-\end{itemize}
-
-We have a @tag2con@ function for a tycon if:
-\begin{itemize}
-\item
-We're deriving @Enum@, or @Ix@ (enum type only???)
-\end{itemize}
-
-If we have a @tag2con@ function, we also generate a @maxtag@ constant.
-
-\begin{code}
-genTaggeryBinds :: [(InstInfo, TyCon)] -> TcM (LHsBinds RdrName)
-genTaggeryBinds infos
-  = do { names_so_far <- foldlM do_con2tag []           tycons_of_interest
-       ; nm_alist_etc <- foldlM do_tag2con names_so_far tycons_of_interest
-       ; return (listToBag (map gen_tag_n_con_monobind nm_alist_etc)) }
-  where
-    all_CTs                 = [ (fst (simpleInstInfoClsTy info), tc) 
-                             | (info, tc) <- infos]
-    all_tycons             = map snd all_CTs
-    (tycons_of_interest, _) = removeDups compare all_tycons
-    
-    do_con2tag acc_Names tycon
-      | isDataTyCon tycon &&
-        ((we_are_deriving eqClassKey tycon
-           && any isNullarySrcDataCon (tyConDataCons tycon))
-        || (we_are_deriving ordClassKey  tycon
-           && not (isProductTyCon tycon))
-        || (we_are_deriving enumClassKey tycon)
-        || (we_are_deriving ixClassKey   tycon))
-       
-      = returnM ((con2tag_RDR tycon, tycon, GenCon2Tag)
-                  : acc_Names)
-      | otherwise
-      = returnM acc_Names
-
-    do_tag2con acc_Names tycon
-      | isDataTyCon tycon &&
-         (we_are_deriving enumClassKey tycon ||
-         we_are_deriving ixClassKey   tycon
-         && isEnumerationTyCon tycon)
-      = returnM ( (tag2con_RDR tycon, tycon, GenTag2Con)
-                : (maxtag_RDR  tycon, tycon, GenMaxTag)
-                : acc_Names)
-      | otherwise
-      = returnM acc_Names
-
-    we_are_deriving clas_key tycon
-      = is_in_eqns clas_key tycon all_CTs
-      where
-       is_in_eqns clas_key tycon [] = False
-       is_in_eqns clas_key tycon ((c,t):cts)
-         =  (clas_key == classKey c && tycon == t)
-         || is_in_eqns clas_key tycon cts
-\end{code}
-
 \begin{code}
-derivingThingErr clas tys tycon ttys why
-  = sep [hsep [ptext SLIT("Can't make a derived instance of"), 
-              quotes (ppr pred)],
-        nest 2 (parens why)]
-  where
-    pred = mkClassPred clas (tys ++ [mkTyConApp tycon ttys])
-
-derivCtxt :: Name -> Maybe [LHsType Name] -> SDoc
-derivCtxt tycon mb_tys
-  = ptext SLIT("When deriving instances for") <+> quotes typeInst
+derivingKindErr :: TyCon -> Class -> [Type] -> Kind -> Message
+derivingKindErr tc cls cls_tys cls_kind
+  = hang (ptext (sLit "Cannot derive well-kinded instance of form")
+               <+> quotes (pprClassPred cls cls_tys <+> parens (ppr tc <+> ptext (sLit "..."))))
+       2 (ptext (sLit "Class") <+> quotes (ppr cls)
+           <+> ptext (sLit "expects an argument of kind") <+> quotes (pprKind cls_kind))
+
+derivingEtaErr :: Class -> [Type] -> Type -> Message
+derivingEtaErr cls cls_tys inst_ty
+  = sep [ptext (sLit "Cannot eta-reduce to an instance of form"),
+        nest 2 (ptext (sLit "instance (...) =>")
+               <+> pprClassPred cls (cls_tys ++ [inst_ty]))]
+
+typeFamilyPapErr :: TyCon -> Class -> [Type] -> Type -> Message
+typeFamilyPapErr tc cls cls_tys inst_ty
+  = hang (ptext (sLit "Derived instance") <+> quotes (pprClassPred cls (cls_tys ++ [inst_ty])))
+       2 (ptext (sLit "requires illegal partial application of data type family") <+> ppr tc) 
+
+derivingThingErr :: Bool -> Class -> [Type] -> Type -> Message -> Message
+derivingThingErr newtype_deriving clas tys ty why
+  = sep [(hang (ptext (sLit "Can't make a derived instance of"))
+            2 (quotes (ppr pred)) 
+          $$ nest 2 extra) <> colon,
+        nest 2 why]
   where
-    typeInst = case mb_tys of
-                Nothing  -> ppr tycon
-                Just tys -> ppr tycon <+> 
-                            hsep (map (pprParendHsType . unLoc) tys)
-
-derivInstCtxt1 clas inst_tys
-  = ptext SLIT("When deriving the instance for") <+> 
-    quotes (pprClassPred clas inst_tys)
+    extra | newtype_deriving = ptext (sLit "(even with cunning newtype deriving)")
+          | otherwise        = empty
+    pred = mkClassPred clas (tys ++ [ty])
+
+derivingHiddenErr :: TyCon -> SDoc
+derivingHiddenErr tc
+  = hang (ptext (sLit "The data constructors of") <+> quotes (ppr tc) <+> ptext (sLit "are not all in scope"))
+       2 (ptext (sLit "so you cannot derive an instance for it"))
+
+standaloneCtxt :: LHsType Name -> SDoc
+standaloneCtxt ty = hang (ptext (sLit "In the stand-alone deriving instance for")) 
+                      2 (quotes (ppr ty))
+
+derivInstCtxt :: Class -> [Type] -> Message
+derivInstCtxt clas inst_tys
+  = ptext (sLit "When deriving the instance for") <+> parens (pprClassPred clas inst_tys)
+
+badDerivedPred :: PredType -> Message
+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)]
 \end{code}
-