Improve error messages for roles by writing role names out
[ghc.git] / compiler / typecheck / TcDeriv.lhs
index 8d79e89..144678e 100644 (file)
@@ -6,13 +6,6 @@
 Handles @deriving@ clauses on @data@ declarations.
 
 \begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
 module TcDeriv ( tcDeriving ) where
 
 #include "HsVersions.h"
@@ -22,10 +15,12 @@ import DynFlags
 
 import TcRnMonad
 import FamInst
+import TcErrors( reportAllUnsolved )
+import TcValidity( validDerivPred )
 import TcEnv
-import TcTyClsDecls( tcFamTyPats, tcAddFamInstCtxt )
-import TcClassDcl( tcAddDeclCtxt )     -- Small helper
-import TcGenDeriv                      -- Deriv stuff
+import TcTyClsDecls( tcFamTyPats, tcAddDataFamInstCtxt )
+import TcClassDcl( tcAddDeclCtxt )      -- Small helper
+import TcGenDeriv                       -- Deriv stuff
 import TcGenGenerics
 import InstEnv
 import Inst
@@ -36,10 +31,11 @@ import TcSimplify
 import TcEvidence
 
 import RnBinds
-import RnEnv  
+import RnEnv
 import RnSource   ( addTcgDUs )
 import HscTypes
 
+import Id( idType )
 import Class
 import Type
 import ErrUtils
@@ -66,9 +62,9 @@ import Data.List
 \end{code}
 
 %************************************************************************
-%*                                                                     *
-               Overview
-%*                                                                     *
+%*                                                                      *
+                Overview
+%*                                                                      *
 %************************************************************************
 
 Overall plan
@@ -84,26 +80,26 @@ Overall plan
 \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
+                     , 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:
@@ -119,24 +115,24 @@ Example:
 
 \begin{code}
 type DerivContext = Maybe ThetaType
-   -- Nothing   <=> Vanilla deriving; infer the context of the instance decl
+   -- 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
+        -- 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 })
+                   ds_cls = c, ds_tys = tys, ds_theta = rhs })
   = parens (hsep [ppr l, ppr n, ppr tvs, ppr c, ppr tys]
-           <+> equals <+> ppr rhs)
+            <+> equals <+> ppr rhs)
 
 instance Outputable DerivSpec where
   ppr = pprDerivSpec
@@ -147,19 +143,19 @@ Inferring missing contexts
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
-       data T a b = C1 (Foo a) (Bar b)
-                  | C2 Int (T b a)
-                  | C3 (T a a)
-                  deriving (Eq)
+        data T a b = C1 (Foo a) (Bar b)
+                   | C2 Int (T b a)
+                   | C3 (T a a)
+                   deriving (Eq)
 
 [NOTE: See end of these comments for what to do with
-       data (C a, D b) => T a b = ...
+        data (C a, D b) => T a b = ...
 ]
 
 We want to come up with an instance declaration of the form
 
-       instance (Ping a, Pong b, ...) => Eq (T a b) where
-               x == y = ...
+        instance (Ping a, Pong b, ...) => Eq (T a b) where
+                x == y = ...
 
 It is pretty easy, albeit tedious, to fill in the code "...".  The
 trick is to figure out what the context for the instance decl is,
@@ -168,13 +164,13 @@ namely @Ping@, @Pong@ and friends.
 Let's call the context reqd for the T instance of class C at types
 (a,b, ...)  C (T a b).  Thus:
 
-       Eq (T a b) = (Ping a, Pong b, ...)
+        Eq (T a b) = (Ping a, Pong b, ...)
 
 Now we can get a (recursive) equation from the @data@ decl:
 
-       Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
-                  u Eq (T b a) u Eq Int        -- From C2
-                  u Eq (T a a)                 -- From C3
+        Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
+                   u Eq (T b a) u Eq Int        -- From C2
+                   u Eq (T a a)                 -- From C3
 
 Foo and Bar may have explicit instances for @Eq@, in which case we can
 just substitute for them.  Alternatively, either or both may have
@@ -189,37 +185,37 @@ Let's suppose Eq (Foo a) = Eq a, and Eq (Bar b) = Ping b.
 
 We start with:
 
-       Eq (T a b) = {}         -- The empty set
+        Eq (T a b) = {}         -- The empty set
 
 Next iteration:
-       Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
-                  u Eq (T b a) u Eq Int        -- From C2
-                  u Eq (T a a)                 -- From C3
+        Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
+                   u Eq (T b a) u Eq Int        -- From C2
+                   u Eq (T a a)                 -- From C3
 
-       After simplification:
-                  = Eq a u Ping b u {} u {} u {}
-                  = Eq a u Ping b
+        After simplification:
+                   = Eq a u Ping b u {} u {} u {}
+                   = Eq a u Ping b
 
 Next iteration:
 
-       Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
-                  u Eq (T b a) u Eq Int        -- From C2
-                  u Eq (T a a)                 -- From C3
+        Eq (T a b) = Eq (Foo a) u Eq (Bar b)    -- From C1
+                   u Eq (T b a) u Eq Int        -- From C2
+                   u Eq (T a a)                 -- From C3
 
-       After simplification:
-                  = Eq a u Ping b
-                  u (Eq b u Ping a)
-                  u (Eq a u Ping a)
+        After simplification:
+                   = Eq a u Ping b
+                   u (Eq b u Ping a)
+                   u (Eq a u Ping a)
 
-                  = Eq a u Ping b u Eq b u Ping a
+                   = Eq a u Ping b u Eq b u Ping a
 
 The next iteration gives the same result, so this is the fixpoint.  We
 need to make a canonical form of the RHS to ensure convergence.  We do
 this by simplifying the RHS to a form in which
 
-       - the classes constrain only tyvars
-       - the list is sorted by tyvar (major key) and then class (minor key)
-       - no duplicates, of course
+        - the classes constrain only tyvars
+        - the list is sorted by tyvar (major key) and then class (minor key)
+        - no duplicates, of course
 
 So, here are the synonyms for the ``equation'' structures:
 
@@ -228,12 +224,12 @@ Note [Data decl contexts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
-       data (RealFloat a) => Complex a = !a :+ !a deriving( Read )
+        data (RealFloat a) => Complex a = !a :+ !a deriving( Read )
 
 We will need an instance decl like:
 
-       instance (Read a, RealFloat a) => Read (Complex a) where
-         ...
+        instance (Read a, RealFloat a) => Read (Complex a) where
+          ...
 
 The RealFloat in the context is because the read method for Complex is bound
 to construct a Complex, and doing that requires that the argument type is
@@ -245,7 +241,7 @@ a Complex; they only take them apart.
 Our approach: identify the offending classes, and add the data type
 context to the instance decl.  The "offending classes" are
 
-       Read, Enum?
+        Read, Enum?
 
 FURTHER NOTE ADDED March 2002.  In fact, Haskell98 now requires that
 pattern matching against a constructor from a data type with a context
@@ -276,16 +272,16 @@ 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 )
+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"
+        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...
+        (+) = ((+)@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
 
@@ -298,9 +294,9 @@ 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.
 
 %************************************************************************
-%*                                                                     *
+%*                                                                      *
 \subsection[TcDeriv-driver]{Top-level function for \tr{derivings}}
-%*                                                                     *
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
@@ -311,31 +307,33 @@ tcDeriving  :: [LTyClDecl Name]  -- All type constructors
 tcDeriving tycl_decls inst_decls deriv_decls
   = recoverM (do { g <- getGblEnv
                  ; return (g, emptyBag, emptyValBindsOut)}) $
-    do {       -- Fish the "deriving"-related information out of the TcEnv
-               -- And make the necessary "equations".
-         is_boot <- tcIsHsBoot
-       ; traceTc "tcDeriving" (ppr is_boot)
-       ; early_specs <- makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
+    do  {       -- Fish the "deriving"-related information out of the TcEnv
+                -- And make the necessary "equations".
+          is_boot <- tcIsHsBoot
+        ; traceTc "tcDeriving" (ppr is_boot)
+
+        ; early_specs <- makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
+        ; traceTc "tcDeriving 1" (ppr early_specs)
 
         -- for each type, determine the auxliary declarations that are common
         -- to multiple derivations involving that type (e.g. Generic and
         -- Generic1 should use the same TcGenGenerics.MetaTyCons)
         ; (commonAuxs, auxDerivStuff) <- commonAuxiliaries $ map (either id id) early_specs
 
-       ; overlap_flag <- getOverlapFlag
-       ; let (infer_specs, given_specs) = splitEithers early_specs
-       ; insts1 <- mapM (genInst True overlap_flag commonAuxs) given_specs
+        ; overlap_flag <- getOverlapFlag
+        ; let (infer_specs, given_specs) = splitEithers early_specs
+        ; insts1 <- mapM (genInst True overlap_flag commonAuxs) given_specs
 
         -- the stand-alone derived instances (@insts1@) are used when inferring
         -- the contexts for "deriving" clauses' instances (@infer_specs@)
-       ; final_specs <- extendLocalInstEnv (map (iSpec . fst) insts1) $
-                           inferInstanceContexts overlap_flag infer_specs
+        ; final_specs <- extendLocalInstEnv (map (iSpec . fst) insts1) $
+                         inferInstanceContexts overlap_flag infer_specs
 
-       ; insts2 <- mapM (genInst False overlap_flag commonAuxs) final_specs
+        ; insts2 <- mapM (genInst False overlap_flag commonAuxs) final_specs
 
         ; let (inst_infos, deriv_stuff) = unzip (insts1 ++ insts2)
         ; loc <- getSrcSpanM
-        ; let (binds, newTyCons, famInsts, extraInstances) = 
+        ; let (binds, newTyCons, famInsts, extraInstances) =
                 genAuxBinds loc (unionManyBags (auxDerivStuff : deriv_stuff))
 
         ; (inst_info, rn_binds, rn_dus) <-
@@ -354,9 +352,9 @@ tcDeriving tycl_decls inst_decls deriv_decls
 
         ; return (addTcgDUs gbl_env rn_dus, inst_info, rn_binds) }
   where
-    ddump_deriving :: Bag (InstInfo Name) -> HsValBinds Name 
-                   -> Bag TyCon    -- ^ Empty data constructors
-                   -> Bag FamInst  -- ^ Rep type family instances
+    ddump_deriving :: Bag (InstInfo Name) -> HsValBinds Name
+                   -> Bag TyCon                 -- ^ Empty data constructors
+                   -> Bag (FamInst)             -- ^ Rep type family instances
                    -> SDoc
     ddump_deriving inst_infos extra_binds repMetaTys repFamInsts
       =    hang (ptext (sLit "Derived instances:"))
@@ -370,7 +368,12 @@ tcDeriving tycl_decls inst_decls deriv_decls
 
     hangP s x = text "" $$ hang (ptext (sLit s)) 2 x
 
-
+-- Prints the representable type family instance
+pprRepTy :: FamInst -> SDoc
+pprRepTy fi@(FamInst { fi_tys = lhs })
+  = ptext (sLit "type") <+> ppr (mkTyConApp (famInstTyCon fi) lhs) <+>
+      equals <+> ppr rhs
+  where rhs = famInstRHS fi
 
 -- As of 24 April 2012, this only shares MetaTyCons between derivations of
 -- Generic and Generic1; thus the types and logic are quite simple.
@@ -387,58 +390,52 @@ commonAuxiliaries = foldM snoc ([], emptyBag) where
            | otherwise = do (ca, new_stuff) <- m
                             return $ ((rep_tycon, ca) : cas, stuff `unionBags` new_stuff)
 
-
-
--- Prints the representable type family instance
-pprRepTy :: FamInst -> SDoc
-pprRepTy fi
-  = pprFamInstHdr fi <+> ptext (sLit "=") <+> ppr (coAxiomRHS (famInstAxiom fi))
-
 renameDeriv :: Bool
-           -> [InstInfo RdrName]
-           -> Bag (LHsBind RdrName, LSig RdrName)
-           -> TcM (Bag (InstInfo Name), HsValBinds Name, DefUses)
+            -> [InstInfo RdrName]
+            -> Bag (LHsBind RdrName, LSig RdrName)
+            -> TcM (Bag (InstInfo Name), HsValBinds Name, DefUses)
 renameDeriv is_boot inst_infos bagBinds
-  | 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 ( listToBag rn_inst_infos
+  | 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 ( listToBag rn_inst_infos
                  , emptyValBindsOut, usesOnly (plusFVs fvs)) }
 
   | otherwise
-  = discardWarnings $   -- Discard warnings about unused bindings etc
-    do {
+  = discardWarnings $         -- Discard warnings about unused bindings etc
+    setXOptM Opt_EmptyCase $  -- Derived decls (for empty types) can have
+                              --    case x of {}
+    do  {
         -- Bring the extra deriving stuff into scope
         -- before renaming the instances themselves
-       ; (aux_binds, aux_sigs) <- mapAndUnzipBagM return bagBinds
-       ; let aux_val_binds = ValBindsIn aux_binds (bagToList aux_sigs)
-       ; rn_aux_lhs <- rnTopBindsLHS emptyFsEnv aux_val_binds
+        ; (aux_binds, aux_sigs) <- mapAndUnzipBagM return bagBinds
+        ; let aux_val_binds = ValBindsIn aux_binds (bagToList aux_sigs)
+        ; rn_aux_lhs <- rnTopBindsLHS emptyFsEnv aux_val_binds
         ; let bndrs = collectHsValBinders rn_aux_lhs
-       ; bindLocalNames bndrs $ 
-    do { (rn_aux, dus_aux) <- rnValBindsRHS (LocalBindCtxt (mkNameSet bndrs)) rn_aux_lhs
-       ; (rn_inst_infos, fvs_insts) <- mapAndUnzipM rn_inst_info inst_infos
-       ; return (listToBag rn_inst_infos, rn_aux,
+        ; bindLocalNames bndrs $
+    do  { (rn_aux, dus_aux) <- rnValBindsRHS (LocalBindCtxt (mkNameSet bndrs)) rn_aux_lhs
+        ; (rn_inst_infos, fvs_insts) <- mapAndUnzipM rn_inst_info inst_infos
+        ; return (listToBag rn_inst_infos, rn_aux,
                   dus_aux `plusDU` usesOnly (plusFVs fvs_insts)) } }
 
   where
     rn_inst_info :: InstInfo RdrName -> TcM (InstInfo Name, FreeVars)
     rn_inst_info info@(InstInfo { iBinds = NewTypeDerived coi tc })
-       = return ( info { iBinds = NewTypeDerived coi tc }
+        = return ( info { iBinds = NewTypeDerived coi tc }
                  , mkFVs (map dataConName (tyConDataCons tc)))
-         -- See Note [Newtype deriving and unused constructors]
+          -- See Note [Newtype deriving and unused constructors]
 
     rn_inst_info 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
+        =       -- 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 (is_cls_nm inst) (\_ -> []) binds
+              ; let binds' = VanillaInst rn_binds [] standalone_deriv
               ; return (inst_info { iBinds = binds' }, fvs) }
-       where
-         (tyvars,_, clas,_) = instanceHead inst
-         clas_nm            = className clas
+        where
+          (tyvars, _) = tcSplitForAllTys (idType (instanceDFunId inst))
 \end{code}
 
 Note [Newtype deriving and unused constructors]
@@ -462,70 +459,107 @@ stored in NewTypeDerived.
 
 
 %************************************************************************
-%*                                                                     *
-               From HsSyn to DerivSpec
-%*                                                                     *
+%*                                                                      *
+                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 :: Bool
+               -> [LTyClDecl Name]
+               -> [LInstDecl Name]
+               -> [LDerivDecl Name]
+               -> TcM [EarlyDerivSpec]
 makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
-  = do  { eqns1 <- concatMapM (recoverM (return []) . deriveTyDecl) tycl_decls
+  = do  { eqns1 <- concatMapM (recoverM (return []) . deriveTyDecl)   tycl_decls
         ; eqns2 <- concatMapM (recoverM (return []) . deriveInstDecl) inst_decls
         ; eqns3 <- mapAndRecoverM deriveStandalone deriv_decls
         ; let eqns = eqns1 ++ eqns2 ++ eqns3
+
+        -- If AutoDeriveTypeable is set, we automatically add Typeable instances
+        -- for every data type and type class declared in the module
+        ; isAutoTypeable <- xoptM Opt_AutoDeriveTypeable
+        ; let eqns4 = if isAutoTypeable then deriveTypeable tycl_decls eqns else []
+        ; eqns4' <- mapAndRecoverM deriveStandalone eqns4
+        ; let eqns' = eqns ++ eqns4'
+
         ; if is_boot then   -- No 'deriving' at all in hs-boot files
-              do { unless (null eqns) (add_deriv_err (head eqns))
+              do { unless (null eqns') (add_deriv_err (head eqns'))
                  ; return [] }
-          else return eqns }
+          else return eqns' }
   where
-    add_deriv_err eqn 
-       = setSrcSpan loc $
+    deriveTypeable :: [LTyClDecl Name] -> [EarlyDerivSpec] -> [LDerivDecl Name]
+    deriveTypeable tys dss =
+      [ L l (DerivDecl (L l (HsAppTy (noLoc (HsTyVar typeableClassName))
+                                     (L l (HsTyVar (tcdName t))))))
+      | L l t <- tys
+        -- Don't add Typeable instances for type synonyms and type families
+      , not (isSynDecl t), not (isTypeFamilyDecl t)
+        -- ... nor if the user has already given a deriving clause
+      , not (hasInstance (tcdName t) dss) ]
+
+    -- Check if an automatically generated DS for deriving Typeable should be
+    -- ommitted because the user had manually requested for an instance
+    hasInstance :: Name -> [EarlyDerivSpec] -> Bool
+    hasInstance n = any (\ds -> n == tyConName (either ds_tc ds_tc ds))
+
+    add_deriv_err eqn
+       = setSrcSpan (either ds_loc ds_loc eqn) $
          addErr (hang (ptext (sLit "Deriving not permitted in hs-boot file"))
                     2 (ptext (sLit "Use an instance declaration instead")))
-       where
-         loc = case eqn of  { Left ds -> ds_loc ds; Right ds -> ds_loc ds }
 
 ------------------------------------------------------------------
 deriveTyDecl :: LTyClDecl Name -> TcM [EarlyDerivSpec]
-deriveTyDecl (L _ decl@(TyDecl { tcdLName = L _ tc_name
-                               , tcdTyDefn = TyData { td_derivs = Just preds } }))
+deriveTyDecl (L _ decl@(DataDecl { tcdLName = L loc tc_name
+                                 , tcdDataDefn = HsDataDefn { dd_derivs = preds } }))
   = tcAddDeclCtxt decl $
     do { tc <- tcLookupTyCon tc_name
-       ; let tvs = tyConTyVars tc
-             tys = mkTyVarTys tvs
-       ; mapM (deriveTyData tvs tc tys) preds }
+       ; let tvs  = tyConTyVars tc
+             tys  = mkTyVarTys tvs
+             pdcs :: [LDerivDecl Name]
+             pdcs = [ L loc (DerivDecl (L loc (HsAppTy (noLoc (HsTyVar typeableClassName))
+                                       (L loc (HsTyVar (tyConName pdc))))))
+                    | Just pdc <- map promoteDataCon_maybe (tyConDataCons tc) ]
+        -- If AutoDeriveTypeable and DataKinds is set, we add Typeable instances
+        -- for every promoted data constructor of datatypes in this module
+       ; isAutoTypeable <- xoptM Opt_AutoDeriveTypeable
+       ; isDataKinds    <- xoptM Opt_DataKinds
+       ; prom_dcs_Typeable_instances <- if isAutoTypeable && isDataKinds
+                                        then mapM deriveStandalone pdcs
+                                        else return []
+       ; other_instances <- case preds of
+                              Just preds' -> mapM (deriveTyData tvs tc tys) preds'
+                              Nothing     -> return []
+       ; return (prom_dcs_Typeable_instances ++ other_instances) }
 
 deriveTyDecl _ = return []
 
 ------------------------------------------------------------------
 deriveInstDecl :: LInstDecl Name -> TcM [EarlyDerivSpec]
-deriveInstDecl (L _ (FamInstD { lid_inst = fam_inst }))
+deriveInstDecl (L _ (TyFamInstD {})) = return []
+deriveInstDecl (L _ (DataFamInstD { dfid_inst = fam_inst }))
   = deriveFamInst fam_inst
-deriveInstDecl (L _ (ClsInstD { cid_fam_insts = fam_insts }))
+deriveInstDecl (L _ (ClsInstD { cid_inst = ClsInstDecl { cid_datafam_insts = fam_insts } }))
   = concatMapM (deriveFamInst . unLoc) fam_insts
 
 ------------------------------------------------------------------
-deriveFamInst :: FamInstDecl Name -> TcM [EarlyDerivSpec]
-deriveFamInst decl@(FamInstDecl { fid_tycon = L _ tc_name, fid_pats = pats
-                                , fid_defn = TyData { td_derivs = Just preds } })
-  = tcAddFamInstCtxt decl $
+deriveFamInst :: DataFamInstDecl Name -> TcM [EarlyDerivSpec]
+deriveFamInst decl@(DataFamInstDecl { dfid_tycon = L _ tc_name, dfid_pats = pats
+                                    , dfid_defn = HsDataDefn { dd_derivs = Just preds } })
+  = tcAddDataFamInstCtxt decl $
     do { fam_tc <- tcLookupTyCon tc_name
-       ; tcFamTyPats fam_tc pats (\_ -> return ()) $ \ tvs' pats' _ ->
-         mapM (deriveTyData tvs' fam_tc pats') preds }
-       -- 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.
+       ; tcFamTyPats tc_name (tyConKind fam_tc) pats (\_ -> return ()) $
+         \ tvs' pats' _ ->
+           mapM (deriveTyData tvs' fam_tc pats') preds }
+        -- 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.
 
 deriveFamInst _ = return []
 
@@ -544,7 +578,8 @@ deriveStandalone (L loc (DerivDecl deriv_ty))
               , text "theta:" <+> ppr theta
               , text "cls:" <+> ppr cls
               , text "tys:" <+> ppr inst_tys ]
-               -- C.f. TcInstDcls.tcLocalInstDecl1
+                -- C.f. TcInstDcls.tcLocalInstDecl1
+       ; checkTc (not (null inst_tys)) derivingNullaryErr
 
        ; let cls_tys = take (length inst_tys - 1) inst_tys
              inst_ty = last inst_tys
@@ -556,148 +591,226 @@ deriveStandalone (L loc (DerivDecl deriv_ty))
                    (Just theta) }
 
 ------------------------------------------------------------------
-deriveTyData :: [TyVar] -> TyCon -> [Type] 
-             -> LHsType Name           -- The deriving predicate
+deriveTyData :: [TyVar] -> TyCon -> [Type]   -- LHS of data or data instance
+             -> LHsType Name                 -- The deriving predicate
              -> TcM EarlyDerivSpec
 -- The deriving clause of a data or newtype declaration
 deriveTyData tvs tc tc_args (L loc deriv_pred)
-  = setSrcSpan loc     $       -- Use the location of the 'deriving' item
-    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
-  
-        ; traceTc "derivTyData" (pprTvBndrs tvs $$ ppr tc $$ ppr tc_args $$ 
-                     pprTvBndrs (varSetElems $ tyVarsOfTypes tc_args) $$ ppr inst_ty)
-
-       -- 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 (varSetElemsKvsFirst univ_tvs) cls cls_tys inst_ty Nothing } 
-\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
+  = setSrcSpan loc     $        -- Use the location of the 'deriving' item
+    tcExtendTyVarEnv tvs $      -- Deriving preds may (now) mention
+                                -- the type variables for the type constructor
 
-When type familes are involved it's trickier:
+    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]).
 
-    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
+                -- Typeable is special
+        ; if className cls == typeableClassName
+          then do {
+        ; dflags <- getDynFlags
+        ; case checkTypeableConditions (dflags, tc, tc_args) of
+               Just err -> failWithTc (derivingThingErr False cls cls_tys
+                                         (mkTyConApp tc tc_args) err)
+               Nothing  -> mkEqnHelp DerivOrigin tvs cls cls_tys
+                             (mkTyConApp tc (kindVarsOnly tc_args)) Nothing }
+          else do {
+
+        -- 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
+        ; checkTc (not (null cls_tyvars)) derivingNullaryErr
+
+        ; let 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    = tyVarsOfTypes args_to_drop
+              univ_tvs       = (mkVarSet tvs `extendVarSetList` deriv_tvs)
+                                             `minusVarSet` dropped_tvs
+
+        ; traceTc "derivTyData" (pprTvBndrs tvs $$ ppr tc $$ ppr tc_args $$
+                     pprTvBndrs (varSetElems $ tyVarsOfTypes tc_args) $$ ppr inst_ty)
 
-    instance Eq [a] => Eq (T Int a)    -- easy by coercion
-    instance Monad [] => Monad (T Int) -- only if we can eta reduce???
+        -- 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 (all isTyVarTy args_to_drop &&                         -- (a)
+                   sizeVarSet dropped_tvs == n_args_to_drop &&           -- (b)
+                   tyVarsOfTypes (inst_ty:cls_tys) `subVarSet` univ_tvs) -- (c)
+                  (derivingEtaErr cls cls_tys inst_ty)
+                -- Check that
+                --  (a) The args to drop are all type variables; eg reject:
+                --              data instance T a Int = .... deriving( Monad )
+                --  (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 )
+
+        ; mkEqnHelp DerivOrigin (varSetElemsKvsFirst univ_tvs) cls cls_tys inst_ty Nothing } }
+  where
+    kindVarsOnly :: [Type] -> [Type]
+    kindVarsOnly [] = []
+    kindVarsOnly (t:ts) | Just v <- getTyVar_maybe t
+                        , isKindVar v = t : kindVarsOnly ts
+                        | otherwise   =     kindVarsOnly ts
+\end{code}
 
-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)
+          -> 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])
+--      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
+  , className cls == typeableClassName || isAlgTyCon tycon
+  -- Avoid functions, primitive types, etc, unless it's Typeable
   = mk_alg_eqn tycon tc_args
+
   | otherwise
   = failWithTc (derivingThingErr False cls cls_tys tc_app
-              (ptext (sLit "The last argument of the instance must be a data or newtype application")))
+               (ptext (sLit "The last argument of the instance must be a data or newtype application")))
 
   where
      bale_out msg = failWithTc (derivingThingErr False cls cls_tys tc_app msg)
 
      mk_alg_eqn tycon tc_args
-      | className cls `elem` typeableClassNames
+      | className cls `elem` oldTypeableClassNames
       = do { dflags <- getDynFlags
-           ; case checkTypeableConditions (dflags, tycon, tc_args) of
+           ; case checkOldTypeableConditions (dflags, tycon, tc_args) of
                Just err -> bale_out err
-               Nothing  -> mk_typeable_eqn orig tvs cls tycon tc_args mtheta }
+               Nothing  -> mkOldTypeableEqn orig tvs cls tycon tc_args mtheta }
 
-      | isDataFamilyTyCon tycon
-      , length tc_args /= tyConArity tycon
-      = bale_out (ptext (sLit "Unsaturated data family application"))
+      | className cls == typeableClassName
+      -- We checked for errors before, so we don't need to do that again
+      = mkPolyKindedTypeableEqn orig tvs cls cls_tys tycon tc_args mtheta
 
       | otherwise
-      = 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.
-          ; rdr_env <- getGlobalRdrEnv
-          ; let hidden_data_cons = not (isWiredInName (tyConName rep_tc)) &&
-                                    (isAbstractTyCon rep_tc || 
-                                     any not_in_scope (tyConDataCons rep_tc))
-                not_in_scope dc  = null (lookupGRE_Name rdr_env (dataConName dc))
-          ; unless (isNothing mtheta || not hidden_data_cons)
-                   (bale_out (derivingHiddenErr tycon))
-
-          ; dflags <- getDynFlags
-          ; 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 }
+      = do { (rep_tc, rep_tc_args) <- lookup_data_fam 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.
+           ; rdr_env <- getGlobalRdrEnv
+           ; let data_con_names = map dataConName (tyConDataCons rep_tc)
+                 hidden_data_cons = not (isWiredInName (tyConName rep_tc)) &&
+                                    (isAbstractTyCon rep_tc ||
+                                     any not_in_scope data_con_names)
+                 not_in_scope dc  = null (lookupGRE_Name rdr_env dc)
+
+                 -- Make a Qual RdrName that will do for each DataCon
+                 -- so we can report it as used (Trac #7969)
+                 data_con_rdrs = [ mkRdrQual (is_as (is_decl imp_spec)) occ
+                                 | dc_name <- data_con_names
+                                 , let occ  = nameOccName dc_name
+                                       gres = lookupGRE_Name rdr_env dc_name
+                                 , not (null gres)
+                                 , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
+
+           ; addUsedRdrNames data_con_rdrs
+           ; unless (isNothing mtheta || not hidden_data_cons)
+                    (bale_out (derivingHiddenErr tycon))
+
+           ; dflags <- getDynFlags
+           ; 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 }
+
+     lookup_data_fam :: TyCon -> [Type] -> TcM (TyCon, [Type])
+     -- Find the instance of a data family
+     -- Note [Looking up family instances for deriving]
+     lookup_data_fam tycon tys
+       | not (isFamilyTyCon tycon)
+       = return (tycon, tys)
+       | otherwise
+       = ASSERT( isAlgTyCon tycon )
+         do { maybeFamInst <- tcLookupFamInst tycon tys
+            ; case maybeFamInst of
+                Nothing -> bale_out (ptext (sLit "No family instance for")
+                                     <+> quotes (pprTypeApp tycon tys))
+                Just (FamInstMatch { fim_instance = famInst
+                                   , fim_tys      = tys })
+                  -> let tycon' = dataFamInstRepTyCon famInst
+                     in return (tycon', tys) }
 \end{code}
 
+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 declarations.
+
+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)
+    --  :Co:RT    :: :RT ~ []          -- Eta-reduced!
+    --  :CoF:RT a :: T Int a ~ :RT a   -- Also eta-reduced!
+
+    instance Eq [a] => Eq (T Int a)     -- easy by coercion
+       -- d1 :: Eq [a]
+       -- d2 :: Eq (T Int a) = d1 |> Eq (sym (:Co:RT a ; :coF:RT a))
+
+    instance Monad [] => Monad (T Int)  -- only if we can eta reduce???
+       -- d1 :: Monad []
+       -- d2 :: Monad (T Int) = d1 |> Monad (sym (:Co:RT ; :coF:RT))
+
+Note the need for the eta-reduced rule axioms.  After all, we can
+write it out
+    instance Monad [] => Monad (T Int)  -- only if we can eta reduce???
+      return x = MkT [x]
+      ... etc ...
+
+See Note [Eta reduction for data family axioms] in TcInstDcls.
+
 
 %************************************************************************
-%*                                                                     *
-               Deriving data types
-%*                                                                     *
+%*                                                                      *
+                Deriving data types
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
@@ -707,7 +820,7 @@ mkDataTypeEqn :: CtOrigin
               -> 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)
+                                        --    (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
@@ -717,79 +830,106 @@ mkDataTypeEqn :: CtOrigin
 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 rep_tc_args of
-       -- NB: pass the *representation* tycon to checkSideConditions
-       CanDerive               -> go_for_it
-       NonDerivableClass       -> bale_out (nonStdErr cls)
-       DerivableClassError msg -> bale_out msg
+        -- 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)
 
 mk_data_eqn :: CtOrigin -> [TyVar] -> Class
-           -> TyCon -> [TcType] -> TyCon -> [TcType] -> DerivContext
-           -> TcM EarlyDerivSpec
+            -> TyCon -> [TcType] -> TyCon -> [TcType] -> DerivContext
+            -> TcM EarlyDerivSpec
 mk_data_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
-  = do { loc                  <- getSrcSpanM
-       ; dfun_name            <- new_dfun_name cls tycon
-       ; inferred_constraints <- inferConstraints cls inst_tys rep_tc rep_tc_args
-       ; let 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
+  = do  { loc                  <- getSrcSpanM
+        ; dfun_name            <- new_dfun_name cls tycon
+        ; inferred_constraints <- inferConstraints cls inst_tys rep_tc rep_tc_args
+        ; let 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
   where
     inst_tys = [mkTyConApp tycon tc_args]
 
 ----------------------
-mk_typeable_eqn :: CtOrigin -> [TyVar] -> Class
-               -> TyCon -> [TcType] -> DerivContext
-               -> TcM EarlyDerivSpec
-mk_typeable_eqn orig tvs cls tycon 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)
+mkOldTypeableEqn :: CtOrigin -> [TyVar] -> Class
+                    -> TyCon -> [TcType] -> DerivContext
+                    -> TcM EarlyDerivSpec
+-- The "old" (pre GHC 7.8 polykinded Typeable) deriving Typeable
+-- used a horrid family of classes: Typeable, Typeable1, Typeable2, ... Typeable7
+mkOldTypeableEqn orig tvs cls tycon 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` oldTypeableClassKey)
+                  (ptext (sLit "Use deriving( Typeable ) on a data type declaration"))
+        ; real_cls <- tcLookupClass (oldTypeableClassNames `getNth` tyConArity tycon)
                       -- See Note [Getting base classes]
-       ; mk_typeable_eqn orig tvs real_cls tycon [] (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 = tycon, ds_tc_args = []
-                    , ds_theta = mtheta `orElse` [], ds_newtype = False })  }
+        ; mkOldTypeableEqn orig tvs real_cls tycon [] (Just []) }
+
+  | otherwise           -- standalone 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 = tycon, ds_tc_args = []
+                     , ds_theta = mtheta `orElse` [], ds_newtype = False })  }
+
+mkPolyKindedTypeableEqn :: CtOrigin -> [TyVar] -> Class -> [TcType]
+                        -> TyCon -> [TcType] -> DerivContext
+                        -> TcM EarlyDerivSpec
+mkPolyKindedTypeableEqn orig tvs cls _cls_tys tycon tc_args mtheta
+  -- The kind-polymorphic Typeable class is less special; namely, there is no
+  -- need to select the class with the right kind anymore, as we only have one.
+  = do  { checkTc (all is_kind_var tc_args)
+                  (ptext (sLit "Derived typeable instance must be of form (Typeable")
+                        <+> ppr tycon <> rparen)
+        ; dfun_name <- new_dfun_name cls tycon
+        ; loc <- getSrcSpanM
+        ; let tc_app = mkTyConApp tycon tc_args
+        ; return (Right $
+                  DS { ds_loc = loc, ds_orig = orig, ds_name = dfun_name
+                     , ds_tvs = filter isKindVar tvs, ds_cls = cls
+                     , ds_tys = typeKind tc_app : [tc_app]
+                         -- Remember, Typeable :: forall k. k -> *
+                     , ds_tc = tycon, ds_tc_args = tc_args
+                     , ds_theta = mtheta `orElse` []  -- Context is empty for polykinded Typeable
+                     , ds_newtype = False })  }
+  where
+    is_kind_var tc_arg = case tcGetTyVar_maybe tc_arg of
+                           Just v  -> isKindVar v
+                           Nothing -> False
 
 ----------------------
 inferConstraints :: Class -> [TcType]
-                 -> TyCon -> [TcType] 
+                 -> TyCon -> [TcType]
                  -> TcM 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
   | cls `hasKey` genClassKey    -- Generic constraints are easy
-  = return [] 
+  = return []
 
   | cls `hasKey` gen1ClassKey   -- Gen1 needs Functor
-  = ASSERT (length rep_tc_tvs > 0)   -- See Note [Getting base classes]
+  = ASSERT(length rep_tc_tvs > 0)   -- See Note [Getting base classes]
     do { functorClass <- tcLookupClass functorClassName
        ; return (con_arg_constraints functorClass (get_gen1_constrained_tys last_tv)) }
 
@@ -797,7 +937,7 @@ inferConstraints cls inst_tys rep_tc rep_tc_args
   = ASSERT2( equalLength rep_tc_tvs all_rep_tc_args, ppr cls <+> ppr rep_tc )
     return (stupid_constraints ++ extra_constraints
             ++ sc_constraints
-            ++ con_arg_constraints cls get_std_constrained_tys) 
+            ++ con_arg_constraints cls get_std_constrained_tys)
 
   where
        -- Constraints arising from the arguments of each constructor
@@ -805,46 +945,46 @@ inferConstraints cls inst_tys rep_tc rep_tc_args
       = [ 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,
+                        get_constrained_tys $
+                        dataConInstOrigArgTys data_con all_rep_tc_args,
           not (isUnLiftedType arg_ty) ]
-               -- No constraints for unlifted types
-               -- See Note [Deriving and unboxed types]
+                -- No constraints for unlifted types
+                -- See Note [Deriving and unboxed types]
 
-               -- 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
+                -- 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_std_constrained_tys :: [Type] -> [Type]
     get_std_constrained_tys tys
         | is_functor_like = concatMap (deepSubtypesContaining last_tv) tys
-       | otherwise       = tys
+        | otherwise       = tys
 
     rep_tc_tvs = tyConTyVars rep_tc
     last_tv = last rep_tc_tvs
     all_rep_tc_args | cls `hasKey` gen1ClassKey || is_functor_like
                       = rep_tc_args ++ [mkTyVarTy last_tv]
-                   | otherwise       = rep_tc_args
+                    | otherwise       = rep_tc_args
 
-       -- Constraints arising from superclasses
-       -- See Note [Superclasses of derived instance]
+        -- Constraints arising from superclasses
+        -- See Note [Superclasses of derived instance]
     sc_constraints = substTheta (zipOpenTvSubst (classTyVars cls) inst_tys)
-                               (classSCTheta cls)
+                                (classSCTheta cls)
 
-       -- Stupid constraints
+        -- 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 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
@@ -856,22 +996,16 @@ inferConstraints cls inst_tys rep_tc rep_tc_args
 Note [Getting base classes]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Functor and Typeable are defined in package 'base', and that is not available
-when compiling 'ghc-prim'.  So we must be careful that 'deriving' for stuff in 
+when compiling 'ghc-prim'.  So we must be careful that 'deriving' for stuff in
 ghc-prim does not use Functor or Typeable implicitly via these lookups.
 
 Note [Deriving and unboxed types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We have some special hacks to support things like
-   data T = MkT Int# deriving( Ord, Show )
-
-Specifically
-  * For Show we use TcGenDeriv.box_if_necy to box the Int# into an Int
-    (which we know how to show)
-
-  * For Eq, Ord, we ust TcGenDeriv.primOrdOps to give Ord operations
-    on some primitive types
+   data T = MkT Int# deriving ( Show )
 
-It's all a bit ad hoc.
+Specifically, we use TcGenDeriv.box_if_necy to box the Int# into an Int
+(which we know how to show). It's a bit ad hoc.
 
 
 \begin{code}
@@ -884,8 +1018,8 @@ It's all a bit ad hoc.
 -- family tycon (with indexes) in error messages.
 
 data DerivStatus = CanDerive
-                | DerivableClassError SDoc     -- Standard class, but can't do it
-                | NonDerivableClass            -- Non-standard class
+                 | DerivableClassError SDoc  -- Standard class, but can't do it
+                 | NonDerivableClass         -- Non-standard class
 
 checkSideConditions :: DynFlags -> DerivContext -> Class -> [TcType]
                     -> TyCon -> [Type] -- tycon and its parameters
@@ -893,38 +1027,39 @@ checkSideConditions :: DynFlags -> DerivContext -> Class -> [TcType]
 checkSideConditions dflags mtheta cls cls_tys rep_tc rep_tc_args
   | Just cond <- sideConditions mtheta cls
   = case (cond (dflags, rep_tc, rep_tc_args)) 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
+        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")
+    ty_args_why = quotes (ppr (mkClassPred cls cls_tys)) <+> ptext (sLit "is not a class")
 
-checkTypeableConditions :: Condition
-checkTypeableConditions = checkFlag Opt_DeriveDataTypeable `andCond` cond_typeableOK
+checkTypeableConditions, checkOldTypeableConditions :: Condition
+checkTypeableConditions    = checkFlag Opt_DeriveDataTypeable `andCond` cond_TypeableOK
+checkOldTypeableConditions = checkFlag Opt_DeriveDataTypeable `andCond` cond_oldTypeableOK
 
 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 `andCond` cond_args cls)
-  | cls_key == ordClassKey                = Just (cond_std `andCond` cond_args cls)
-  | cls_key == showClassKey               = Just (cond_std `andCond` cond_args cls)
-  | cls_key == readClassKey               = Just (cond_std `andCond` cond_args cls)
-  | cls_key == enumClassKey               = Just (cond_std `andCond` cond_isEnumeration)
-  | cls_key == ixClassKey                 = Just (cond_std `andCond` cond_enumOrProduct cls)
-  | cls_key == boundedClassKey            = Just (cond_std `andCond` cond_enumOrProduct cls)
-  | cls_key == dataClassKey               = Just (checkFlag Opt_DeriveDataTypeable `andCond`
+  | cls_key == eqClassKey          = Just (cond_std `andCond` cond_args cls)
+  | cls_key == ordClassKey         = Just (cond_std `andCond` cond_args cls)
+  | cls_key == showClassKey        = Just (cond_std `andCond` cond_args cls)
+  | cls_key == readClassKey        = Just (cond_std `andCond` cond_args cls)
+  | cls_key == enumClassKey        = Just (cond_std `andCond` cond_isEnumeration)
+  | cls_key == ixClassKey          = Just (cond_std `andCond` cond_enumOrProduct cls)
+  | cls_key == boundedClassKey     = Just (cond_std `andCond` cond_enumOrProduct cls)
+  | cls_key == dataClassKey        = Just (checkFlag Opt_DeriveDataTypeable `andCond`
                                            cond_std `andCond` cond_args cls)
-  | 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 == 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)
+                                           cond_functorOK False)
   | cls_key == genClassKey         = Just (cond_RepresentableOk `andCond`
                                            checkFlag Opt_DeriveGeneric)
   | cls_key == gen1ClassKey        = Just (cond_Representable1Ok `andCond`
@@ -944,26 +1079,26 @@ type Condition = (DynFlags, TyCon, [Type]) -> Maybe SDoc
 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 "  or") $$ y)
-                                   -- Both fail
+        Nothing -> Nothing          -- c1 succeeds
+        Just x  -> case c2 tc of    -- c1 fails
+                     Nothing -> Nothing
+                     Just y  -> Just (x $$ ptext (sLit "  or") $$ 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
+                     Nothing -> c2 tc   -- c1 succeeds
+                     Just x  -> Just x  -- c1 fails
 
 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
+  = 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
+  | otherwise           = Nothing
   where
     suggestion  = ptext (sLit "Possible fix: use a standalone deriving declaration instead")
     data_cons   = tyConDataCons rep_tc
@@ -977,7 +1112,7 @@ cond_stdOK Nothing (_, rep_tc, _)
 
 no_cons_why :: TyCon -> SDoc
 no_cons_why rep_tc = quotes (pprSourceTyCon rep_tc) <+>
-                    ptext (sLit "must have at least one data constructor")
+                     ptext (sLit "must have at least one data constructor")
 
 cond_RepresentableOk :: Condition
 cond_RepresentableOk (_, tc, tc_args) = canDoGenerics tc tc_args
@@ -987,7 +1122,7 @@ cond_Representable1Ok (_, tc, tc_args) = canDoGenerics1 tc tc_args
 
 cond_enumOrProduct :: Class -> Condition
 cond_enumOrProduct cls = cond_isEnumeration `orCond`
-                        (cond_isProduct `andCond` cond_args cls)
+                         (cond_isProduct `andCond` cond_args cls)
 
 cond_args :: Class -> Condition
 -- For some classes (eg Eq, Ord) we allow unlifted arg types
@@ -999,9 +1134,9 @@ cond_args cls (_, tc, _)
                          2 (ptext (sLit "for type") <+> quotes (ppr ty)))
   where
     bad_args = [ arg_ty | con <- tyConDataCons tc
-                       , arg_ty <- dataConOrigArgTys con
-                       , isUnLiftedType arg_ty
-                       , not (ok_ty arg_ty) ]
+                        , arg_ty <- dataConOrigArgTys con
+                        , isUnLiftedType arg_ty
+                        , not (ok_ty arg_ty) ]
 
     cls_key = classKey cls
     ok_ty arg_ty
@@ -1016,36 +1151,50 @@ cond_args cls (_, tc, _)
 
 cond_isEnumeration :: Condition
 cond_isEnumeration (_, rep_tc, _)
-  | isEnumerationTyCon rep_tc   = Nothing
-  | otherwise                  = Just why
+  | isEnumerationTyCon rep_tc = Nothing
+  | otherwise                 = Just why
   where
     why = sep [ quotes (pprSourceTyCon rep_tc) <+>
-                 ptext (sLit "must be an enumeration type")
+                  ptext (sLit "must be an enumeration type")
               , ptext (sLit "(an enumeration consists of one or more nullary, non-GADT constructors)") ]
-                 -- See Note [Enumeration types] in TyCon
+                  -- See Note [Enumeration types] in TyCon
 
 cond_isProduct :: Condition
 cond_isProduct (_, rep_tc, _)
   | isProductTyCon rep_tc = Nothing
-  | otherwise            = Just why
+  | otherwise             = Just why
   where
     why = quotes (pprSourceTyCon rep_tc) <+>
-         ptext (sLit "must have precisely one constructor")
+          ptext (sLit "must have precisely one constructor")
 
-cond_typeableOK :: Condition
--- OK for Typeable class
+cond_oldTypeableOK :: Condition
+-- OK for kind-monomorphic Typeable class
 -- Currently: (a) args all of kind *
---           (b) 7 or fewer args
-cond_typeableOK (_, tc, _)
+--            (b) 7 or fewer args
+cond_oldTypeableOK (_, tc, _)
   | tyConArity tc > 7 = Just too_many
   | not (all (isSubOpenTypeKind . tyVarKind) (tyConTyVars tc))
                       = Just bad_kind
-  | otherwise        = Nothing
+  | otherwise         = Nothing
   where
     too_many = quotes (pprSourceTyCon tc) <+>
-              ptext (sLit "must have 7 or fewer arguments")
+               ptext (sLit "must have 7 or fewer arguments")
     bad_kind = quotes (pprSourceTyCon tc) <+>
-              ptext (sLit "must only have arguments of kind `*'")
+               ptext (sLit "must only have arguments of kind `*'")
+
+cond_TypeableOK :: Condition
+-- Only not ok if it's a data instance
+cond_TypeableOK (_, tc, tc_args)
+  | isDataFamilyTyCon tc && not (null tc_args)
+  = Just no_families
+
+  | otherwise
+  = Nothing
+  where
+    no_families = sep [ ptext (sLit "Deriving Typeable is not allowed for family instances;")
+                      , ptext (sLit "derive Typeable for")
+                          <+> quotes (pprSourceTyCon tc)
+                          <+> ptext (sLit "alone") ]
 
 functorLikeClassKeys :: [Unique]
 functorLikeClassKeys = [functorClassKey, foldableClassKey, traversableClassKey]
@@ -1067,7 +1216,7 @@ cond_functorOK allowFunctions (_, rep_tc, _)
           <+> ptext (sLit "must not have a class context") <+> pprTheta bad_stupid_theta)
 
   | otherwise
-  = msum (map check_con data_cons)     -- msum picks the first 'Just', if any
+  = 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
@@ -1079,12 +1228,12 @@ cond_functorOK allowFunctions (_, rep_tc, _)
 
     check_vanilla :: DataCon -> Maybe SDoc
     check_vanilla con | isVanillaDataCon con = Nothing
-                     | otherwise            = Just (badCon con existential)
+                      | 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
+                      , 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
@@ -1092,9 +1241,9 @@ cond_functorOK allowFunctions (_, rep_tc, _)
                       , ft_forall = \_ x   -> x }
 
     existential = ptext (sLit "must not have existential arguments")
-    covariant  = ptext (sLit "must not use the type variable in a function argument")
-    functions  = ptext (sLit "must not contain function types")
-    wrong_arg  = ptext (sLit "must use the type variable only as the last argument of a data type")
+    covariant   = ptext (sLit "must not use the type variable in a function argument")
+    functions   = ptext (sLit "must not contain function types")
+    wrong_arg   = ptext (sLit "must use the type variable only as the last argument of a data type")
 
 checkFlag :: ExtensionFlag -> Condition
 checkFlag flag (dflags, _, _)
@@ -1113,8 +1262,8 @@ std_class_via_iso :: Class -> Bool
 -- 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
+        -- Not Read/Show because they respect the type
+        -- Not Enum, because newtypes are never in Enum
 
 
 non_iso_class :: Class -> Bool
@@ -1122,17 +1271,18 @@ non_iso_class :: Class -> Bool
 -- even with -XGeneralizedNewtypeDeriving
 non_iso_class cls
   = classKey cls `elem` ([ readClassKey, showClassKey, dataClassKey
-                         , genClassKey, gen1ClassKey] ++ typeableClassKeys)
+                         , genClassKey, gen1ClassKey, typeableClassKey]
+                         ++ oldTypeableClassKeys)
 
-typeableClassKeys :: [Unique]
-typeableClassKeys = map getUnique typeableClassNames
+oldTypeableClassKeys :: [Unique]
+oldTypeableClassKeys = map getUnique oldTypeableClassNames
 
 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
+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
@@ -1142,7 +1292,7 @@ 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 )
+        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
@@ -1157,16 +1307,16 @@ be satisfied too.  But not always; consider:
 
 The derived instance for (Ord (T a)) must have a (Num a) constraint!
 Similarly consider:
-       data T a = MkT deriving( Data, Typeable )
+        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 ...
+        instance Typable a => Data (T a) where ...
 
 
 %************************************************************************
-%*                                                                     *
-               Deriving newtypes
-%*                                                                     *
+%*                                                                      *
+                Deriving newtypes
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
@@ -1178,150 +1328,164 @@ 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 = varSetElemsKvsFirst 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) }
+  = 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 = varSetElemsKvsFirst 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 rep_tc_args of
-      CanDerive -> go_for_it   -- Use the standard H98 method
-      DerivableClassError msg  -- Error with standard class
+      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
+      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
+        | 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)
+        bale_out msg     = failWithTc (derivingThingErr newtype_deriving cls cls_tys inst_ty msg)
 
-       non_std    = nonStdErr cls
+        non_std    = nonStdErr cls
         suggest_nd = 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, ...)
-       -- where t is a type,
-       --       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)).
-       --                C s1 .. sm t => C s1 .. sm (T a1...ak)
-       -- where T a1...ap is the partial application of
-       --       the LHS of the correct kind and p >= k
-       --
-       --      NB: the variables below are:
-       --              tc_tvs = [a1, ..., an]
-       --              tyvars_to_keep = [a1, ..., ak]
-       --              rep_ty = t ak .. an
-       --              deriv_tvs = fvs(s1..sm) \ tc_tvs
-       --              tys = [s1, ..., sm]
-       --              rep_fn' = t
-       --
-       -- Running example: newtype T s a = MkT (ST s a) deriving( Monad )
-       -- We generate the instance
-       --      instance Monad (ST s) => Monad (T s) where
-
-       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!
-       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
+        -- 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, 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)).
+        --                C s1 .. sm t => C s1 .. sm (T a1...ak)
+        -- where T a1...ap is the partial application of
+        --       the LHS of the correct kind and p >= k
+        --
+        --      NB: the variables below are:
+        --              tc_tvs = [a1, ..., an]
+        --              tyvars_to_keep = [a1, ..., ak]
+        --              rep_ty = t ak .. an
+        --              deriv_tvs = fvs(s1..sm) \ tc_tvs
+        --              tys = [s1, ..., sm]
+        --              rep_fn' = t
+        --
+        -- Running example: newtype T s a = MkT (ST s a) deriving( Monad )
+        -- We generate the instance
+        --      instance Monad (ST s) => Monad (T s) where
+
+        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!
+        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
 
 
     -- Next we figure out what superclass dictionaries to use
     -- See Note [Newtype deriving superclasses] above
 
-       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
-               -- Example:     newtype T = MkT Int deriving( C )
-               -- We get the derived instance
-               --              instance C T
-               -- rather than
-               --              instance C Int => C T
-       all_preds = rep_pred : sc_theta         -- NB: rep_pred comes first
-
-       -------------------------------------------------------------------
-       --  Figuring out whether we can only do this newtype-deriving thing
-
-       can_derive_via_isomorphism
-          =  not (non_iso_class cls)
-          && arity_ok
-          && eta_ok
-          && ats_ok
---        && not (isRecursiveTyCon tycon)      -- Note [Recursive newtypes]
-
-       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 = 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 ]
+        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
+                -- Example:     newtype T = MkT Int deriving( C )
+                -- We get the derived instance
+                --              instance C T
+                -- rather than
+                --              instance C Int => C T
+        all_preds = rep_pred : sc_theta         -- NB: rep_pred comes first
+
+        -------------------------------------------------------------------
+        --  Figuring out whether we can only do this newtype-deriving thing
+
+        can_derive_via_isomorphism
+           =  not (non_iso_class cls)
+           && arity_ok
+           && eta_ok
+           && ats_ok
+           && roles_ok
+--         && not (isRecursiveTyCon tycon)      -- Note [Recursive newtypes]
+
+        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 = 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
+
+        roles_ok = let cls_roles = tyConRoles (classTyCon cls) in
+                   not (null cls_roles) && last cls_roles /= Nominal
+               -- We must make sure that the class definition (and all its
+               -- members) never pattern-match on the last parameter.
+               -- See Trac #1496 and Note [Roles] in Coercion
+
+        cant_derive_err
+           = vcat [ ppUnless arity_ok arity_msg
+                  , ppUnless eta_ok eta_msg
+                  , ppUnless ats_ok ats_msg
+                  , ppUnless roles_ok roles_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")
+        eta_msg   = ptext (sLit "cannot eta-reduce the representation type enough")
+        ats_msg   = ptext (sLit "the class has associated types")
+        roles_msg = ptext (sLit "it is not type-safe to use") <+>
+                    ptext (sLit "GeneralizedNewtypeDeriving on this class;") $$
+                    ptext (sLit "the last parameter of") <+>
+                    quotes (ppr (className cls)) <+>
+                    ptext (sLit "is at role Nominal")
+
 \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 )
+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.
@@ -1329,14 +1493,14 @@ 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!
+   instance Eq [A] => Eq A      -- Makes typechecker loop!
 But now we require a simple context, so it's ok.
 
 
 %************************************************************************
-%*                                                                     *
+%*                                                                      *
 \subsection[TcDeriv-fixpoint]{Finding the fixed point of \tr{deriving} equations}
-%*                                                                     *
+%*                                                                      *
 %************************************************************************
 
 A ``solution'' (to one of the equations) is a list of (k,TyVarTy tv)
@@ -1359,73 +1523,73 @@ inferInstanceContexts :: OverlapFlag -> [DerivSpec] -> TcM [DerivSpec]
 inferInstanceContexts _ [] = return []
 
 inferInstanceContexts oflag infer_specs
-  = do { traceTc "inferInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
-       ; iterate_deriv 1 initial_solutions }
+  = 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.
+        -- The initial solutions for the equations claim that each
+        -- instance has an empty context; this solution is certainly
+        -- in canonical form.
     initial_solutions :: [ThetaType]
     initial_solutions = [ [] | _ <- infer_specs ]
 
     ------------------------------------------------------------------
-       -- 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
+        -- 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
     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 -XUndecidableInstances
-               -- (See TcSimplify.tcSimplifyDeriv.)
+      | n > 20  -- Looks as if we are in an infinite loop
+                -- This can happen if we have -XUndecidableInstances
+                -- (See TcSimplify.tcSimplifyDeriv.)
       = pprPanic "solveDerivEqns: probable loop"
-                (vcat (map pprDerivSpec infer_specs) $$ ppr current_solns)
+                 (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" (mkInstance oflag)
-                                          current_solns infer_specs
-          ; new_solns <- checkNoErrs $
-                         extendLocalInstEnv inst_specs $
-                         mapM gen_soln infer_specs
+      = do {      -- Extend the inst info from the explicit instance decls
+                  -- with the current set of solutions, and simplify each RHS
+             inst_specs <- zipWithM (mkInstance oflag) current_solns infer_specs
+           ; new_solns <- checkNoErrs $
+                          extendLocalInstEnv inst_specs $
+                          mapM gen_soln infer_specs
 
            ; let eqList :: (a -> b -> Bool) -> [a] -> [b] -> Bool
                  eqList f xs ys = length xs == length ys && and (zipWith f xs ys)
 
-          ; if (eqList (eqList eqType) current_solns new_solns) then
-               return [ spec { ds_theta = soln }
+           ; if (eqList (eqList eqType) current_solns new_solns) then
+                return [ spec { ds_theta = soln }
                        | (spec, soln) <- zip infer_specs current_solns ]
-            else
-               iterate_deriv (n+1) new_solns }
+             else
+                iterate_deriv (n+1) new_solns }
 
     ------------------------------------------------------------------
     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 $
-       addErrCtxt (derivInstCtxt the_pred) $
-       do { theta <- simplifyDeriv orig the_pred tyvars deriv_rhs
-               -- checkValidInstance tyvars theta clas inst_tys
-               -- Not necessary; see Note [Exotic derived instance contexts]
-               --                in TcSimplify
+                 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
+      = setSrcSpan loc  $
+        addErrCtxt (derivInstCtxt the_pred) $
+        do { theta <- simplifyDeriv orig the_pred 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 (sortBy cmpType theta) }    -- Canonicalise before returning the solution
+                -- Claim: the result instance declaration is guaranteed valid
+                -- Hence no need to call:
+                --   checkValidInstance tyvars theta clas inst_tys
+           ; return (sortBy cmpType theta) }    -- Canonicalise before returning the solution
       where
         the_pred = mkClassPred clas inst_tys
 
 ------------------------------------------------------------------
-mkInstance :: OverlapFlag -> ThetaType -> DerivSpec -> ClsInst
+mkInstance :: OverlapFlag -> ThetaType -> DerivSpec -> TcM ClsInst
 mkInstance overlap_flag theta
-           (DS { ds_name = dfun_name
-               , ds_tvs = tyvars, ds_cls = clas, ds_tys = tys })
-  = mkLocalInstance dfun overlap_flag
+           (DS { ds_name = dfun_name
+               , ds_tvs = tvs, ds_cls = clas, ds_tys = tys })
+  = do { (subst, tvs') <- tcInstSkolTyVars tvs
+       ; return (mkLocalInstance dfun overlap_flag tvs' clas (substTys subst tys)) }
   where
-    dfun = mkDictFunId dfun_name tyvars theta clas tys
+    dfun = mkDictFunId dfun_name tvs theta clas tys
 
 
 extendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
@@ -1434,15 +1598,145 @@ extendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
 extendLocalInstEnv dfuns thing_inside
  = do { env <- getGblEnv
       ; let  inst_env' = extendInstEnvList (tcg_inst_env env) dfuns
-            env'      = env { tcg_inst_env = inst_env' }
+             env'      = env { tcg_inst_env = inst_env' }
       ; setGblEnv env' thing_inside }
 \end{code}
 
 
+***********************************************************************************
+*                                                                                 *
+*            Simplify derived constraints
+*                                                                                 *
+***********************************************************************************
+
+\begin{code}
+simplifyDeriv :: CtOrigin
+              -> PredType
+              -> [TyVar]
+              -> ThetaType              -- Wanted
+              -> TcM ThetaType  -- Needed
+-- Given  instance (wanted) => C inst_ty
+-- Simplify 'wanted' as much as possibles
+-- Fail if not possible
+simplifyDeriv orig pred tvs theta
+  = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
+                -- The constraint solving machinery
+                -- expects *TcTyVars* not TyVars.
+                -- We use *non-overlappable* (vanilla) skolems
+                -- See Note [Overlap and deriving]
+
+       ; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+             skol_set   = mkVarSet tvs_skols
+             doc = ptext (sLit "deriving") <+> parens (ppr pred)
+
+       ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
+
+       ; traceTc "simplifyDeriv" $
+         vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
+       ; (residual_wanted, _ev_binds1)
+             <- solveWantedsTcM (mkFlatWC wanted)
+                -- Post: residual_wanted are already zonked
+
+       ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
+                         -- See Note [Exotic derived instance contexts]
+             get_good :: Ct -> Either PredType Ct
+             get_good ct | validDerivPred skol_set p
+                         , isWantedCt ct  = Left p
+                         -- NB: residual_wanted may contain unsolved
+                         -- Derived and we stick them into the bad set
+                         -- so that reportUnsolved may decide what to do with them
+                         | otherwise = Right ct
+                         where p = ctPred ct
+
+       -- We never want to defer these errors because they are errors in the
+       -- compiler! Hence the `False` below
+       ; reportAllUnsolved (residual_wanted { wc_flat = bad })
+
+       ; let min_theta = mkMinimalBySCs (bagToList good)
+       ; return (substTheta subst_skol min_theta) }
+\end{code}
+
+Note [Overlap and deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider some overlapping instances:
+  data Show a => Show [a] where ..
+  data Show [Char] where ...
+
+Now a data type with deriving:
+  data T a = MkT [a] deriving( Show )
+
+We want to get the derived instance
+  instance Show [a] => Show (T a) where...
+and NOT
+  instance Show a => Show (T a) where...
+so that the (Show (T Char)) instance does the Right Thing
+
+It's very like the situation when we're inferring the type
+of a function
+   f x = show [x]
+and we want to infer
+   f :: Show [a] => a -> String
+
+BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
+             the context for the derived instance.
+             Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+
+Note [Exotic derived instance contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a 'derived' instance declaration, we *infer* the context.  It's a
+bit unclear what rules we should apply for this; the Haskell report is
+silent.  Obviously, constraints like (Eq a) are fine, but what about
+        data T f a = MkT (f a) deriving( Eq )
+where we'd get an Eq (f a) constraint.  That's probably fine too.
+
+One could go further: consider
+        data T a b c = MkT (Foo a b c) deriving( Eq )
+        instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
+
+Notice that this instance (just) satisfies the Paterson termination
+conditions.  Then we *could* derive an instance decl like this:
+
+        instance (C Int a, Eq b, Eq c) => Eq (T a b c)
+even though there is no instance for (C Int a), because there just
+*might* be an instance for, say, (C Int Bool) at a site where we
+need the equality instance for T's.
+
+However, this seems pretty exotic, and it's quite tricky to allow
+this, and yet give sensible error messages in the (much more common)
+case where we really want that instance decl for C.
+
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
+
+Here is another example:
+        data Fix f = In (f (Fix f)) deriving( Eq )
+Here, if we are prepared to allow -XUndecidableInstances we
+could derive the instance
+        instance Eq (f (Fix f)) => Eq (Fix f)
+but this is so delicate that I don't think it should happen inside
+'deriving'. If you want this, write it yourself!
+
+NB: if you want to lift this condition, make sure you still meet the
+termination conditions!  If not, the deriving mechanism generates
+larger and larger constraints.  Example:
+  data Succ a = S a
+  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ.  First we'll generate
+  instance (Show (Succ a), Show a) => Show (Seq a)
+and then
+  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+and so on.  Instead we want to complain of no instance for (Show (Succ a)).
+
+The bottom line
+~~~~~~~~~~~~~~~
+Allow constraints which consist only of type variables, with no repeats.
+
+
 %************************************************************************
-%*                                                                     *
+%*                                                                      *
 \subsection[TcDeriv-normal-binds]{Bindings for the various classes}
-%*                                                                     *
+%*                                                                      *
 %************************************************************************
 
 After all the trouble to figure out the required context for the
@@ -1518,26 +1812,26 @@ genInst standalone_deriv oflag comauxs
                  , ds_theta = theta, ds_newtype = is_newtype
                  , ds_name = name, ds_cls = clas })
   | is_newtype
-  = return (InstInfo { iSpec   = inst_spec
-                     , iBinds  = NewTypeDerived co rep_tycon }, emptyBag)
+  = do { inst_spec <- mkInstance oflag theta spec
+       ; return (InstInfo { iSpec   = inst_spec
+                          , iBinds  = NewTypeDerived co rep_tycon }, emptyBag) }
 
   | otherwise
   = do { fix_env <- getFixityEnv
-       ; (meth_binds, deriv_stuff) <- genDerivStuff (getSrcSpan name) 
+       ; (meth_binds, deriv_stuff) <- genDerivStuff (getSrcSpan name)
                                         fix_env clas name rep_tycon
                                         (lookup rep_tycon comauxs)
+       ; inst_spec <- mkInstance oflag theta spec
        ; let inst_info = InstInfo { iSpec   = inst_spec
                                   , iBinds  = VanillaInst meth_binds []
                                                 standalone_deriv }
        ; return ( inst_info, deriv_stuff) }
   where
-
-    inst_spec = mkInstance oflag theta spec
     co1 = case tyConFamilyCoercion_maybe rep_tycon of
-              Just co_con -> mkTcAxInstCo co_con rep_tc_args
+              Just co_con -> mkTcUnbranchedAxInstCo co_con rep_tc_args
               Nothing     -> id_co
               -- Not a family => rep_tycon = main tycon
-    co2 = mkTcAxInstCo (newTyConCo rep_tycon) rep_tc_args
+    co2 = mkTcUnbranchedAxInstCo (newTyConCo rep_tycon) rep_tc_args
     co  = mkTcForAllCos tvs (co1 `mkTcTransCo` co2)
     id_co = mkTcReflCo (mkTyConApp rep_tycon rep_tc_args)
 
@@ -1553,8 +1847,13 @@ genDerivStuff :: SrcSpan -> FixityEnv -> Class -> Name -> TyCon
               -> Maybe CommonAuxiliary
               -> TcM (LHsBinds RdrName, BagDerivStuff)
 genDerivStuff loc fix_env clas name tycon comaux_maybe
-  | className clas `elem` typeableClassNames
-  = return (gen_Typeable_binds loc tycon, emptyBag)
+  | className clas `elem` oldTypeableClassNames
+  = do dflags <- getDynFlags
+       return (gen_old_Typeable_binds dflags loc tycon, emptyBag)
+
+  | className clas == typeableClassName
+  = do dflags <- getDynFlags
+       return (gen_Typeable_binds dflags loc tycon, emptyBag)
 
   | ck `elem` [genClassKey, gen1ClassKey]   -- Special case because monadic
   = let gk =  if ck == genClassKey then Gen0 else Gen1 -- TODO NSF: correctly identify when we're building Both instead of One
@@ -1563,11 +1862,11 @@ genDerivStuff loc fix_env clas name tycon comaux_maybe
       (binds, faminst) <- gen_Generic_binds gk tycon metaTyCons (nameModule name)
       return (binds, DerivFamInst faminst `consBag` emptyBag)
 
-  | otherwise                     -- Non-monadic generators
+  | otherwise                      -- Non-monadic generators
   = do dflags <- getDynFlags
        case assocMaybe (gen_list dflags) (getUnique clas) of
         Just gen_fn -> return (gen_fn loc tycon)
-        Nothing            -> pprPanic "genDerivStuff: bad derived class" (ppr clas)
+        Nothing     -> pprPanic "genDerivStuff: bad derived class" (ppr clas)
   where
     ck = classKey clas
 
@@ -1589,36 +1888,34 @@ genDerivStuff loc fix_env clas name tycon comaux_maybe
 \end{code}
 
 %************************************************************************
-%*                                                                     *
+%*                                                                      *
 \subsection[TcDeriv-taggery-Names]{What con2tag/tag2con functions are available?}
-%*                                                                     *
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
+derivingNullaryErr :: MsgDoc
+derivingNullaryErr = ptext (sLit "Cannot derive instances for nullary classes")
+
 derivingKindErr :: TyCon -> Class -> [Type] -> Kind -> MsgDoc
 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 "..."))))
+                <+> 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))
+            <+> ptext (sLit "expects an argument of kind") <+> quotes (pprKind cls_kind))
 
 derivingEtaErr :: Class -> [Type] -> Type -> MsgDoc
 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 -> MsgDoc
-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)
+         nest 2 (ptext (sLit "instance (...) =>")
+                <+> pprClassPred cls (cls_tys ++ [inst_ty]))]
 
 derivingThingErr :: Bool -> Class -> [Type] -> Type -> MsgDoc -> MsgDoc
 derivingThingErr newtype_deriving clas tys ty why
   = sep [(hang (ptext (sLit "Can't make a derived instance of"))
-            2 (quotes (ppr pred))
+             2 (quotes (ppr pred))
           $$ nest 2 extra) <> colon,
-        nest 2 why]
+         nest 2 why]
   where
     extra | newtype_deriving = ptext (sLit "(even with cunning newtype deriving)")
           | otherwise        = empty
@@ -1631,7 +1928,7 @@ derivingHiddenErr tc
 
 standaloneCtxt :: LHsType Name -> SDoc
 standaloneCtxt ty = hang (ptext (sLit "In the stand-alone deriving instance for"))
-                      2 (quotes (ppr ty))
+                       2 (quotes (ppr ty))
 
 derivInstCtxt :: PredType -> MsgDoc
 derivInstCtxt pred