Improve error messages for roles by writing role names out
[ghc.git] / compiler / typecheck / TcDeriv.lhs
index 10670f7..144678e 100644 (file)
@@ -15,6 +15,8 @@ import DynFlags
 
 import TcRnMonad
 import FamInst
+import TcErrors( reportAllUnsolved )
+import TcValidity( validDerivPred )
 import TcEnv
 import TcTyClsDecls( tcFamTyPats, tcAddDataFamInstCtxt )
 import TcClassDcl( tcAddDeclCtxt )      -- Small helper
@@ -44,7 +46,6 @@ import RdrName
 import Name
 import NameSet
 import TyCon
-import CoAxiom
 import TcType
 import Var
 import VarSet
@@ -310,7 +311,9 @@ tcDeriving tycl_decls inst_decls deriv_decls
                 -- 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
@@ -351,7 +354,7 @@ tcDeriving tycl_decls inst_decls deriv_decls
   where
     ddump_deriving :: Bag (InstInfo Name) -> HsValBinds Name
                    -> Bag TyCon                 -- ^ Empty data constructors
-                   -> Bag (FamInst Unbranched)  -- ^ Rep type family instances
+                   -> Bag (FamInst)             -- ^ Rep type family instances
                    -> SDoc
     ddump_deriving inst_infos extra_binds repMetaTys repFamInsts
       =    hang (ptext (sLit "Derived instances:"))
@@ -366,12 +369,11 @@ 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 Unbranched -> SDoc
-pprRepTy fi@(FamInst { fi_branches = FirstBranch (FamInstBranch { fib_lhs = lhs
-                                                                , fib_rhs = rhs }) })
+pprRepTy :: FamInst -> SDoc
+pprRepTy fi@(FamInst { fi_tys = lhs })
   = ptext (sLit "type") <+> ppr (mkTyConApp (famInstTyCon fi) lhs) <+>
-      equals <+> ppr rhs 
-
+      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.
@@ -402,7 +404,7 @@ renameDeriv is_boot inst_infos bagBinds
 
   | otherwise
   = discardWarnings $         -- Discard warnings about unused bindings etc
-    setXOptM Opt_EmptyCase $  -- Derived decls (for empty types) can have 
+    setXOptM Opt_EmptyCase $  -- Derived decls (for empty types) can have
                               --    case x of {}
     do  {
         -- Bring the extra deriving stuff into scope
@@ -471,31 +473,66 @@ makeDerivSpecs :: Bool
                -> [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
+    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 loc $
+       = 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@(DataDecl { tcdLName = L _ tc_name
-                                 , tcdDataDefn = HsDataDefn { dd_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 []
 
@@ -513,8 +550,9 @@ 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 }
+       ; 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)
@@ -541,6 +579,7 @@ deriveStandalone (L loc (DerivDecl deriv_ty))
               , text "cls:" <+> ppr cls
               , text "tys:" <+> ppr inst_tys ]
                 -- 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
@@ -552,8 +591,8 @@ 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)
@@ -565,17 +604,30 @@ deriveTyData tvs tc tc_args (L loc 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]).
 
+                -- 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
-              kind           = tyVarKind (last cls_tyvars)
+        ; 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    = mkVarSet (mapCatMaybes getTyVar_maybe args_to_drop)
+              dropped_tvs    = tyVarsOfTypes args_to_drop
               univ_tvs       = (mkVarSet tvs `extendVarSetList` deriv_tvs)
                                              `minusVarSet` dropped_tvs
 
@@ -586,52 +638,28 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
         ; 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)
+        ; 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 )
 
-        -- 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 }
+        ; 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}
 
-Note [Deriving, type families, and partial applications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When there are no type families, it's quite easy:
-
-    newtype S a = MkS [a]
-    -- :CoS :: S  ~ []  -- Eta-reduced
-
-    instance Eq [a] => Eq (S a)         -- by coercion sym (Eq (:CoS a)) : Eq [a] ~ Eq (S a)
-    instance Monad [] => Monad S        -- by coercion sym (Monad :CoS)  : Monad [] ~ Monad S
-
-When type familes are involved it's trickier:
-
-    data family T a b
-    newtype instance T Int a = MkT [a] deriving( Eq, Monad )
-    -- :RT is the representation type for (T Int a)
-    --  :CoF:R1T a :: T Int a ~ :RT a   -- Not eta reduced
-    --  :Co:R1T    :: :RT ~ []          -- Eta-reduced
-
-    instance Eq [a] => Eq (T Int a)     -- easy by coercion
-    instance Monad [] => Monad (T Int)  -- only if we can eta reduce???
-
-The "???" bit is that we don't build the :CoF thing in eta-reduced form
-Henc the current typeFamilyPapErr, even though the instance makes sense.
-After all, we can write it out
-    instance Monad [] => Monad (T Int)  -- only if we can eta reduce???
-      return x = MkT [x]
-      ... etc ...
 
 \begin{code}
 mkEqnHelp :: CtOrigin -> [TyVar] -> Class -> [Type] -> Type
@@ -645,8 +673,10 @@ mkEqnHelp :: CtOrigin -> [TyVar] -> Class -> [Type] -> Type
 
 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")))
@@ -655,28 +685,40 @@ mkEqnHelp orig tvs cls cls_tys tc_app mtheta
      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
+      = 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 hidden_data_cons = not (isWiredInName (tyConName rep_tc)) &&
+           ; let data_con_names = map dataConName (tyConDataCons rep_tc)
+                 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))
+                                     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))
 
@@ -687,8 +729,83 @@ mkEqnHelp orig tvs cls cls_tys tc_app 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.
+
 
 %************************************************************************
 %*                                                                      *
@@ -741,10 +858,12 @@ mk_data_eqn orig tvs cls tycon tc_args rep_tc rep_tc_args mtheta
     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
+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
@@ -755,13 +874,13 @@ mk_typeable_eqn orig tvs cls tycon tc_args mtheta
         -- 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)
+  = do  { checkTc (cls `hasKey` oldTypeableClassKey)
                   (ptext (sLit "Use deriving( Typeable ) on a data type declaration"))
-        ; real_cls <- tcLookupClass (typeableClassNames `getNth` tyConArity tycon)
+        ; real_cls <- tcLookupClass (oldTypeableClassNames `getNth` tyConArity tycon)
                       -- See Note [Getting base classes]
-        ; mk_typeable_eqn orig tvs real_cls tycon [] (Just []) }
+        ; mkOldTypeableEqn orig tvs real_cls tycon [] (Just []) }
 
-  | otherwise           -- standaone deriving
+  | otherwise           -- standalone deriving
   = do  { checkTc (null tc_args)
                   (ptext (sLit "Derived typeable instance must be of form (Typeable")
                         <> int (tyConArity tycon) <+> ppr tycon <> rparen)
@@ -773,6 +892,31 @@ mk_typeable_eqn orig tvs cls tycon tc_args mtheta
                      , 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]
@@ -785,7 +929,7 @@ inferConstraints cls inst_tys rep_tc rep_tc_args
   = 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)) }
 
@@ -858,16 +1002,10 @@ 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}
@@ -898,8 +1036,9 @@ checkSideConditions dflags mtheta cls cls_tys rep_tc rep_tc_args
   where
     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")
@@ -1028,11 +1167,11 @@ cond_isProduct (_, rep_tc, _)
     why = quotes (pprSourceTyCon rep_tc) <+>
           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, _)
+cond_oldTypeableOK (_, tc, _)
   | tyConArity tc > 7 = Just too_many
   | not (all (isSubOpenTypeKind . tyVarKind) (tyConTyVars tc))
                       = Just bad_kind
@@ -1043,6 +1182,20 @@ cond_typeableOK (_, tc, _)
     bad_kind = quotes (pprSourceTyCon tc) <+>
                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]
 
@@ -1118,10 +1271,11 @@ 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
@@ -1284,6 +1438,7 @@ mkNewTypeEqn orig dflags tvs
            && arity_ok
            && eta_ok
            && ats_ok
+           && roles_ok
 --         && not (isRecursiveTyCon tycon)      -- Note [Recursive newtypes]
 
         arity_ok = length cls_tys + 1 == classArity cls
@@ -1304,13 +1459,26 @@ mkNewTypeEqn orig dflags tvs
                -- 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 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")
+        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]
@@ -1435,6 +1603,136 @@ extendLocalInstEnv dfuns 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}
@@ -1549,7 +1847,11 @@ 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
+  | 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)
 
@@ -1592,6 +1894,9 @@ genDerivStuff loc fix_env clas name tycon comaux_maybe
 %************************************************************************
 
 \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")
@@ -1605,11 +1910,6 @@ derivingEtaErr cls cls_tys inst_ty
          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)
-
 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"))