Fix Trac #3012: allow more free-wheeling in standalone deriving
[ghc-hetmet.git] / compiler / typecheck / TcDeriv.lhs
index 3aecc43..a24f147 100644 (file)
@@ -30,6 +30,7 @@ import HscTypes
 
 import Class
 import Type
+import Coercion
 import ErrUtils
 import MkId
 import DataCon
@@ -48,6 +49,8 @@ import ListSetOps
 import Outputable
 import FastString
 import Bag
+
+import Control.Monad
 \end{code}
 
 %************************************************************************
@@ -74,13 +77,17 @@ data DerivSpec  = DS { ds_loc     :: SrcSpan
                     , 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 family indexes, the tycon is the *family* tycon
-       --              (not the representation tycon)
+       -- For family indexes, 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
@@ -250,7 +257,12 @@ 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.
 
 %************************************************************************
 %*                                                                     *
@@ -262,79 +274,110 @@ when the dict is constructed in TcInstDcls.tcInstDecl2
 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 inst_decls deriv_decls
-  = recoverM (return ([], emptyValBindsOut)) $
+  = recoverM (return ([], emptyValBindsOut, emptyDUs)) $
     do {       -- Fish the "deriving"-related information out of the TcEnv
                -- And make the necessary "equations".
-       ; early_specs <- makeDerivSpecs tycl_decls inst_decls deriv_decls
+         is_boot <- tcIsHsBoot
+       ; traceTc (text "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, aux_binds1) <- mapAndUnzipM (genInst overlap_flag) given_specs
+       ; insts1 <- mapM (genInst True overlap_flag) given_specs
 
-       ; final_specs <- extendLocalInstEnv (map iSpec insts1) $
+       ; final_specs <- extendLocalInstEnv (map (iSpec . fst) insts1) $
                         inferInstanceContexts overlap_flag infer_specs
 
-       ; (insts2, aux_binds2) <- mapAndUnzipM (genInst overlap_flag) final_specs
-
-       ; is_boot <- tcIsHsBoot
-       ; rn_binds <- makeAuxBinds is_boot tycl_decls
-                                  (concat aux_binds1 ++ concat aux_binds2)
+       ; insts2 <- mapM (genInst False overlap_flag) final_specs
 
-       ; let inst_info = insts1 ++ insts2
+                -- Generate the generic to/from functions from each type declaration
+       ; gen_binds <- mkGenericBinds is_boot
+       ; (inst_info, rn_binds, rn_dus) <- renameDeriv is_boot gen_binds (insts1 ++ insts2)
 
        ; dflags <- getDOpts
        ; liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
                 (ddump_deriving inst_info rn_binds))
 
-       ; return (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
 
-makeAuxBinds :: Bool -> [LTyClDecl Name] -> DerivAuxBinds -> TcM (HsValBinds Name)
-makeAuxBinds is_boot tycl_decls deriv_aux_binds
-  | is_boot    -- If we are compiling a hs-boot file, 
-               -- don't generate any derived bindings
-  = return emptyValBindsOut
+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
-  = do { let aux_binds = listToBag (map genAuxBind (rm_dups [] deriv_aux_binds))
-               -- Generate any extra not-one-inst-decl-specific binds, 
+  = 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 = listToBag $ map (genAuxBind loc) $ 
+                         rm_dups [] $ concat deriv_aux_binds
+       ; rn_aux_lhs <- rnTopBindsLHS emptyFsEnv (ValBindsIn aux_binds [])
+       ; let aux_names = map unLoc (collectHsValBinders rn_aux_lhs)
+
+       ; bindLocalNames aux_names $ 
+    do { (rn_aux, dus_aux) <- rnTopBindsRHS (mkNameSet aux_names) 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)) } }
 
-       -- 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
-       -- Type signatures in patterns are used in the generic binds
-       ; discardWarnings $
-          setOptM Opt_PatternSignatures $
-          do   { (rn_deriv, _dus1) <- rnTopBinds (ValBindsIn aux_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) } }
   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 { iSpec = inst, iBinds = NewTypeDerived co })
+       = return (InstInfo { iSpec = inst, iBinds = NewTypeDerived co }, emptyFVs)
+
+    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
+
 -----------------------------------------
-mkGenericBinds :: [LTyClDecl Name] -> TcM (LHsBinds RdrName)
-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
+mkGenericBinds :: Bool -> TcM (LHsBinds RdrName)
+mkGenericBinds is_boot
+  | is_boot 
+  = return emptyBag
+  | otherwise
+  = do { gbl_env <- getGblEnv
+       ; let tcs = typeEnvTyCons (tcg_type_env gbl_env)
        ; return (unionManyBags [ mkTyConGenericBinds tc | 
                                  tc <- tcs, tyConHasGenerics tc ]) }
-               -- And then only in the ones whose 'has-generics' flag is on
+               -- 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}
 
 
@@ -344,44 +387,45 @@ mkGenericBinds tycl_decls
 %*                                                                     *
 %************************************************************************
 
-@makeDerivSpecs@ 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).
-
-\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}
-
-[See Appendix~E in the Haskell~1.2 report.] This code here deals w/
-all those.
+@makeDerivSpecs@ fishes around to find the info about needed derived instances.
 
 \begin{code}
-makeDerivSpecs :: [LTyClDecl Name] 
+makeDerivSpecs :: Bool 
+              -> [LTyClDecl Name] 
                -> [LInstDecl Name]
               -> [LDerivDecl Name] 
               -> TcM [EarlyDerivSpec]
 
-makeDerivSpecs tycl_decls inst_decls deriv_decls
-  = do { eqns1 <- mapAndRecoverM deriveTyData $
-                     extractTyDataPreds tycl_decls ++
-                    [ pd                        -- traverse assoc data families
-                     | L _ (InstDecl _ _ _ ats) <- inst_decls
-                    , pd <- extractTyDataPreds ats ]
+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 (catMaybes (eqns1 ++ eqns2)) }
+       ; return (eqns1 ++ eqns2) }
   where
-    extractTyDataPreds decls =                    
-      [(p, d) | d@(L _ (TyData {tcdDerivs = Just preds})) <- decls, p <- preds]
+    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 tycl_decls ++
+                [ pd                -- Traverse assoc data families
+                 | L _ (InstDecl _ _ _ ats) <- inst_decls
+                , pd <- extractTyDataPreds ats ]
+
+    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 (Maybe EarlyDerivSpec)
+deriveStandalone :: LDerivDecl Name -> TcM EarlyDerivSpec
 -- Standalone deriving declarations
---  e.g.   deriving instance show a => Show (T a)
+--  e.g.   deriving instance Show a => Show (T a)
 -- Rather like tcLocalInstDecl
 deriveStandalone (L loc (DerivDecl deriv_ty))
   = setSrcSpan loc                   $
@@ -393,9 +437,11 @@ deriveStandalone (L loc (DerivDecl deriv_ty))
               <+> text "theta:" <+> ppr theta
               <+> text "tau:" <+> ppr tau)
        ; (cls, inst_tys) <- checkValidInstHead tau
+       ; checkValidInstance tvs theta cls inst_tys
+               -- C.f. TcInstDcls.tcLocalInstDecl1
+
        ; let cls_tys = take (length inst_tys - 1) inst_tys
              inst_ty = last inst_tys
-
        ; traceTc (text "standalone deriving;"
               <+> text "class:" <+> ppr cls
               <+> text "class types:" <+> ppr cls_tys
@@ -404,70 +450,167 @@ deriveStandalone (L loc (DerivDecl deriv_ty))
                    (Just theta) }
 
 ------------------------------------------------------------------
-deriveTyData :: (LHsType Name, LTyClDecl Name) -> TcM (Maybe EarlyDerivSpec)
-deriveTyData (deriv_pred, L loc decl@(TyData { tcdLName = L _ tycon_name, 
-                                              tcdTyVars = tv_names, 
-                                              tcdTyPats = ty_pats }))
-  = setSrcSpan loc                   $
-    tcAddDeclCtxt decl              $
-    do { let hs_ty_args = ty_pats `orElse` map (nlHsTyVar . hsLTyVarName) tv_names
-             hs_app     = nlHsTyConApp tycon_name hs_ty_args
-               -- We get kinding info for the tyvars by typechecking (T a b)
-               -- Hence forming a tycon application and then dis-assembling it
-       ; (tvs, tc_app) <- tcHsQuantifiedType tv_names hs_app
+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]).
-       ; mkEqnHelp DerivOrigin (tvs++deriv_tvs) cls cls_tys tc_app Nothing } }
+
+       -- 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 (isOpenTyCon 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 (coMkS a)) : Eq [a] ~ Eq (S a)
+    instance Monad [] => Monad S       -- by coercion sym (Monad coMkS)  : 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 :: InstOrigin -> [TyVar] -> Class -> [Type] -> Type
           -> Maybe ThetaType   -- Just    => context supplied (standalone deriving)
                                -- Nothing => context inferred (deriving on data decl)
-          -> TcRn (Maybe EarlyDerivSpec)
+          -> 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
-  = do {
+  , isAlgTyCon tycon   -- Check for functions, primitive types etc
+  = do { (rep_tc, rep_tc_args) <- tcLookupFamInstExact 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
-       -- By this time we know that the thing is algebraic
-       --      because we've called checkInstHead in derivingStandalone
-         rdr_env <- getGlobalRdrEnv
-       ; let hidden_data_cons = filter not_in_scope (tyConDataCons tycon)
-             not_in_scope dc = null (lookupGRE_Name rdr_env (dataConName dc))
-       ; checkTc (isNothing mtheta || null hidden_data_cons) 
+       -- 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)
 
-       ; mayDeriveDataTypeable <- doptM Opt_DeriveDataTypeable
-       ; newtype_deriving <- doptM Opt_GeneralizedNewtypeDeriving
-
-       ; (rep_tc, rep_tc_args) <- tcLookupFamInstExact 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
+       ; dflags <- getDOpts
        ; if isDataTyCon rep_tc then
-               mkDataTypeEqn orig mayDeriveDataTypeable tvs cls cls_tys 
+               mkDataTypeEqn orig dflags tvs cls cls_tys
                              tycon tc_args rep_tc rep_tc_args mtheta
          else
-               mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving
-                            tvs cls cls_tys 
+               mkNewTypeEqn orig dflags tvs cls cls_tys 
                             tycon tc_args rep_tc rep_tc_args mtheta }
   | otherwise
-  = baleOut (derivingThingErr cls cls_tys tc_app
-               (ptext (sLit "Last argument of the instance must be a type application")))
-
-baleOut :: Message -> TcM (Maybe a)
-baleOut err = do { addErrTc err;  return Nothing }
+  = failWithTc (derivingThingErr cls cls_tys tc_app
+              (ptext (sLit "The last argument of the instance must be a data or newtype application")))
 \end{code}
 
-Auxiliary lookup wrapper which requires that looked up family instances are
-not type instances.  If called with a vanilla tycon, the old type application
-is simply returned.
+Note [Looking up family instances for deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+tcLookupFamInstExact is an auxiliary lookup wrapper which requires
+that looked-up family instances exist.  If called with a vanilla
+tycon, the old type application is simply returned.
+
+If we have
+  data instance F () = ... deriving Eq
+  data instance F () = ... deriving Eq
+then tcLookupFamInstExact will be confused by the two matches;
+but that can't happen because tcInstDecls1 doesn't call tcDeriving
+if there are any overlaps.
+
+There are two other things that might go wrong with the lookup.
+First, we might see a standalone deriving clause
+       deriving Eq (F ())
+when there is no data instance F () in scope. 
+
+Note that it's OK to have
+  data instance F [a] = ...
+  deriving Eq (F [(a,b)])
+where the match is not exact; the same holds for ordinary data types
+with standalone deriving declrations.
 
 \begin{code}
 tcLookupFamInstExact :: TyCon -> [Type] -> TcM (TyCon, [Type])
@@ -477,18 +620,14 @@ tcLookupFamInstExact tycon tys
   | otherwise
   = do { maybeFamInst <- tcLookupFamInst tycon tys
        ; case maybeFamInst of
-           Nothing                     -> famInstNotFound tycon tys False
-           Just famInst@(_, rep_tys)
-             | not variable_only_subst -> famInstNotFound tycon tys True
-             | otherwise               -> return famInst
-             where
-               tvs                 = map (Type.getTyVar 
-                                             "TcDeriv.tcLookupFamInstExact") 
-                                         rep_tys
-              variable_only_subst  = all Type.isTyVarTy rep_tys &&
-                                     sizeVarSet (mkVarSet tvs) == length tvs
-                                       -- renaming may have no repetitions
+           Nothing      -> famInstNotFound tycon tys
+           Just famInst -> return famInst
        }
+
+famInstNotFound :: TyCon -> [Type] -> TcM a
+famInstNotFound tycon tys 
+  = failWithTc (ptext (sLit "No family instance for")
+                       <+> quotes (pprTypeApp tycon tys))
 \end{code}
 
 
@@ -499,24 +638,34 @@ tcLookupFamInstExact tycon tys
 %************************************************************************
 
 \begin{code}
-mkDataTypeEqn :: InstOrigin -> Bool -> [Var] -> Class -> [Type]
-              -> TyCon -> [Type] -> TyCon -> [Type] -> Maybe ThetaType
-              -> TcRn (Maybe EarlyDerivSpec)   -- Return 'Nothing' if error
-               
-mkDataTypeEqn orig mayDeriveDataTypeable tvs cls cls_tys
+mkDataTypeEqn :: InstOrigin
+              -> 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
+              -> Maybe ThetaType        -- 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
-  | Just err <- checkSideConditions mayDeriveDataTypeable cls cls_tys rep_tc
-       -- NB: pass the *representation* tycon to checkSideConditions
-  = baleOut (derivingThingErr cls cls_tys (mkTyConApp tycon tc_args) err)
-
-  | otherwise 
-  = ASSERT( null cls_tys )
-    mk_data_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
+  | isJust mtheta = go_for_it  -- Do not test side conditions for standalone deriving
+  | otherwise     = case checkSideConditions dflags 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 cls cls_tys (mkTyConApp tycon tc_args) msg)
 
 mk_data_eqn, mk_typeable_eqn
    :: InstOrigin -> [TyVar] -> Class 
    -> TyCon -> [TcType] -> TyCon -> [TcType] -> Maybe ThetaType
-   -> TcM (Maybe EarlyDerivSpec)
+   -> 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
@@ -524,32 +673,19 @@ mk_data_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
   | otherwise
   = do { dfun_name <- new_dfun_name cls tycon
        ; loc <- getSrcSpanM
-       ; let ordinary_constraints
-               = [ mkClassPred cls [arg_ty] 
-                 | data_con <- tyConDataCons rep_tc,
-                   arg_ty   <- ASSERT( isVanillaDataCon data_con )
-                               dataConInstOrigArgTys data_con rep_tc_args,
-                   not (isUnLiftedType arg_ty) ] -- No constraints for unlifted types?
-
-                       -- See Note [Superclasses of derived instance]
-             sc_constraints = substTheta (zipOpenTvSubst (classTyVars cls) inst_tys)
-                                         (classSCTheta cls)
-             inst_tys =  [mkTyConApp tycon tc_args]
-
-             stupid_subst = zipTopTvSubst (tyConTyVars rep_tc) rep_tc_args
-             stupid_constraints = substTheta stupid_subst (tyConStupidTheta rep_tc)
-             all_constraints = stupid_constraints ++ sc_constraints ++ ordinary_constraints
-
+       ; 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_theta =  mtheta `orElse` all_constraints
+                       , ds_tc = rep_tc, ds_tc_args = rep_tc_args
+                       , ds_theta =  mtheta `orElse` inferred_constraints
                        , ds_newtype = False }
 
-       ; return (if isJust mtheta then Just (Right spec)       -- Specified context
-                                  else Just (Left spec)) }     -- Infer context
+       ; 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
+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
@@ -571,11 +707,68 @@ mk_typeable_eqn orig tvs cls tycon tc_args rep_tc _rep_tc_args mtheta
                        <> int (tyConArity tycon) <+> ppr tycon <> rparen)
        ; dfun_name <- new_dfun_name cls tycon
        ; loc <- getSrcSpanM
-       ; return (Just $ Right $
+       ; return (Right $
                  DS { ds_loc = loc, ds_orig = orig, ds_name = dfun_name, ds_tvs = []
-                    , ds_cls = cls, ds_tys = [mkTyConApp tycon []] 
+                    , 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 tvs 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 constraints
+       -- The Data class (only) requires that for 
+       --    instance (...) => Data (T a b) 
+       -- then (Data a, Data b) are among the (...) constraints
+       -- Reason: that's what you need to typecheck the method
+       --             dataCast1 f = gcast1 f
+    extra_constraints 
+      | cls `hasKey` dataClassKey = [mkClassPred cls [mkTyVarTy tv] | tv <- tvs]
+      | otherwise                = []
+
 ------------------------------------------------------------------
 -- Check side conditions that dis-allow derivability for particular classes
 -- This is *apart* from the newtype-deriving mechanism
@@ -584,35 +777,49 @@ mk_typeable_eqn orig tvs cls tycon tc_args rep_tc _rep_tc_args mtheta
 -- the data constructors - but we need to be careful to fall back to the
 -- family tycon (with indexes) in error messages.
 
-checkSideConditions :: Bool -> Class -> [TcType] -> TyCon -> Maybe SDoc
-checkSideConditions mayDeriveDataTypeable cls cls_tys rep_tc
-  | notNull cls_tys    
-  = Just ty_args_why   -- e.g. deriving( Foo s )
-  | otherwise
-  = case sideConditions cls of
-       Just cond -> cond (mayDeriveDataTypeable, rep_tc)
-       Nothing   -> Just non_std_why
+data DerivStatus = CanDerive
+                | DerivableClassError SDoc     -- Standard class, but can't do it
+                | NonDerivableClass            -- Non-standard class
+
+checkSideConditions :: DynFlags -> Class -> [TcType] -> TyCon -> DerivStatus
+checkSideConditions dflags cls cls_tys rep_tc
+  | Just cond <- sideConditions cls
+  = case (cond (dflags, rep_tc)) of
+       Just err -> DerivableClassError err     -- Class-specific error
+       Nothing  | null cls_tys -> CanDerive
+                | 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")
-    non_std_why = quotes (ppr cls) <+> ptext (sLit "is not a derivable class")
+
+nonStdErr :: Class -> SDoc
+nonStdErr cls = quotes (ppr cls) <+> ptext (sLit "is not a derivable class")
 
 sideConditions :: Class -> Maybe Condition
 sideConditions cls
-  | cls_key == eqClassKey   = Just cond_std
-  | cls_key == ordClassKey  = Just cond_std
-  | cls_key == readClassKey = Just cond_std
-  | cls_key == showClassKey = Just cond_std
-  | cls_key == enumClassKey = Just (cond_std `andCond` cond_isEnumeration)
-  | cls_key == ixClassKey   = Just (cond_std `andCond` (cond_isEnumeration `orCond` cond_isProduct))
-  | cls_key == boundedClassKey = Just (cond_std `andCond` (cond_isEnumeration `orCond` cond_isProduct))
-  | cls_key == dataClassKey    = Just (cond_mayDeriveDataTypeable `andCond` cond_std)
-  | getName cls `elem` typeableClassNames = Just (cond_mayDeriveDataTypeable `andCond` cond_typeableOK)
+  | 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
 
-type Condition = (Bool, TyCon) -> Maybe SDoc
-       -- Bool is whether or not we are allowed to derive Data and Typeable
+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
@@ -633,16 +840,37 @@ andCond c1 c2 tc = case c1 tc of
 
 cond_std :: Condition
 cond_std (_, rep_tc)
-  | any (not . isVanillaDataCon) data_cons = Just existential_why     
-  | null data_cons                        = Just no_cons_why
-  | otherwise                             = Nothing
+  | null data_cons      = Just no_cons_why
+  | not (null con_whys) = Just (vcat con_whys)
+  | otherwise          = Nothing
   where
     data_cons       = tyConDataCons rep_tc
     no_cons_why            = quotes (pprSourceTyCon rep_tc) <+> 
                      ptext (sLit "has no data constructors")
-    existential_why = quotes (pprSourceTyCon rep_tc) <+> 
-                     ptext (sLit "has non-Haskell-98 constructor(s)")
+
+    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")))
   
+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"))
+
 cond_isEnumeration :: Condition
 cond_isEnumeration (_, rep_tc)
   | isEnumerationTyCon rep_tc = Nothing
@@ -677,26 +905,72 @@ cond_typeableOK (_, rep_tc)
     fam_inst = quotes (pprSourceTyCon rep_tc) <+> 
               ptext (sLit "is a type family")
 
-cond_mayDeriveDataTypeable :: Condition
-cond_mayDeriveDataTypeable (mayDeriveDataTypeable, _)
- | mayDeriveDataTypeable = Nothing
- | otherwise = Just why
+
+functorLikeClassKeys :: [Unique]
+functorLikeClassKeys = [functorClassKey, foldableClassKey, traversableClassKey]
+
+cond_functorOK :: Bool -> Condition
+-- OK for Functor 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
+cond_functorOK allowFunctions (dflags, rep_tc) 
+  | not (dopt Opt_DeriveFunctor dflags)
+  = Just (ptext (sLit "You need -XDeriveFunctor to derive an instance for this class"))
+  | otherwise
+  = msum (map check_con data_cons)     -- msum picks the first 'Just', if any
+  where
+    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 :: DynFlag -> Condition
+checkFlag flag (dflags, _)
+  | dopt flag dflags = Nothing
+  | otherwise        = Just why
   where
-    why  = ptext (sLit "You need -XDeriveDataTypeable to derive an instance for this class")
+    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
 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]
+  = classKey clas `elem` [eqClassKey, ordClassKey, ixClassKey, boundedClassKey]
        -- Not Read/Show because they respect the type
        -- Not Enum, because newtypes are never in Enum
 
 
 new_dfun_name :: Class -> TyCon -> TcM Name
 new_dfun_name clas tycon       -- Just a simple wrapper
-  = newDFunName clas [mkTyConApp tycon []] (getSrcSpan tycon)
+  = 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] 
@@ -731,35 +1005,41 @@ a context for the Data instances:
 %************************************************************************
 
 \begin{code}
-mkNewTypeEqn :: InstOrigin -> Bool -> Bool -> [Var] -> Class
+mkNewTypeEqn :: InstOrigin -> DynFlags -> [Var] -> Class
              -> [Type] -> TyCon -> [Type] -> TyCon -> [Type]
              -> Maybe ThetaType
-             -> TcRn (Maybe EarlyDerivSpec)
-mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving tvs
+             -> 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 (text "newtype deriving:" <+> ppr tycon <+> ppr rep_tys)
        ; dfun_name <- new_dfun_name cls tycon
        ; loc <- getSrcSpanM
        ; let spec = DS { ds_loc = loc, ds_orig = orig
-                       , ds_name = dfun_name, ds_tvs = dict_tvs 
+                       , 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 Just (Right spec)
-                                  else Just (Left spec)) }
+       ; return (if isJust mtheta then Right spec
+                                  else Left spec) }
 
-  | isNothing mb_std_err       -- Use the standard H98 method
-  = mk_data_eqn orig tvs cls tycon tc_args rep_tycon rep_tc_args mtheta
-
-       -- Otherwise we can't derive
-  | newtype_deriving = baleOut cant_derive_err -- Too hard
-  | otherwise        = baleOut std_err         -- Just complain about being a non-std instance
+  | isJust mtheta = go_for_it  -- Do not check side conditions for standalone deriving
+  | otherwise
+  = case checkSideConditions dflags cls cls_tys rep_tycon of
+      CanDerive               -> go_for_it     -- Use the standard H98 method
+      DerivableClassError msg -> bale_out msg  -- Error with standard class
+      NonDerivableClass        -- Must use newtype deriving
+       | newtype_deriving    -> bale_out cant_derive_err  -- Too hard, even with newtype deriving
+       | otherwise           -> bale_out non_std_err      -- Try newtype deriving!
   where
-       mb_std_err = checkSideConditions mayDeriveDataTypeable cls cls_tys rep_tycon
-       std_err = derivingThingErr cls cls_tys tc_app $
-                 vcat [fromJust mb_std_err,
-                       ptext (sLit "Try -XGeneralizedNewtypeDeriving for GHC's newtype-deriving extension")]
+        newtype_deriving = dopt 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 cls cls_tys inst_ty msg)
+
+       non_std_err = nonStdErr cls $$
+                     ptext (sLit "Try -XGeneralizedNewtypeDeriving for GHC's newtype-deriving extension")
 
        -- Here is the plan for newtype derivings.  We see
        --        newtype T a1...an = MkT (t ak+1...an) deriving (.., C s1 .. sm, ...)
@@ -770,6 +1050,8 @@ mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving tvs
        --                      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)).
@@ -789,15 +1071,12 @@ mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving tvs
        -- We generate the instance
        --      instance Monad (ST s) => Monad (T s) where 
 
-       cls_tyvars = classTyVars cls
-       kind = tyVarKind (last cls_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)
+       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]
        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -807,30 +1086,21 @@ mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving tvs
        --      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!
-       rep_ty                = newTyConInstRhs rep_tycon rep_tc_args
-       (rep_fn, rep_ty_args) = tcSplitAppTys rep_ty
-
-       n_tyargs_to_keep = tyConArity tycon - n_args_to_drop
-       dropped_tc_args = drop n_tyargs_to_keep tc_args
-       dropped_tvs     = tyVarsOfTypes dropped_tc_args
-
-       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  = cls_tys ++ [rep_fn']
-       rep_pred = mkClassPred cls 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 
 
-       tc_app = mkTyConApp tycon (take n_tyargs_to_keep tc_args)
 
     -- Next we figure out what superclass dictionaries to use
     -- See Note [Newtype deriving superclasses] above
 
-       inst_tys = cls_tys ++ [tc_app]
+       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)
 
@@ -841,75 +1111,65 @@ mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving tvs
                --              instance C T
                -- rather than
                --              instance C Int => C T
-       dict_tvs = filterOut (`elemVarSet` dropped_tvs) tvs
        all_preds = rep_pred : sc_theta         -- NB: rep_pred comes first
 
        -------------------------------------------------------------------
        --  Figuring out whether we can only do this newtype-deriving thing
 
-       right_arity = length cls_tys + 1 == classArity cls
-
-               -- Never derive Read,Show,Typeable,Data this way 
-       non_iso_classes = [readClassKey, showClassKey, typeableClassKey, dataClassKey]
        can_derive_via_isomorphism
-          =  not (getUnique cls `elem` non_iso_classes)
-          && right_arity                       -- Well kinded;
-                                               -- eg not: newtype T ... deriving( ST )
-                                               --      because ST needs *2* type params
-          && n_tyargs_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
+          =  not (non_iso_class cls)
+          && arity_ok
+          && eta_ok
+          && ats_ok
+--        && not (isRecursiveTyCon tycon)      -- Note [Recursive newtypes]
+
+               -- Never derive Read,Show,Typeable,Data by isomorphism
+       non_iso_class cls = className cls `elem` ([readClassName, showClassName, dataClassName] ++
+                                                 typeableClassNames)
+
+       arity_ok = length cls_tys + 1 == classArity cls
+               -- Well kinded; eg not: newtype T ... deriving( ST )
+               --                      because ST needs *2* type params
 
        -- Check that eta reduction is OK
-       eta_ok = (args_to_drop `tcEqTypes` dropped_tc_args)
-               -- (a) the dropped-off args are identical in the source and rep type
+       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)
-
-             && (tyVarsOfType rep_fn' `disjointVarSet` dropped_tvs)
-               -- (b) the remaining type args do not mention any of the dropped
-               --     type variables 
-
-             && (tyVarsOfTypes cls_tys `disjointVarSet` dropped_tvs)
-               -- (c) the type class args do not mention any of the dropped type
-               --     variables 
-
-             && all isTyVarTy dropped_tc_args
-               -- (d) in case of newtype family instances, the eta-dropped
-               --      arguments must be type variables (not more complex indexes)
-
-       cant_derive_err = derivingThingErr cls cls_tys tc_app
-                               (vcat [ptext (sLit "even with cunning newtype deriving:"),
-                                       if isRecursiveTyCon tycon then
-                                         ptext (sLit "the newtype may be recursive")
-                                       else empty,
-                                       if not right_arity then 
-                                         quotes (ppr (mkClassPred cls cls_tys)) <+> ptext (sLit "does not have arity 1")
-                                       else empty,
-                                       if not (n_tyargs_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
-                                     ])
+               --     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 [ ptext (sLit "even with cunning newtype deriving:")
+                 , if arity_ok then empty else arity_msg
+                 , if eta_ok then empty else eta_msg
+                 , if ats_ok then empty else 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}
 
+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.
+
+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.
+
 
 %************************************************************************
 %*                                                                     *
@@ -955,14 +1215,14 @@ inferInstanceContexts oflag infer_specs
     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 pprDerivSpec infer_specs) $$ ppr current_solns)
       | otherwise
       =        do {      -- Extend the inst info from the explicit instance decls
                  -- with the current set of solutions, and simplify each RHS
-            let inst_specs = zipWithEqual "add_solns" (mkInstance2 oflag)
+            let inst_specs = zipWithEqual "add_solns" (mkInstance oflag)
                                           current_solns infer_specs
           ; new_solns <- checkNoErrs $
                          extendLocalInstEnv inst_specs $
@@ -1000,11 +1260,8 @@ inferInstanceContexts oflag infer_specs
           ; return (sortLe (<=) theta) }       -- Canonicalise before returning the solution
 
 ------------------------------------------------------------------
-mkInstance1 :: OverlapFlag -> DerivSpec -> Instance
-mkInstance1 overlap_flag spec = mkInstance2 overlap_flag (ds_theta spec) spec
-
-mkInstance2 :: OverlapFlag -> ThetaType -> DerivSpec -> Instance
-mkInstance2 overlap_flag theta
+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
@@ -1093,50 +1350,55 @@ the renamer.  What a great hack!
 -- Representation tycons differ from the tycon in the instance signature in
 -- case of instances for indexed families.
 --
-genInst :: OverlapFlag -> DerivSpec -> TcM (InstInfo, DerivAuxBinds)
-genInst oflag spec
+genInst :: Bool        -- True <=> standalone deriving
+       -> OverlapFlag
+        -> DerivSpec -> TcM (InstInfo RdrName, DerivAuxBinds)
+genInst standalone_deriv oflag spec
   | ds_newtype spec
-  = return (InstInfo { iSpec = mkInstance1 oflag spec 
-                    , iBinds = NewTypeDerived }, [])
+  = return (InstInfo { iSpec  = mkInstance oflag (ds_theta spec) spec
+                    , iBinds = NewTypeDerived co }, [])
 
   | otherwise
-  = do { fix_env <- getFixityEnv
-       ; let
-           inst                    = mkInstance1 oflag spec
-           (tyvars,_,clas,[ty])    = instanceHead inst
-           clas_nm                 = className clas
-           (visible_tycon, tyArgs) = tcSplitTyConApp ty 
+  = 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, _) <- tcLookupFamInstExact visible_tycon tyArgs
-       ; 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 (\_ -> []) [] meth_binds
-
-       -- Build the InstInfo
-       ; return (InstInfo { iSpec = inst, 
-                            iBinds = VanillaInst rn_meth_binds [] },
-                 aux_binds)
+       ; 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 :: Class -> FixityEnv -> TyCon -> (LHsBinds RdrName, DerivAuxBinds)
-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
+             Nothing     -> IdCo
+             Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
+    co2 = case newTyConCo_maybe rep_tycon of
+              Nothing     -> IdCo      -- The newtype is transparent; no need for a cast
+             Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
+    co = co1 `mkTransCoI` co2
+
+-- 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)
+
+genDerivBinds :: SrcSpan -> FixityEnv -> Class -> TyCon -> (LHsBinds RdrName, DerivAuxBinds)
+genDerivBinds loc fix_env clas tycon
   | className clas `elem` typeableClassNames
-  = (gen_Typeable_binds tycon, [])
+  = (gen_Typeable_binds loc tycon, [])
 
   | otherwise
   = case assocMaybe gen_list (getUnique clas) of
-       Just gen_fn -> gen_fn tycon
+       Just gen_fn -> gen_fn loc tycon
        Nothing     -> pprPanic "genDerivBinds: bad derived class" (ppr clas)
   where
-    gen_list :: [(Unique, TyCon -> (LHsBinds RdrName, DerivAuxBinds))]
+    gen_list :: [(Unique, SrcSpan -> TyCon -> (LHsBinds RdrName, DerivAuxBinds))]
     gen_list = [(eqClassKey,       gen_Eq_binds)
               ,(ordClassKey,      gen_Ord_binds)
               ,(enumClassKey,     gen_Enum_binds)
@@ -1144,7 +1406,10 @@ genDerivBinds clas fix_env tycon
               ,(ixClassKey,       gen_Ix_binds)
               ,(showClassKey,     gen_Show_binds fix_env)
               ,(readClassKey,     gen_Read_binds fix_env)
-              ,(dataClassKey,     gen_Data_binds fix_env)
+              ,(dataClassKey,     gen_Data_binds)
+              ,(functorClassKey,  gen_Functor_binds)
+              ,(foldableClassKey, gen_Foldable_binds)
+              ,(traversableClassKey, gen_Traversable_binds)
               ]
 \end{code}
 
@@ -1156,6 +1421,24 @@ genDerivBinds clas fix_env tycon
 %************************************************************************
 
 \begin{code}
+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 :: Class -> [Type] -> Type -> Message -> Message
 derivingThingErr clas tys ty why
   = sep [hsep [ptext (sLit "Can't make a derived instance of"), 
@@ -1182,12 +1465,4 @@ 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)]
-
-famInstNotFound :: TyCon -> [Type] -> Bool -> TcM a
-famInstNotFound tycon tys notExact
-  = failWithTc (msg <+> quotes (pprTypeApp tycon (ppr tycon) tys))
-  where
-    msg = ptext $ if notExact
-                 then sLit "No family instance exactly matching"
-                 else sLit "More than one family instance for"
 \end{code}