Custom `Typeable` solver, that keeps track of kinds.

Summary:
This implements the new `Typeable` solver: when GHC sees `Typeable` constraints
it solves them on the spot.

The current implementation creates `TyCon` representations on the spot.

Pro: No overhead at all in code that does not use `Typeable`
Cons: Code that uses `Typeable` may create multipe `TyCon` represntations.

We have discussed an implementation where representations of `TyCons` are
computed once, in the module, where a datatype is declared.  This would
lead to more code being generated:  for a promotable datatype we need to
generate `2 + number_of_data_cons` type-constructro representations,
and we have to do that for all programs, even ones that do not intend to
use typeable.

I added code to emit warning whenevar `deriving Typeable` is encountered---
the idea being that this is not needed anymore, and shold be fixed.

Also, we allow `instance Typeable T` in .hs-boot files, but they result
in a warning, and are ignored.  This last one was to avoid breaking exisitng
code, and should become an error, eventually.

Test Plan:
1. GHC can compile itself.
2. I compiled a number of large libraries, including `lens`.
    - I had to make some small changes:
      `unordered-containers` uses internals of `TypeReps`, so I had to do a 1 line fix
    - `lens` needed one instance changed, due to a poly-kinded `Typeble` instance

3. I also run some code that uses `syb` to traverse a largish datastrucutre.
I didn't notice any signifiant performance difference between the 7.8.3 version,
and this implementation.

Reviewers: simonpj, simonmar, austin, hvr

Reviewed By: austin, hvr

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D652

GHC Trac Issues: #9858

31 files changed, 512 insertions, 574 deletions

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index c4222be0f5..98e6847d8d 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -32,6 +32,7 @@ module MkId (
         voidPrimId, voidArgId,
         nullAddrId, seqId, lazyId, lazyIdKey,
         coercionTokenId, magicDictId, coerceId,
+        proxyHashId,
 
         -- Re-export error Ids
         module PrelRules
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 6e9fcdf05a..079cfbf8ba 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -39,7 +39,9 @@ import UniqSupply
 import Digraph
 
 import PrelNames
-import TyCon      ( isTupleTyCon, tyConDataCons_maybe )
+import TysPrim ( mkProxyPrimTy )
+import TyCon      ( isTupleTyCon, tyConDataCons_maybe
+                  , tyConName, isPromotedTyCon, isPromotedDataCon )
 import TcEvidence
 import TcType
 import Type
@@ -47,6 +49,7 @@ import Coercion hiding (substCo)
 import TysWiredIn ( eqBoxDataCon, coercibleDataCon, tupleCon, mkListTy
                   , mkBoxedTupleTy, stringTy )
 import Id
+import MkId(proxyHashId)
 import Class
 import DataCon  ( dataConTyCon, dataConWorkId )
 import Name
@@ -71,6 +74,7 @@ import Util
 import Control.Monad( when )
 import MonadUtils
 import Control.Monad(liftM)
+import Fingerprint(Fingerprint(..), fingerprintString)
 
 {-
 ************************************************************************
@@ -879,6 +883,128 @@ dsEvTerm (EvLit l) =
 
 dsEvTerm (EvCallStack cs) = dsEvCallStack cs
 
+dsEvTerm (EvTypeable ev) = dsEvTypeable ev
+
+dsEvTypeable :: EvTypeable -> DsM CoreExpr
+dsEvTypeable ev =
+  do tyCl      <- dsLookupTyCon typeableClassName
+     typeRepTc <- dsLookupTyCon typeRepTyConName
+     let tyRepType = mkTyConApp typeRepTc []
+
+     (ty, rep) <-
+        case ev of
+
+          EvTypeableTyCon tc ks ts ->
+            do ctr       <- dsLookupGlobalId mkPolyTyConAppName
+               mkTyCon   <- dsLookupGlobalId mkTyConName
+               dflags    <- getDynFlags
+               let mkRep cRep kReps tReps =
+                     mkApps (Var ctr) [ cRep, mkListExpr tyRepType kReps
+                                            , mkListExpr tyRepType tReps ]
+
+               let kindRep k =
+                     case splitTyConApp_maybe k of
+                       Nothing -> panic "dsEvTypeable: not a kind constructor"
+                       Just (kc,ks) ->
+                         do kcRep <- tyConRep dflags mkTyCon kc
+                            reps  <- mapM kindRep ks
+                            return (mkRep kcRep [] reps)
+
+               tcRep     <- tyConRep dflags mkTyCon tc
+
+               kReps     <- mapM kindRep ks
+               tReps     <- mapM (getRep tyCl) ts
+
+               return ( mkTyConApp tc (ks ++ map snd ts)
+                      , mkRep tcRep kReps tReps
+                      )
+
+          EvTypeableTyApp t1 t2 ->
+            do e1  <- getRep tyCl t1
+               e2  <- getRep tyCl t2
+               ctr <- dsLookupGlobalId mkAppTyName
+
+               return ( mkAppTy (snd t1) (snd t2)
+                      , mkApps (Var ctr) [ e1, e2 ]
+                      )
+
+          EvTypeableTyLit ty ->
+            do str <- case (isNumLitTy ty, isStrLitTy ty) of
+                        (Just n, _) -> return (show n)
+                        (_, Just n) -> return (show n)
+                        _ -> panic "dsEvTypeable: malformed TyLit evidence"
+               ctr <- dsLookupGlobalId typeLitTypeRepName
+               tag <- mkStringExpr str
+               return (ty, mkApps (Var ctr) [ tag ])
+
+     -- TyRep -> Typeable t
+     -- see also: Note [Memoising typeOf]
+     repName <- newSysLocalDs tyRepType
+     let proxyT = mkProxyPrimTy (typeKind ty) ty
+         method = bindNonRec repName rep
+                $ mkLams [mkWildValBinder proxyT] (Var repName)
+
+     -- package up the method as `Typeable` dictionary
+     return $ mkCast method $ mkSymCo $ getTypeableCo tyCl ty
+
+  where
+  -- co: method -> Typeable k t
+  getTypeableCo tc t =
+    case instNewTyCon_maybe tc [typeKind t, t] of
+      Just (_,co) -> co
+      _           -> panic "Class `Typeable` is not a `newtype`."
+
+  -- Typeable t -> TyRep
+  getRep tc (ev,t) =
+    do typeableExpr <- dsEvTerm ev
+       let co     = getTypeableCo tc t
+           method = mkCast typeableExpr co
+           proxy  = mkTyApps (Var proxyHashId) [typeKind t, t]
+       return (mkApps method [proxy])
+
+  -- This part could be cached
+  tyConRep dflags mkTyCon tc =
+    do pkgStr  <- mkStringExprFS pkg_fs
+       modStr  <- mkStringExprFS modl_fs
+       nameStr <- mkStringExprFS name_fs
+       return (mkApps (Var mkTyCon) [ int64 high, int64 low
+                                    , pkgStr, modStr, nameStr
+                                    ])
+    where
+    tycon_name                = tyConName tc
+    modl                      = nameModule tycon_name
+    pkg                       = modulePackageKey modl
+
+    modl_fs                   = moduleNameFS (moduleName modl)
+    pkg_fs                    = packageKeyFS pkg
+    name_fs                   = occNameFS (nameOccName tycon_name)
+    hash_name_fs
+      | isPromotedTyCon tc    = appendFS (mkFastString "$k") name_fs
+      | isPromotedDataCon tc  = appendFS (mkFastString "$c") name_fs
+      | otherwise             = name_fs
+
+    hashThis = unwords $ map unpackFS [pkg_fs, modl_fs, hash_name_fs]
+    Fingerprint high low = fingerprintString hashThis
+
+    int64
+      | wORD_SIZE dflags == 4 = mkWord64LitWord64
+      | otherwise             = mkWordLit dflags . fromIntegral
+
+
+
+{- Note [Memoising typeOf]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+See #3245, #9203
+
+IMPORTANT: we don't want to recalculate the TypeRep once per call with
+the proxy argument.  This is what went wrong in #3245 and #9203. So we
+help GHC by manually keeping the 'rep' *outside* the lambda.
+-}
+
+
+
+
+
 dsEvCallStack :: EvCallStack -> DsM CoreExpr
 -- See Note [Overview of implicit CallStacks] in TcEvidence.hs
 dsEvCallStack cs = do
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 8d6d4296b8..04445c8cdc 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -518,6 +518,7 @@ data WarningFlag =
    | Opt_WarnPartialTypeSignatures
    | Opt_WarnMissingExportedSigs
    | Opt_WarnUntickedPromotedConstructors
+   | Opt_WarnDerivingTypeable
    deriving (Eq, Show, Enum)
 
 data Language = Haskell98 | Haskell2010
@@ -2845,6 +2846,7 @@ fWarningFlags = [
   flagSpec "warn-auto-orphans"                Opt_WarnAutoOrphans,
   flagSpec "warn-deprecations"                Opt_WarnWarningsDeprecations,
   flagSpec "warn-deprecated-flags"            Opt_WarnDeprecatedFlags,
+  flagSpec "warn-deriving-typeable"           Opt_WarnDerivingTypeable,
   flagSpec "warn-dodgy-exports"               Opt_WarnDodgyExports,
   flagSpec "warn-dodgy-foreign-imports"       Opt_WarnDodgyForeignImports,
   flagSpec "warn-dodgy-imports"               Opt_WarnDodgyImports,
diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs
index a3d00996fd..5e13227572 100644
--- a/compiler/prelude/PrelNames.hs
+++ b/compiler/prelude/PrelNames.hs
@@ -213,7 +213,15 @@ basicKnownKeyNames
         alternativeClassName,
         foldableClassName,
         traversableClassName,
-        typeableClassName,              -- derivable
+
+        -- Typeable
+        typeableClassName,
+        typeRepTyConName,
+        mkTyConName,
+        mkPolyTyConAppName,
+        mkAppTyName,
+        typeLitTypeRepName,
+
 
         -- Numeric stuff
         negateName, minusName, geName, eqName,
@@ -1032,9 +1040,21 @@ rationalToDoubleName = varQual gHC_FLOAT (fsLit "rationalToDouble") rationalToDo
 ixClassName :: Name
 ixClassName = clsQual gHC_ARR (fsLit "Ix") ixClassKey
 
--- Class Typeable
-typeableClassName :: Name
-typeableClassName     = clsQual tYPEABLE_INTERNAL    (fsLit "Typeable")  typeableClassKey
+-- Class Typeable, and functions for constructing `Typeable` dictionaries
+typeableClassName
+  , typeRepTyConName
+  , mkTyConName
+  , mkPolyTyConAppName
+  , mkAppTyName
+  , typeLitTypeRepName
+  :: Name
+typeableClassName     = clsQual tYPEABLE_INTERNAL (fsLit "Typeable")       typeableClassKey
+typeRepTyConName      = tcQual  tYPEABLE_INTERNAL (fsLit "TypeRep")        typeRepTyConKey
+mkTyConName           = varQual tYPEABLE_INTERNAL (fsLit "mkTyCon")        mkTyConKey
+mkPolyTyConAppName    = varQual tYPEABLE_INTERNAL (fsLit "mkPolyTyConApp") mkPolyTyConAppKey
+mkAppTyName           = varQual tYPEABLE_INTERNAL (fsLit "mkAppTy")        mkAppTyKey
+typeLitTypeRepName    = varQual tYPEABLE_INTERNAL (fsLit "typeLitTypeRep") typeLitTypeRepKey
+
 
 
 -- Class Data
@@ -1541,6 +1561,10 @@ staticPtrInfoTyConKey = mkPreludeTyConUnique 181
 callStackTyConKey :: Unique
 callStackTyConKey = mkPreludeTyConUnique 182
 
+-- Typeables
+typeRepTyConKey :: Unique
+typeRepTyConKey = mkPreludeTyConUnique 183
+
 ---------------- Template Haskell -------------------
 --      USES TyConUniques 200-299
 -----------------------------------------------------
@@ -1872,6 +1896,18 @@ proxyHashKey = mkPreludeMiscIdUnique 502
 --      USES IdUniques 200-499
 -----------------------------------------------------
 
+-- Used to make `Typeable` dictionaries
+mkTyConKey
+  , mkPolyTyConAppKey
+  , mkAppTyKey
+  , typeLitTypeRepKey
+  :: Unique
+mkTyConKey        = mkPreludeMiscIdUnique 503
+mkPolyTyConAppKey = mkPreludeMiscIdUnique 504
+mkAppTyKey        = mkPreludeMiscIdUnique 505
+typeLitTypeRepKey = mkPreludeMiscIdUnique 506
+
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 04023b56fb..7719c08534 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -43,7 +43,6 @@ import Avail
 import Unify( tcUnifyTy )
 import Class
 import Type
-import Kind( isKind )
 import ErrUtils
 import DataCon
 import Maybes
@@ -150,18 +149,10 @@ forgetTheta :: EarlyDerivSpec -> DerivSpec ()
 forgetTheta (InferTheta spec) = spec { ds_theta = () }
 forgetTheta (GivenTheta spec) = spec { ds_theta = () }
 
-earlyDSTyCon :: EarlyDerivSpec -> TyCon
-earlyDSTyCon (InferTheta spec) = ds_tc spec
-earlyDSTyCon (GivenTheta spec) = ds_tc spec
-
 earlyDSLoc :: EarlyDerivSpec -> SrcSpan
 earlyDSLoc (InferTheta spec) = ds_loc spec
 earlyDSLoc (GivenTheta spec) = ds_loc spec
 
-earlyDSClass :: EarlyDerivSpec -> Class
-earlyDSClass (InferTheta spec) = ds_cls spec
-earlyDSClass (GivenTheta spec) = ds_cls spec
-
 splitEarlyDerivSpec :: [EarlyDerivSpec] -> ([DerivSpec ThetaOrigin], [DerivSpec ThetaType])
 splitEarlyDerivSpec [] = ([],[])
 splitEarlyDerivSpec (InferTheta spec : specs) =
@@ -382,10 +373,11 @@ tcDeriving tycl_decls inst_decls deriv_decls
         ; let (binds, newTyCons, famInsts, extraInstances) =
                 genAuxBinds loc (unionManyBags (auxDerivStuff : deriv_stuff))
 
+        ; dflags <- getDynFlags
+
         ; (inst_info, rn_binds, rn_dus) <-
             renameDeriv is_boot (inst_infos ++ (bagToList extraInstances)) binds
 
-        ; dflags <- getDynFlags
         ; unless (isEmptyBag inst_info) $
              liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
                         (ddump_deriving inst_info rn_binds newTyCons famInsts))
@@ -414,6 +406,73 @@ tcDeriving tycl_decls inst_decls deriv_decls
 
     hangP s x = text "" $$ hang (ptext (sLit s)) 2 x
 
+{-
+genTypeableTyConReps :: DynFlags ->
+                        [LTyClDecl Name] ->
+                        [LInstDecl Name] ->
+                        TcM (Bag (LHsBind RdrName, LSig RdrName))
+genTypeableTyConReps dflags decls insts =
+  do tcs1 <- mapM tyConsFromDecl decls
+     tcs2 <- mapM tyConsFromInst insts
+     return $ listToBag [ genTypeableTyConRep dflags loc tc
+                                          | (loc,tc) <- concat (tcs1 ++ tcs2) ]
+  where
+
+  tyConFromDataCon (L l n) = do dc <- tcLookupDataCon n
+                                return (do tc <- promoteDataCon_maybe dc
+                                           return (l,tc))
+
+  -- Promoted data constructors from a data declaration, or
+  -- a data-family instance.
+  tyConsFromDataRHS = fmap catMaybes
+                    . mapM tyConFromDataCon
+                    . concatMap (con_names . unLoc)
+                    . dd_cons
+
+  -- Tycons from a data-family declaration; not promotable.
+  tyConFromDataFamDecl FamilyDecl { fdLName = L loc name } =
+    do tc <- tcLookupTyCon name
+       return (loc,tc)
+
+
+  -- tycons from a type-level declaration
+  tyConsFromDecl (L _ d)
+
+    -- data or newtype declaration: promoted tycon, tycon, promoted ctrs.
+    | isDataDecl d =
+      do let L loc name = tcdLName d
+         tc           <- tcLookupTyCon name
+         promotedCtrs <- tyConsFromDataRHS (tcdDataDefn d)
+         let tyCons = (loc,tc) : promotedCtrs
+
+         return (case promotableTyCon_maybe tc of
+                   Nothing -> tyCons
+                   Just kc -> (loc,kc) : tyCons)
+
+    -- data family: just the type constructor;  these are not promotable.
+    | isDataFamilyDecl d =
+      do res <- tyConFromDataFamDecl (tcdFam d)
+         return [res]
+
+    -- class: the type constructors of associated data families
+    | isClassDecl d =
+      let isData FamilyDecl { fdInfo = DataFamily } = True
+          isData _ = False
+
+      in mapM tyConFromDataFamDecl (filter isData (map unLoc (tcdATs d)))
+
+    | otherwise = return []
+
+
+  tyConsFromInst (L _ d) =
+    case d of
+      ClsInstD ci      -> fmap concat
+                        $ mapM (tyConsFromDataRHS . dfid_defn . unLoc)
+                        $ cid_datafam_insts ci
+      DataFamInstD dfi -> tyConsFromDataRHS (dfid_defn dfi)
+      TyFamInstD {}    -> return []
+-}
+
 -- Prints the representable type family instance
 pprRepTy :: FamInst -> SDoc
 pprRepTy fi@(FamInst { fi_tys = lhs })
@@ -527,13 +586,7 @@ makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
   = do  { eqns1 <- concatMapM (recoverM (return []) . deriveTyDecl)     tycl_decls
         ; eqns2 <- concatMapM (recoverM (return []) . deriveInstDecl)   inst_decls
         ; eqns3 <- concatMapM (recoverM (return []) . deriveStandalone) deriv_decls
-
-        -- If AutoDeriveTypeable is set, we automatically add Typeable instances
-        -- for every data type and type class declared in the module
-        ; auto_typeable <- xoptM Opt_AutoDeriveTypeable
-        ; eqns4 <- deriveAutoTypeable auto_typeable (eqns1 ++ eqns3) tycl_decls
-
-        ; let eqns = eqns1 ++ eqns2 ++ eqns3 ++ eqns4
+        ; let eqns = eqns1 ++ eqns2 ++ eqns3
 
         ; if is_boot then   -- No 'deriving' at all in hs-boot files
               do { unless (null eqns) (add_deriv_err (head eqns))
@@ -545,31 +598,6 @@ makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
          addErr (hang (ptext (sLit "Deriving not permitted in hs-boot file"))
                     2 (ptext (sLit "Use an instance declaration instead")))
 
-deriveAutoTypeable :: Bool -> [EarlyDerivSpec] -> [LTyClDecl Name] -> TcM [EarlyDerivSpec]
--- Runs over *all* TyCl declarations, including classes and data families
--- i.e. not just data type decls
-deriveAutoTypeable auto_typeable done_specs tycl_decls
-  | not auto_typeable = return []
-  | otherwise         = do { cls <- tcLookupClass typeableClassName
-                           ; concatMapM (do_one cls) tycl_decls }
-  where
-    done_tcs = mkNameSet [ tyConName (earlyDSTyCon spec)
-                         | spec <- done_specs
-                         , className (earlyDSClass spec) == typeableClassName ]
-        -- Check if an automatically generated DS for deriving Typeable should be
-        -- omitted because the user had manually requested an instance
-
-    do_one cls (L _ decl)
-      | isClassDecl decl  -- Traverse into class declarations to check if they have ATs (#9999)
-      = concatMapM (do_one cls) (map (fmap FamDecl) (tcdATs decl))
-      | otherwise
-      = do { tc <- tcLookupTyCon (tcdName decl)
-           ; if (isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
-                                       || tyConName tc `elemNameSet` done_tcs)
-                     -- Do not derive Typeable for type synonyms or type families
-             then return []
-             else mkPolyKindedTypeableEqn cls tc }
-
 ------------------------------------------------------------------
 deriveTyDecl :: LTyClDecl Name -> TcM [EarlyDerivSpec]
 deriveTyDecl (L _ decl@(DataDecl { tcdLName = L _ tc_name
@@ -580,7 +608,7 @@ deriveTyDecl (L _ decl@(DataDecl { tcdLName = L _ tc_name
              tys  = mkTyVarTys tvs
 
        ; case preds of
-          Just (L _ preds') -> concatMapM (deriveTyData False tvs tc tys) preds'
+          Just (L _ preds') -> concatMapM (deriveTyData tvs tc tys) preds'
           Nothing           -> return [] }
 
 deriveTyDecl _ = return []
@@ -604,7 +632,7 @@ deriveFamInst decl@(DataFamInstDecl
        ; tcFamTyPats (famTyConShape fam_tc) pats (kcDataDefn defn) $
              -- kcDataDefn defn: see Note [Finding the LHS patterns]
          \ tvs' pats' _ ->
-           concatMapM (deriveTyData True tvs' fam_tc pats') preds }
+           concatMapM (deriveTyData tvs' fam_tc pats') preds }
 
 deriveFamInst _ = return []
 
@@ -638,8 +666,7 @@ deriveStandalone (L loc (DerivDecl deriv_ty overlap_mode))
   = setSrcSpan loc                   $
     addErrCtxt (standaloneCtxt deriv_ty)  $
     do { traceTc "Standalone deriving decl for" (ppr deriv_ty)
-       ; (tvs, theta, cls, inst_tys) <- setXOptM Opt_DataKinds $ -- for polykinded typeable
-                                        tcHsInstHead TcType.InstDeclCtxt deriv_ty
+       ; (tvs, theta, cls, inst_tys) <- tcHsInstHead TcType.InstDeclCtxt deriv_ty
        ; traceTc "Standalone deriving;" $ vcat
               [ text "tvs:" <+> ppr tvs
               , text "theta:" <+> ppr theta
@@ -657,10 +684,12 @@ deriveStandalone (L loc (DerivDecl deriv_ty overlap_mode))
 
        ; case tcSplitTyConApp_maybe inst_ty of
            Just (tc, tc_args)
-              | className cls == typeableClassName  -- Works for algebraic TyCons
-                                                    -- _and_ data families
-              -> do { check_standalone_typeable theta tc tc_args
-                    ; mkPolyKindedTypeableEqn cls tc }
+              | className cls == typeableClassName
+              -> do warn <- woptM Opt_WarnDerivingTypeable
+                    when warn
+                       $ addWarnTc
+                       $ text "Standalone deriving `Typeable` has no effect."
+                    return []
 
               | isAlgTyCon tc  -- All other classes
               -> do { spec <- mkEqnHelp (fmap unLoc overlap_mode)
@@ -668,59 +697,19 @@ deriveStandalone (L loc (DerivDecl deriv_ty overlap_mode))
                     ; return [spec] }
 
            _  -> -- Complain about functions, primitive types, etc,
-                 -- except for the Typeable class
                  failWithTc $ derivingThingErr False cls cls_tys inst_ty $
                  ptext (sLit "The last argument of the instance must be a data or newtype application")
         }
-  where
-    check_standalone_typeable theta tc tc_args
-             -- We expect to see
-             --       deriving Typeable <kind> T
-             -- for some tycon T.  But if S is kind-polymorphic,
-             -- say (S :: forall k. k -> *), we might see
-             --       deriving Typable <kind> (S k)
-             --
-             -- But we should NOT see
-             --       deriving Typeable <kind> (T Int)
-             -- or    deriving Typeable <kind> (S *)   where S is kind-polymorphic
-             --
-             -- So all the tc_args should be distinct kind variables
-      | null theta
-      , allDistinctTyVars tc_args
-      , all is_kind_var tc_args
-      = return ()
-
-      | otherwise
-      = do { polykinds <- xoptM Opt_PolyKinds
-           ; failWith (mk_msg polykinds theta tc tc_args) }
-
-    is_kind_var tc_arg = case tcGetTyVar_maybe tc_arg of
-                           Just v  -> isKindVar v
-                           Nothing -> False
-
-    mk_msg polykinds theta tc tc_args
-      | not polykinds
-      , all isKind tc_args   -- Non-empty, all kinds, at least one not a kind variable
-      , null theta
-      = hang (ptext (sLit "To make a Typeable instance of poly-kinded")
-               <+> quotes (ppr tc) <> comma)
-           2 (ptext (sLit "use XPolyKinds"))
-
-      | otherwise
-      = hang (ptext (sLit "Derived Typeable instance must be of form"))
-           2 (ptext (sLit "deriving instance Typeable") <+> ppr tc)
 
 
 ------------------------------------------------------------------
-deriveTyData :: Bool                         -- False <=> data/newtype
-                                             -- True  <=> data/newtype *instance*
-             -> [TyVar] -> TyCon -> [Type]   -- LHS of data or data instance
+deriveTyData :: [TyVar] -> TyCon -> [Type]   -- LHS of data or data instance
                                              --   Can be a data instance, hence [Type] args
              -> LHsType Name                 -- The deriving predicate
              -> TcM [EarlyDerivSpec]
 -- The deriving clause of a data or newtype declaration
 -- I.e. not standalone deriving
-deriveTyData is_instance tvs tc tc_args (L loc deriv_pred)
+deriveTyData tvs tc tc_args (L loc deriv_pred)
   = setSrcSpan loc     $        -- Use the location of the 'deriving' item
     do  { (deriv_tvs, cls, cls_tys, cls_arg_kind)
                 <- tcExtendTyVarEnv tvs $
@@ -734,7 +723,11 @@ deriveTyData is_instance tvs tc tc_args (L loc deriv_pred)
                 -- so the argument kind 'k' is not decomposable by splitKindFunTys
                 -- as is the case for all other derivable type classes
         ; if className cls == typeableClassName
-          then derivePolyKindedTypeable is_instance cls cls_tys tvs tc tc_args
+          then do warn <- woptM Opt_WarnDerivingTypeable
+                  when warn
+                     $ addWarnTc
+                     $ text "Deriving `Typeable` has no effect."
+                  return []
           else
 
      do {  -- Given data T a b c = ... deriving( C d ),
@@ -790,25 +783,6 @@ deriveTyData is_instance tvs tc tc_args (L loc deriv_pred)
                             cls final_cls_tys tc final_tc_args Nothing
         ; return [spec] } }
 
-derivePolyKindedTypeable :: Bool -> Class -> [Type]
-                         -> [TyVar] -> TyCon -> [Type]
-                         -> TcM [EarlyDerivSpec]
--- The deriving( Typeable ) clause of a data/newtype decl
--- I.e. not standalone deriving
-derivePolyKindedTypeable is_instance cls cls_tys _tvs tc tc_args
-  | is_instance
-  = failWith (sep [ ptext (sLit "Deriving Typeable is not allowed for family instances;")
-                  , ptext (sLit "derive Typeable for")
-                    <+> quotes (pprSourceTyCon tc)
-                    <+> ptext (sLit "alone") ])
-
-  | otherwise
-  = ASSERT( allDistinctTyVars tc_args )  -- Came from a data/newtype decl
-    do { checkTc (isSingleton cls_tys) $   -- Typeable k
-         derivingThingErr False cls cls_tys (mkTyConApp tc tc_args)
-                          (classArgsErr cls cls_tys)
-
-       ; mkPolyKindedTypeableEqn cls tc }
 
 {-
 Note [Unify kinds in deriving]
@@ -1044,38 +1018,6 @@ mk_data_eqn overlap_mode tvs cls tycon tc_args rep_tc rep_tc_args mtheta
 
 ----------------------
 
-mkPolyKindedTypeableEqn :: Class -> TyCon -> TcM [EarlyDerivSpec]
--- We can arrive here from a 'deriving' clause
--- or from standalone deriving
-mkPolyKindedTypeableEqn cls tc
-  = do { dflags <- getDynFlags   -- It's awkward to re-used checkFlag here,
-       ; checkTc(xopt Opt_DeriveDataTypeable dflags) -- so we do a DIY job
-                (hang (ptext (sLit "Can't make a Typeable instance of") <+> quotes (ppr tc))
-                    2 (ptext (sLit "You need DeriveDataTypeable to derive Typeable instances")))
-
-       ; loc <- getSrcSpanM
-       ; let prom_dcs = mapMaybe promoteDataCon_maybe (tyConDataCons tc)
-       ; mapM (mk_one loc) (tc : prom_dcs) }
-  where
-     mk_one loc tc = do { traceTc "mkPolyKindedTypeableEqn" (ppr tc)
-                        ; dfun_name <- new_dfun_name cls tc
-                        ; return $ GivenTheta $
-                          DS { ds_loc = loc, ds_name = dfun_name
-                             , ds_tvs = kvs, ds_cls = cls
-                             , ds_tys = [tc_app_kind, tc_app]
-                                 -- Remember, Typeable :: forall k. k -> *
-                                 -- so we must instantiate it appropiately
-                             , ds_tc = tc, ds_tc_args = tc_args
-                             , ds_theta = []  -- Context is empty for polykinded Typeable
-                             , ds_overlap = Nothing
-                               -- Perhaps this should be `Just NoOverlap`?
-
-                             , ds_newtype = False } }
-        where
-          (kvs,tc_app_kind) = splitForAllTys (tyConKind tc)
-          tc_args = mkTyVarTys kvs
-          tc_app  = mkTyConApp tc tc_args
-
 inferConstraints :: Class -> [TcType]
                  -> TyCon -> [TcType]
                  -> TcM ThetaOrigin
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index e549b1e8e5..3eb5a31736 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -17,6 +17,7 @@ module TcEvidence (
   EvTerm(..), mkEvCast, evVarsOfTerm,
   EvLit(..), evTermCoercion,
   EvCallStack(..),
+  EvTypeable(..),
 
   -- TcCoercion
   TcCoercion(..), LeftOrRight(..), pickLR,
@@ -727,9 +728,25 @@ data EvTerm
 
   | EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
 
+  | EvTypeable EvTypeable   -- Dictionary for `Typeable`
+
   deriving( Data.Data, Data.Typeable )
 
 
+-- | Instructions on how to make a 'Typeable' dictionary.
+data EvTypeable
+  = EvTypeableTyCon TyCon [Kind] [(EvTerm, Type)]
+    -- ^ Dicitionary for concrete type constructors.
+
+  | EvTypeableTyApp (EvTerm,Type) (EvTerm,Type)
+    -- ^ Dictionary for type applications;  this is used when we have
+    -- a type expression starting with a type variable (e.g., @Typeable (f a)@)
+
+  | EvTypeableTyLit Type
+    -- ^ Dictionary for a type literal.
+
+  deriving ( Data.Data, Data.Typeable )
+
 data EvLit
   = EvNum Integer
   | EvStr FastString
@@ -984,6 +1001,7 @@ evVarsOfTerm (EvTupleMk evs)      = evVarsOfTerms evs
 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
 evVarsOfTerm (EvLit _)            = emptyVarSet
 evVarsOfTerm (EvCallStack cs)     = evVarsOfCallStack cs
+evVarsOfTerm (EvTypeable ev)      = evVarsOfTypeable ev
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
@@ -994,6 +1012,13 @@ evVarsOfCallStack cs = case cs of
   EvCsTop _ _ tm -> evVarsOfTerm tm
   EvCsPushCall _ _ tm -> evVarsOfTerm tm
 
+evVarsOfTypeable :: EvTypeable -> VarSet
+evVarsOfTypeable ev =
+  case ev of
+    EvTypeableTyCon _ _ es -> evVarsOfTerms (map fst es)
+    EvTypeableTyApp e1 e2  -> evVarsOfTerms (map fst [e1,e2])
+    EvTypeableTyLit _      -> emptyVarSet
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1060,6 +1085,7 @@ instance Outputable EvTerm where
   ppr (EvCallStack cs)   = ppr cs
   ppr (EvDelayedError ty msg) =     ptext (sLit "error")
                                 <+> sep [ char '@' <> ppr ty, ppr msg ]
+  ppr (EvTypeable ev)    = ppr ev
 
 instance Outputable EvLit where
   ppr (EvNum n) = integer n
@@ -1073,6 +1099,15 @@ instance Outputable EvCallStack where
   ppr (EvCsPushCall name loc tm)
     = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
 
+instance Outputable EvTypeable where
+  ppr ev =
+    case ev of
+      EvTypeableTyCon tc ks ts -> parens (ppr tc <+> sep (map ppr ks) <+>
+                                                     sep (map (ppr . fst) ts))
+      EvTypeableTyApp t1 t2    -> parens (ppr (fst t1) <+> ppr (fst t2))
+      EvTypeableTyLit x        -> ppr x
+
+
 ----------------------------------------------------------------------
 -- Helper functions for dealing with IP newtype-dictionaries
 ----------------------------------------------------------------------
diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs
index 57718b0007..7802a22f87 100644
--- a/compiler/typecheck/TcGenDeriv.hs
+++ b/compiler/typecheck/TcGenDeriv.hs
@@ -54,7 +54,6 @@ import Class
 import TypeRep
 import VarSet
 import VarEnv
-import Module
 import State
 import Util
 import Var
@@ -66,7 +65,6 @@ import Lexeme
 import FastString
 import Pair
 import Bag
-import Fingerprint
 import TcEnv (InstInfo)
 import StaticFlags( opt_PprStyle_Debug )
 
@@ -121,7 +119,6 @@ genDerivedBinds dflags fix_env clas loc tycon
   where
     gen_list :: [(Unique, SrcSpan -> TyCon -> (LHsBinds RdrName, BagDerivStuff))]
     gen_list = [ (eqClassKey,          gen_Eq_binds)
-               , (typeableClassKey,    gen_Typeable_binds dflags)
                , (ordClassKey,         gen_Ord_binds)
                , (enumClassKey,        gen_Enum_binds)
                , (boundedClassKey,     gen_Bounded_binds)
@@ -1252,55 +1249,6 @@ getPrecedence get_fixity nm
 {-
 ************************************************************************
 *                                                                      *
-\subsection{Typeable (new)}
-*                                                                      *
-************************************************************************
-
-From the data type
-
-        data T a b = ....
-
-we generate
-
-        instance Typeable2 T where
-                typeOf2 _ = mkTyConApp (mkTyCon <hash-high> <hash-low>
-                                                <pkg> <module> "T") []
-
-We are passed the Typeable2 class as well as T
--}
-
-gen_Typeable_binds :: DynFlags -> SrcSpan -> TyCon
-                   -> (LHsBinds RdrName, BagDerivStuff)
-gen_Typeable_binds dflags loc tycon
-  = ( unitBag $ mk_easy_FunBind loc typeRep_RDR [nlWildPat]
-                (nlHsApps mkTyConApp_RDR [tycon_rep, nlList []])
-    , emptyBag )
-  where
-    tycon_name = tyConName tycon
-    modl       = nameModule tycon_name
-    pkg        = modulePackageKey modl
-
-    modl_fs    = moduleNameFS (moduleName modl)
-    pkg_fs     = packageKeyFS pkg
-    name_fs    = occNameFS (nameOccName tycon_name)
-
-    tycon_rep = nlHsApps mkTyCon_RDR
-                    (map nlHsLit [int64 high,
-                                  int64 low,
-                                  HsString "" pkg_fs,
-                                  HsString "" modl_fs,
-                                  HsString "" name_fs])
-
-    hashThis = unwords $ map unpackFS [pkg_fs, modl_fs, name_fs]
-    Fingerprint high low = fingerprintString hashThis
-
-    int64
-      | wORD_SIZE dflags == 4 = HsWord64Prim "" . fromIntegral
-      | otherwise             = HsWordPrim "" . fromIntegral
-
-{-
-************************************************************************
-*                                                                      *
         Data instances
 *                                                                      *
 ************************************************************************
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index b46212ea6d..69bb795c86 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1246,6 +1246,20 @@ zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
 zonkEvTerm env (EvTupleMk tms)    = do { tms' <- mapM (zonkEvTerm env) tms
                                        ; return (EvTupleMk tms') }
 zonkEvTerm _   (EvLit l)          = return (EvLit l)
+
+zonkEvTerm env (EvTypeable ev) =
+  fmap EvTypeable $
+  case ev of
+    EvTypeableTyCon tc ks ts -> EvTypeableTyCon tc ks `fmap` mapM zonk ts
+    EvTypeableTyApp t1 t2    -> do e1 <- zonk t1
+                                   e2 <- zonk t2
+                                   return (EvTypeableTyApp e1 e2)
+    EvTypeableTyLit t        -> EvTypeableTyLit `fmap` zonkTcTypeToType env t
+  where
+  zonk (ev,t) = do ev' <- zonkEvTerm env ev
+                   t'  <- zonkTcTypeToType env t
+                   return (ev',t')
+
 zonkEvTerm env (EvCallStack cs)
   = case cs of
       EvCsEmpty -> return (EvCallStack cs)
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 5ee64791e9..2dc2117bf0 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -43,7 +43,7 @@ import Class
 import Var
 import VarEnv
 import VarSet
-import PrelNames  ( tYPEABLE_INTERNAL, typeableClassName, genericClassNames )
+import PrelNames  ( typeableClassName, genericClassNames )
 import Bag
 import BasicTypes
 import DynFlags
@@ -371,7 +371,6 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
             -- round)
 
             -- Do class and family instance declarations
-       ; env <- getGblEnv
        ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
        ; let (local_infos_s, fam_insts_s) = unzip stuff
              fam_insts    = concat fam_insts_s
@@ -379,7 +378,7 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
              -- Handwritten instances of the poly-kinded Typeable class are
              -- forbidden, so we handle those separately
              (typeable_instances, local_infos)
-                = partition (bad_typeable_instance env) local_infos'
+                = partition bad_typeable_instance local_infos'
 
        ; addClsInsts local_infos $
          addFamInsts fam_insts   $
@@ -423,14 +422,9 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
     }}
   where
     -- Separate the Typeable instances from the rest
-    bad_typeable_instance env i
-      =       -- Class name is Typeable
-         typeableClassName == is_cls_nm (iSpec i)
-              -- but not those that come from Data.Typeable.Internal
-      && tcg_mod env /= tYPEABLE_INTERNAL
-              -- nor those from an .hs-boot or .hsig file
-              -- (deriving can't be used there)
-      && not (isHsBootOrSig (tcg_src env))
+    bad_typeable_instance i
+      = typeableClassName == is_cls_nm (iSpec i)
+
 
     overlapCheck ty = case overlapMode (is_flag $ iSpec ty) of
                         NoOverlap _ -> False
@@ -441,18 +435,21 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
                          ptext (sLit "Replace the following instance:"))
                      2 (pprInstanceHdr (iSpec i))
 
-    typeable_err i
-      = setSrcSpan (getSrcSpan ispec) $
-        addErrTc $ hang (ptext (sLit "Typeable instances can only be derived"))
-                      2 (vcat [ ptext (sLit "Try") <+> quotes (ptext (sLit "deriving instance Typeable")
-                                                <+> pp_tc)
-                              , ptext (sLit "(requires StandaloneDeriving)") ])
-      where
-        ispec = iSpec i
-        pp_tc | [_kind, ty] <- is_tys ispec
-              , Just (tc,_) <- tcSplitTyConApp_maybe ty
-              = ppr tc
-              | otherwise = ptext (sLit "<tycon>")
+    -- Report an error or a warning for a `Typeable` instances.
+    -- If we are workikng on an .hs-boot file, we just report a warning,
+    -- and ignore the instance.  We do this, to give users a chance to fix
+    -- their code.
+    typeable_err i =
+      setSrcSpan (getSrcSpan (iSpec i)) $
+        do env <- getGblEnv
+           if isHsBootOrSig (tcg_src env)
+             then
+               do warn <- woptM Opt_WarnDerivingTypeable
+                  when warn $ addWarnTc $ vcat
+                    [ ptext (sLit "`Typeable` instances in .hs-boot files are ignored.")
+                    , ptext (sLit "This warning will become an error in future versions of the compiler.")
+                    ]
+             else addErrTc $ ptext (sLit "Class `Typeable` does not support user-specified instances.")
 
 addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
 addClsInsts infos thing_inside
@@ -1068,6 +1065,10 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
       | (sc_co, norm_sc_pred) <- normaliseType fam_envs Nominal sc_pred
                                  -- sc_co :: sc_pred ~ norm_sc_pred
       , ClassPred cls tys <- classifyPredType norm_sc_pred
+      , className cls /= typeableClassName
+        -- `Typeable` has custom solving rules, which is why we exlucde it
+        -- from the short cut, and fall throught to calling the solver.
+
       = do { sc_ev_tm <- emit_sc_cls_pred norm_sc_pred cls tys
            ; sc_ev_id <- newEvVar sc_pred
            ; let tc_co = TcCoercion (mkSubCo (mkSymCo sc_co))
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 5ebeb270b1..8f85dd3c81 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -14,6 +14,7 @@ import TcCanonical
 import TcFlatten
 import VarSet
 import Type
+import Kind (isKind)
 import Unify
 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
 import CoAxiom(sfInteractTop, sfInteractInert)
@@ -21,7 +22,7 @@ import CoAxiom(sfInteractTop, sfInteractInert)
 import Var
 import TcType
 import PrelNames ( knownNatClassName, knownSymbolClassName, ipClassNameKey,
-                   callStackTyConKey )
+                   callStackTyConKey, typeableClassName )
 import Id( idType )
 import Class
 import TyCon
@@ -1691,6 +1692,9 @@ matchClassInst _ clas [ ty ] _
     = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
                      $$ vcat (map (ppr . idType) (classMethods clas)))
 
+matchClassInst _ clas [k,t] loc
+  | className clas == typeableClassName = matchTypeableClass clas k t loc
+
 matchClassInst inerts clas tys loc
    = do { dflags <- getDynFlags
         ; tclvl <- getTcLevel
@@ -1833,3 +1837,62 @@ isCallStackIP loc cls ty
     = ctLocSpan loc
 isCallStackIP _ _ _
   = Nothing
+
+
+
+-- | Assumes that we've checked that this is the 'Typeable' class,
+-- and it was applied to the correc arugment.
+matchTypeableClass :: Class -> Kind -> Type -> CtLoc -> TcS LookupInstResult
+matchTypeableClass clas k t loc
+  | isForAllTy k                               = return NoInstance
+  | Just (tc, ks_tys) <- splitTyConApp_maybe t = doTyConApp tc ks_tys
+  | Just (f,kt)       <- splitAppTy_maybe t    = doTyApp f kt
+  | Just _            <- isNumLitTy t          = mkEv [] (EvTypeableTyLit t)
+  | Just _            <- isStrLitTy t          = mkEv [] (EvTypeableTyLit t)
+  | otherwise                                  = return NoInstance
+
+  where
+  -- Representation for type constructor applied to some kinds and some types.
+  doTyConApp tc ks_ts =
+    case mapM kindRep ks of
+      Nothing    -> return NoInstance      -- Not concrete kinds
+      Just kReps ->
+        do tCts <- mapM subGoal ts
+           mkEv tCts (EvTypeableTyCon tc kReps (map ctEvTerm tCts `zip` ts))
+    where
+    (ks,ts)    = span isKind ks_ts
+
+
+  {- Representation for an application of a type to a type-or-kind.
+  This may happen when the type expression starts with a type variable.
+  Example (ignoring kind parameter):
+    Typeable (f Int Char)                      -->
+    (Typeable (f Int), Typeable Char)          -->
+    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
+    Typeable f
+  -}
+  doTyApp f tk
+    | isKind tk = return NoInstance -- We can't solve until we know the ctr.
+    | otherwise =
+      do ct1 <- subGoal f
+         ct2 <- subGoal tk
+         mkEv [ct1,ct2] (EvTypeableTyApp (ctEvTerm ct1,f) (ctEvTerm ct2,tk))
+
+
+  -- Representation for concrete kinds.  We just use the kind itself,
+  -- but first check to make sure that it is "simple" (i.e., made entirely
+  -- out of kind constructors).
+  kindRep ki = do (_,ks) <- splitTyConApp_maybe ki
+                  mapM_ kindRep ks
+                  return ki
+
+
+  -- Emit a `Typeable` constraint for the given type.
+  subGoal ty = do let goal = mkClassPred clas [ typeKind ty, ty ]
+                  ev <- newWantedEvVarNC loc goal
+                  return ev
+
+
+  mkEv subs ev = return (GenInst subs (EvTypeable ev))
+
+
diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml
index 4bf78b6fc0..bdb783d0a6 100644
--- a/docs/users_guide/flags.xml
+++ b/docs/users_guide/flags.xml
@@ -752,7 +752,8 @@
           </row>
           <row>
             <entry><option>-XAutoDeriveTypeable</option></entry>
-            <entry>Automatically <link linkend="deriving-typeable">derive Typeable instances for every datatype and type class declaration</link>.
+            <entry>As of GHC 7.10, this option is not needed, and should
+                   not be used.  Automatically <link linkend="deriving-typeable">derive Typeable instances for every datatype and type class declaration</link>.
             Implies <option>-XDeriveDataTypeable</option>.</entry>
             <entry>dynamic</entry>
             <entry><option>-XNoAutoDeriveTypeable</option></entry>
@@ -814,7 +815,7 @@
           </row>
           <row>
             <entry><option>-XDeriveDataTypeable</option></entry>
-            <entry>Enable <link linkend="deriving-typeable">deriving for the Data and Typeable classes</link>.
+            <entry>Enable <link linkend="deriving-typeable">deriving for the Data class</link>.
               Implied by <option>-XAutoDeriveTypeable</option>.</entry>
             <entry>dynamic</entry>
             <entry><option>-XNoDeriveDataTypeable</option></entry>
@@ -1708,6 +1709,20 @@
             <entry><option>-fno-warn-partial-type-signatures</option></entry>
           </row>
 
+          <row>
+            <entry><option>-fwarn-deriving-typeable</option></entry>
+            <entry>
+              warn when encountering a request to derive an instance of
+              class <literal>Typeable</literal>. As of GHC 7.10, such
+              declarations are unnecessary and are ignored by the compiler
+              because GHC has a custom solver for discharging this type of
+              constraint.
+            </entry>
+            <entry>dynamic</entry>
+            <entry><option>-fno-warn-deriving-typeable</option></entry>
+          </row>
+
+
         </tbody>
       </tgroup>
     </informaltable>
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index d98445eb5d..e8337dd559 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -4062,44 +4062,49 @@ can be mentioned in the <literal>deriving</literal> clause.
 </para></listitem>
 
 <listitem><para>
-Only derived instances of <literal>Typeable</literal> are allowed;
-i.e. handwritten instances are forbidden.  This ensures that the
-programmer cannot subert the type system by writing bogus instances.
+GHC has a custom solver for discharging constraints that involve
+class <literal>Typeable</literal>, and handwritten instances are forbidden.
+This ensures that the programmer cannot subert the type system by
+writing bogus instances.
 </para></listitem>
 
 <listitem><para>
-With <option>-XDeriveDataTypeable</option>
-GHC allows you to derive instances of <literal>Typeable</literal> for data types or newtypes,
-using a <literal>deriving</literal> clause, or using
-a standalone deriving declaration (<xref linkend="stand-alone-deriving"/>).
+Derived instances of <literal>Typeable</literal> are ignored,
+and may be reported as an error in a later version of the compiler.
 </para></listitem>
 
 <listitem><para>
-With <option>-XDataKinds</option>, deriving <literal>Typeable</literal> for a data
-type (whether via a deriving clause or standalone deriving)
-also derives <literal>Typeable</literal> for the promoted data constructors (<xref linkend="promotion"/>).
+The rules for solving `Typeable` constraints are as follows:
+<itemizedlist>
+<listitem><para>A concrete type constructor applied to some types.
+<programlisting>
+instance (Typeable t1, .., Typeable t_n) =>
+  Typeable (T t1 .. t_n)
+</programlisting>
+This rule works for any concrete type constructor, including type
+constructors with polymorhic kinds.   The only restriction is that
+if the type constructor has a polymorhic kind, then it has to be applied
+to all of its kinds parameters, and these kinds need to be concrete
+(i.e., they cannot mention kind variables).
 </para></listitem>
 
 <listitem><para>
-However, using standalone deriving, you can <emphasis>also</emphasis> derive
-a <literal>Typeable</literal> instance for a data family.
-You may not add a <literal>deriving(Typeable)</literal> clause to a
-<literal>data instance</literal> declaration; instead you must use a
-standalone deriving declaration for the data family.
+<programlisting>A type variable applied to some types.
+instance (Typeable f, Typeable t1, .., Typeable t_n) =>
+  Typeable (f t1 .. t_n)
+</programlisting>
 </para></listitem>
 
 <listitem><para>
-Using standalone deriving, you can <emphasis>also</emphasis> derive
-a <literal>Typeable</literal> instance for a type class.
+<programlisting>A concrete type literal.
+instance Typeable 0       -- Type natural literals
+instance Typeable "Hello" -- Type-level symbols
+</programlisting>
 </para></listitem>
-
-<listitem><para>
-The flag <option>-XAutoDeriveTypeable</option> triggers the generation
-of derived <literal>Typeable</literal> instances for every datatype, data family,
-and type class declaration in the module it is used, unless a manually-specified one is
-already provided.
-This flag implies <option>-XDeriveDataTypeable</option>.
+</itemizedlist>
 </para></listitem>
+
+
 </itemizedlist>
 
 </para>
diff --git a/libraries/base/Data/Data.hs b/libraries/base/Data/Data.hs
index 34c235021e..7fe9c4d16f 100644
--- a/libraries/base/Data/Data.hs
+++ b/libraries/base/Data/Data.hs
@@ -1504,7 +1504,7 @@ altConstr = mkConstr altDataType "Alt" ["getAlt"] Prefix
 altDataType :: DataType
 altDataType = mkDataType "Alt" [altConstr]
 
-instance (Data (f a), Typeable f, Typeable a) => Data (Alt f a) where
+instance (Data (f a), Data a, Typeable f) => Data (Alt f a) where
   gfoldl f z (Alt x) = (z Alt `f` x)
   gunfold k z _ = k (z Alt)
   toConstr (Alt _) = altConstr
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 891783341b..4cdc57de22 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -27,6 +27,7 @@
 module Data.Typeable.Internal (
     Proxy (..),
     TypeRep(..),
+    KindRep,
     Fingerprint(..),
     typeOf, typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7,
     Typeable1, Typeable2, Typeable3, Typeable4, Typeable5, Typeable6, Typeable7,
@@ -35,11 +36,13 @@ module Data.Typeable.Internal (
     mkTyCon,
     mkTyCon3,
     mkTyConApp,
+    mkPolyTyConApp,
     mkAppTy,
     typeRepTyCon,
     Typeable(..),
     mkFunTy,
     splitTyConApp,
+    splitPolyTyConApp,
     funResultTy,
     typeRepArgs,
     typeRepHash,
@@ -47,33 +50,15 @@ module Data.Typeable.Internal (
     showsTypeRep,
     tyConString,
     rnfTyCon,
-    listTc, funTc
+    listTc, funTc,
+    typeRepKinds,
+    typeLitTypeRep
   ) where
 
 import GHC.Base
 import GHC.Word
 import GHC.Show
-import GHC.Read ( Read )
 import Data.Proxy
-import GHC.Num
-import GHC.Real
--- import GHC.IORef
--- import GHC.IOArray
--- import GHC.MVar
-import GHC.ST           ( ST, STret )
-import GHC.STRef        ( STRef )
-import GHC.Ptr          ( Ptr, FunPtr )
--- import GHC.Stable
-import GHC.Arr          ( Array, STArray, Ix )
-import GHC.TypeLits ( Nat, Symbol, KnownNat, KnownSymbol, natVal', symbolVal' )
-import Data.Type.Coercion
-import Data.Type.Equality
-import Text.ParserCombinators.ReadP ( ReadP )
-import Text.Read.Lex ( Lexeme, Number )
-import Text.ParserCombinators.ReadPrec ( ReadPrec )
-import GHC.Float ( FFFormat, RealFloat, Floating )
-import Data.Bits ( Bits, FiniteBits )
-import GHC.Enum ( Bounded, Enum )
 
 import GHC.Fingerprint.Type
 import {-# SOURCE #-} GHC.Fingerprint
@@ -84,14 +69,17 @@ import {-# SOURCE #-} GHC.Fingerprint
 
 -- | A concrete representation of a (monomorphic) type.  'TypeRep'
 -- supports reasonably efficient equality.
-data TypeRep = TypeRep {-# UNPACK #-} !Fingerprint TyCon [TypeRep]
+data TypeRep = TypeRep {-# UNPACK #-} !Fingerprint TyCon [KindRep] [TypeRep]
+
+type KindRep = TypeRep
 
 -- Compare keys for equality
 instance Eq TypeRep where
-  (TypeRep k1 _ _) == (TypeRep k2 _ _) = k1 == k2
+  TypeRep x _ _ _ == TypeRep y _ _ _ = x == y
 
 instance Ord TypeRep where
-  (TypeRep k1 _ _) <= (TypeRep k2 _ _) = k1 <= k2
+  TypeRep x _ _ _ <= TypeRep y _ _ _ = x <= y
+
 
 -- | An abstract representation of a type constructor.  'TyCon' objects can
 -- be built using 'mkTyCon'.
@@ -126,25 +114,33 @@ mkTyCon :: Word#   -> Word#   -> String -> String -> String -> TyCon
 mkTyCon high# low# pkg modl name
   = TyCon (Fingerprint (W64# high#) (W64# low#)) pkg modl name
 
--- | Applies a type constructor to a sequence of types
-mkTyConApp  :: TyCon -> [TypeRep] -> TypeRep
-mkTyConApp tc@(TyCon tc_k _ _ _) []
-  = TypeRep tc_k tc [] -- optimisation: all derived Typeable instances
-                       -- end up here, and it helps generate smaller
-                       -- code for derived Typeable.
-mkTyConApp tc@(TyCon tc_k _ _ _) args
-  = TypeRep (fingerprintFingerprints (tc_k : arg_ks)) tc args
+-- | Applies a polymorhic type constructor to a sequence of kinds and types
+mkPolyTyConApp :: TyCon -> [KindRep] -> [TypeRep] -> TypeRep
+mkPolyTyConApp tc@(TyCon tc_k _ _ _) [] [] = TypeRep tc_k tc [] []
+mkPolyTyConApp tc@(TyCon tc_k _ _ _) kinds types =
+  TypeRep (fingerprintFingerprints (tc_k : arg_ks)) tc kinds types
   where
-    arg_ks = [k | TypeRep k _ _ <- args]
+  arg_ks = [ k | TypeRep k _ _ _ <- kinds ++ types ]
+
+-- | Applies a monomorphic type constructor to a sequence of types
+mkTyConApp  :: TyCon -> [TypeRep] -> TypeRep
+mkTyConApp tc = mkPolyTyConApp tc []
 
 -- | A special case of 'mkTyConApp', which applies the function
 -- type constructor to a pair of types.
 mkFunTy  :: TypeRep -> TypeRep -> TypeRep
 mkFunTy f a = mkTyConApp funTc [f,a]
 
--- | Splits a type constructor application
+-- | Splits a type constructor application.
+-- Note that if the type construcotr is polymorphic, this will
+-- not return the kinds that were used.
+-- See 'splitPolyTyConApp' if you need all parts.
 splitTyConApp :: TypeRep -> (TyCon,[TypeRep])
-splitTyConApp (TypeRep _ tc trs) = (tc,trs)
+splitTyConApp (TypeRep _ tc _ trs) = (tc,trs)
+
+-- | Split a type constructor application
+splitPolyTyConApp :: TypeRep -> (TyCon,[KindRep],[TypeRep])
+splitPolyTyConApp (TypeRep _ tc ks trs) = (tc,ks,trs)
 
 -- | Applies a type to a function type.  Returns: @'Just' u@ if the
 -- first argument represents a function of type @t -> u@ and the
@@ -158,7 +154,7 @@ funResultTy trFun trArg
 
 -- | Adds a TypeRep argument to a TypeRep.
 mkAppTy :: TypeRep -> TypeRep -> TypeRep
-mkAppTy (TypeRep _ tc trs) arg_tr = mkTyConApp tc (trs ++ [arg_tr])
+mkAppTy (TypeRep _ tc ks trs) arg_tr = mkPolyTyConApp tc ks (trs ++ [arg_tr])
    -- Notice that we call mkTyConApp to construct the fingerprint from tc and
    -- the arg fingerprints.  Simply combining the current fingerprint with
    -- the new one won't give the same answer, but of course we want to
@@ -183,11 +179,15 @@ mkTyCon3 pkg modl name =
 
 -- | Observe the type constructor of a type representation
 typeRepTyCon :: TypeRep -> TyCon
-typeRepTyCon (TypeRep _ tc _) = tc
+typeRepTyCon (TypeRep _ tc _ _) = tc
 
 -- | Observe the argument types of a type representation
 typeRepArgs :: TypeRep -> [TypeRep]
-typeRepArgs (TypeRep _ _ args) = args
+typeRepArgs (TypeRep _ _ _ tys) = tys
+
+-- | Observe the argument kinds of a type representation
+typeRepKinds :: TypeRep -> [KindRep]
+typeRepKinds (TypeRep _ _ ks _) = ks
 
 -- | Observe string encoding of a type representation
 {-# DEPRECATED tyConString "renamed to 'tyConName'; 'tyConModule' and 'tyConPackage' are also available." #-} -- deprecated in 7.4
@@ -198,7 +198,7 @@ tyConString = tyConName
 --
 -- @since 4.8.0.0
 typeRepHash :: TypeRep -> Fingerprint
-typeRepHash (TypeRep fpr _ _) = fpr
+typeRepHash (TypeRep fpr _ _ _) = fpr
 
 -------------------------------------------------------------
 --
@@ -265,27 +265,11 @@ type Typeable7 (a :: * -> * -> * -> * -> * -> * -> * -> *) = Typeable a
 {-# DEPRECATED Typeable6 "renamed to 'Typeable'" #-} -- deprecated in 7.8
 {-# DEPRECATED Typeable7 "renamed to 'Typeable'" #-} -- deprecated in 7.8
 
--- | Kind-polymorphic Typeable instance for type application
-instance (Typeable s, Typeable a) => Typeable (s a) where
-         -- See Note [The apparent incoherence of Typable]
-  typeRep# = \_ -> rep                  -- Note [Memoising typeOf]
-    where !ty1 = typeRep# (proxy# :: Proxy# s)
-          !ty2 = typeRep# (proxy# :: Proxy# a)
-          !rep = ty1 `mkAppTy` ty2
-
-{- Note [Memoising typeOf]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-See #3245, #9203
-
-IMPORTANT: we don't want to recalculate the TypeRep once per call with
-the proxy argument.  This is what went wrong in #3245 and #9203. So we
-help GHC by manually keeping the 'rep' *outside* the lambda.
--}
 
 ----------------- Showing TypeReps --------------------
 
 instance Show TypeRep where
-  showsPrec p (TypeRep _ tycon tys) =
+  showsPrec p (TypeRep _ tycon kinds tys) =
     case tys of
       [] -> showsPrec p tycon
       [x]   | tycon == listTc -> showChar '[' . shows x . showChar ']'
@@ -298,7 +282,7 @@ instance Show TypeRep where
             showParen (p > 9) $
             showsPrec p tycon .
             showChar ' '      .
-            showArgs (showChar ' ') tys
+            showArgs (showChar ' ') (kinds ++ tys)
 
 showsTypeRep :: TypeRep -> ShowS
 showsTypeRep = shows
@@ -314,7 +298,7 @@ isTupleTyCon _                         = False
 --
 -- @since 4.8.0.0
 rnfTypeRep :: TypeRep -> ()
-rnfTypeRep (TypeRep _ tyc tyrs) = rnfTyCon tyc `seq` go tyrs
+rnfTypeRep (TypeRep _ tyc krs tyrs) = rnfTyCon tyc `seq` go krs `seq` go tyrs
   where
     go [] = ()
     go (x:xs) = rnfTypeRep x `seq` go xs
@@ -346,147 +330,11 @@ listTc = typeRepTyCon (typeOf [()])
 funTc :: TyCon
 funTc = typeRepTyCon (typeRep (Proxy :: Proxy (->)))
 
--------------------------------------------------------------
---
---      Instances of the Typeable classes for Prelude types
---
--------------------------------------------------------------
-
-deriving instance Typeable ()
-deriving instance Typeable []
-deriving instance Typeable Maybe
-deriving instance Typeable Ratio
-deriving instance Typeable (->)
-deriving instance Typeable IO
-
-deriving instance Typeable Array
-
-deriving instance Typeable ST
-deriving instance Typeable STret
-deriving instance Typeable STRef
-deriving instance Typeable STArray
-
-deriving instance Typeable (,)
-deriving instance Typeable (,,)
-deriving instance Typeable (,,,)
-deriving instance Typeable (,,,,)
-deriving instance Typeable (,,,,,)
-deriving instance Typeable (,,,,,,)
 
-deriving instance Typeable Ptr
-deriving instance Typeable FunPtr
 
--------------------------------------------------------
---
--- Generate Typeable instances for standard datatypes
---
--------------------------------------------------------
-
-deriving instance Typeable Bool
-deriving instance Typeable Char
-deriving instance Typeable Float
-deriving instance Typeable Double
-deriving instance Typeable Int
-deriving instance Typeable Word
-deriving instance Typeable Integer
-deriving instance Typeable Ordering
-
-deriving instance Typeable Word8
-deriving instance Typeable Word16
-deriving instance Typeable Word32
-deriving instance Typeable Word64
-
-deriving instance Typeable TyCon
-deriving instance Typeable TypeRep
-deriving instance Typeable Fingerprint
-
-deriving instance Typeable RealWorld
-deriving instance Typeable Proxy
-deriving instance Typeable KProxy
-deriving instance Typeable (:~:)
-deriving instance Typeable Coercion
-
-deriving instance Typeable ReadP
-deriving instance Typeable Lexeme
-deriving instance Typeable Number
-deriving instance Typeable ReadPrec
-
-deriving instance Typeable FFFormat
-
--------------------------------------------------------
---
--- Generate Typeable instances for standard classes
---
--------------------------------------------------------
-
-deriving instance Typeable (~)
-deriving instance Typeable Coercible
-deriving instance Typeable TestEquality
-deriving instance Typeable TestCoercion
-
-deriving instance Typeable Eq
-deriving instance Typeable Ord
-
-deriving instance Typeable Bits
-deriving instance Typeable FiniteBits
-deriving instance Typeable Num
-deriving instance Typeable Real
-deriving instance Typeable Integral
-deriving instance Typeable Fractional
-deriving instance Typeable RealFrac
-deriving instance Typeable Floating
-deriving instance Typeable RealFloat
-
-deriving instance Typeable Bounded
-deriving instance Typeable Enum
-deriving instance Typeable Ix
-
-deriving instance Typeable Show
-deriving instance Typeable Read
-
-deriving instance Typeable Alternative
-deriving instance Typeable Applicative
-deriving instance Typeable Functor
-deriving instance Typeable Monad
-deriving instance Typeable MonadPlus
-deriving instance Typeable Monoid
-
-deriving instance Typeable Typeable
-
-
-
---------------------------------------------------------------------------------
--- Instances for type literals
-
-{- Note [Potential Collisions in `Nat` and `Symbol` instances]
-
-Kinds resulting from lifted types have finitely many type-constructors.
-This is not the case for `Nat` and `Symbol`, which both contain *infinitely*
-many type constructors (e.g., `Nat` has 0, 1, 2, 3, etc.).  One might think
-that this would increase the chance of hash-collisions in the type but this
-is not the case because the fingerprint stored in a `TypeRep` identifies
-the whole *type* and not just the type constructor.  This is why the chance
-of collisions for `Nat` and `Symbol` is not any worse than it is for other
-lifted types with infinitely many inhabitants.  Indeed, `Nat` is
-isomorphic to (lifted) `[()]`  and `Symbol` is isomorphic to `[Char]`.
--}
-
-{- Note [The apparent incoherence of Typable] See Trac #9242
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The reason we have INCOHERENT on Typeable (n:Nat) and Typeable (s:Symbol)
-because we also have an instance Typable (f a).  Now suppose we have
-  [Wanted] Typeable (a :: Nat)
-we should pick the (x::Nat) instance, even though the instance
-matching rules would worry that 'a' might later be instantiated to
-(f b), for some f and b. But we type theorists know that there are no
-type constructors f of kind blah -> Nat, so this can never happen and
-it's safe to pick the second instance. -}
-
-
-instance {-# INCOHERENT #-} KnownNat n => Typeable (n :: Nat) where
-  -- See Note [The apparent incoherence of Typable]
-  -- See #9203 for an explanation of why this is written as `\_ -> rep`.
-  typeRep# = \_ -> rep
+-- | An internal function, to make representations for type literals.
+typeLitTypeRep :: String -> TypeRep
+typeLitTypeRep nm = rep
     where
     rep = mkTyConApp tc []
     tc = TyCon
@@ -497,24 +345,6 @@ instance {-# INCOHERENT #-} KnownNat n => Typeable (n :: Nat) where
            }
     pack = "base"
     modu = "GHC.TypeLits"
-    nm   = show (natVal' (proxy# :: Proxy# n))
     mk a b c = a ++ " " ++ b ++ " " ++ c
 
 
-instance {-# INCOHERENT #-} KnownSymbol s => Typeable (s :: Symbol) where
-  -- See Note [The apparent incoherence of Typable]
-  -- See #9203 for an explanation of why this is written as `\_ -> rep`.
-  typeRep# = \_ -> rep
-    where
-    rep = mkTyConApp tc []
-    tc = TyCon
-           { tyConHash     = fingerprintString (mk pack modu nm)
-           , tyConPackage  = pack
-           , tyConModule   = modu
-           , tyConName     = nm
-           }
-    pack = "base"
-    modu = "GHC.TypeLits"
-    nm   = show (symbolVal' (proxy# :: Proxy# s))
-    mk a b c = a ++ " " ++ b ++ " " ++ c
-
diff --git a/testsuite/tests/annotations/should_fail/annfail10.stderr b/testsuite/tests/annotations/should_fail/annfail10.stderr
index 262677b7f8..5b42bd3c9b 100644
--- a/testsuite/tests/annotations/should_fail/annfail10.stderr
+++ b/testsuite/tests/annotations/should_fail/annfail10.stderr
@@ -7,9 +7,8 @@ annfail10.hs:9:1:
                Data.Data.Data (Either a b)
         -- Defined in ‘Data.Data’
       instance Data.Data.Data Data.Monoid.All -- Defined in ‘Data.Data’
-      instance forall (k :: BOX) (f :: k -> *) (a :: k).
-               (Data.Data.Data (f a), Data.Typeable.Internal.Typeable f,
-                Data.Typeable.Internal.Typeable a) =>
+      instance (Data.Data.Data (f a), Data.Data.Data a,
+                Data.Typeable.Internal.Typeable f) =>
                Data.Data.Data (Data.Monoid.Alt f a)
         -- Defined in ‘Data.Data’
       ...plus 39 others
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 8d9023646c..b56baed668 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -46,7 +46,7 @@ test('T8758', extra_clean(['T8758a.o', 'T8758a.hi']), multimod_compile, ['T8758a
 test('T8678', normal, compile, [''])
 test('T8865', normal, compile, [''])
 test('T8893', normal, compile, [''])
-test('T8950', expect_broken(8950), compile, [''])
+test('T8950', normal, compile, [''])
 test('T8963', normal, compile, [''])
 test('T7269', normal, compile, [''])
 test('T9069', normal, compile, [''])
diff --git a/testsuite/tests/deriving/should_fail/T2604.hs b/testsuite/tests/deriving/should_fail/T2604.hs
deleted file mode 100644
index 0f830d992b..0000000000
--- a/testsuite/tests/deriving/should_fail/T2604.hs
+++ /dev/null
@@ -1,9 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
-module Test where
-
-import Data.Typeable
-
-data DList a = DList [a] deriving(Typeable)
-
-newtype NList a = NList [a] deriving(Typeable)
diff --git a/testsuite/tests/deriving/should_fail/T2604.stderr b/testsuite/tests/deriving/should_fail/T2604.stderr
deleted file mode 100644
index 3000b5002f..0000000000
--- a/testsuite/tests/deriving/should_fail/T2604.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-T2604.hs:7:35:
-    Can't make a Typeable instance of ‘DList’
-      You need DeriveDataTypeable to derive Typeable instances
-    In the data declaration for ‘DList’
-
-T2604.hs:9:38:
-    Can't make a Typeable instance of ‘NList’
-      You need DeriveDataTypeable to derive Typeable instances
-    In the newtype declaration for ‘NList’
diff --git a/testsuite/tests/deriving/should_fail/T5863a.hs b/testsuite/tests/deriving/should_fail/T5863a.hs
deleted file mode 100644
index 3506dcc04a..0000000000
--- a/testsuite/tests/deriving/should_fail/T5863a.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable, TypeFamilies #-}

-

-import Data.Typeable

-

-class C a where

-    data T a :: * 

-

-instance C Int where

-    data T Int = A1 deriving (Typeable)

-

-instance C Bool where

-    data T Bool = A2 deriving (Typeable)

diff --git a/testsuite/tests/deriving/should_fail/T5863a.stderr b/testsuite/tests/deriving/should_fail/T5863a.stderr
deleted file mode 100644
index d64f1b20ce..0000000000
--- a/testsuite/tests/deriving/should_fail/T5863a.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-T5863a.hs:9:31:
-    Deriving Typeable is not allowed for family instances;
-    derive Typeable for ‘T’ alone
-    In the data instance declaration for ‘T’
-
-T5863a.hs:12:32:
-    Deriving Typeable is not allowed for family instances;
-    derive Typeable for ‘T’ alone
-    In the data instance declaration for ‘T’
diff --git a/testsuite/tests/deriving/should_fail/T7800.hs b/testsuite/tests/deriving/should_fail/T7800.hs
deleted file mode 100644
index 9f190cfa51..0000000000
--- a/testsuite/tests/deriving/should_fail/T7800.hs
+++ /dev/null
@@ -1,7 +0,0 @@
-{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable #-}
-module T7800 where
-
-import T7800a
-import Data.Typeable
-
-deriving instance Typeable A
diff --git a/testsuite/tests/deriving/should_fail/T7800.stderr b/testsuite/tests/deriving/should_fail/T7800.stderr
deleted file mode 100644
index 8cd8533968..0000000000
--- a/testsuite/tests/deriving/should_fail/T7800.stderr
+++ /dev/null
@@ -1,6 +0,0 @@
-[1 of 2] Compiling T7800a           ( T7800a.hs, T7800a.o )
-[2 of 2] Compiling T7800            ( T7800.hs, T7800.o )
-
-T7800.hs:7:1:
-    To make a Typeable instance of poly-kinded ‘A’, use XPolyKinds
-    In the stand-alone deriving instance for ‘Typeable A’
diff --git a/testsuite/tests/deriving/should_fail/T7800a.hs b/testsuite/tests/deriving/should_fail/T7800a.hs
deleted file mode 100644
index 22f1305d2e..0000000000
--- a/testsuite/tests/deriving/should_fail/T7800a.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-{-# LANGUAGE PolyKinds #-}
-module T7800a where
-
-data A a
\ No newline at end of file
diff --git a/testsuite/tests/deriving/should_fail/T9687.stderr b/testsuite/tests/deriving/should_fail/T9687.stderr
index 10619a6575..ad95393db7 100644
--- a/testsuite/tests/deriving/should_fail/T9687.stderr
+++ b/testsuite/tests/deriving/should_fail/T9687.stderr
@@ -1,5 +1,3 @@
 
 T9687.hs:4:10:
-    Typeable instances can only be derived
-      Try ‘deriving instance Typeable (,,,,,,,)’
-      (requires StandaloneDeriving)
+    Class `Typeable` does not support user-specified instances.
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index df7957d9b0..60a4b7b45c 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -17,7 +17,7 @@ test('drvfail016',
      run_command,
      ['$MAKE --no-print-directory -s drvfail016'])
 test('T2394', normal, compile_fail, [''])
-test('T2604', normal, compile_fail, [''])
+# T2604 was removed as it was out of date re: fixing #9858
 test('T2701', normal, compile_fail, [''])
 test('T2851', normal, compile_fail, [''])
 test('T2721', normal, compile_fail, [''])
@@ -38,14 +38,14 @@ test('T1133A',
      extra_clean(['T1133A.o-boot', 'T1133A.hi-boot']),
      run_command,
      ['$MAKE --no-print-directory -s T1133A'])
-test('T5863a', normal, compile_fail, [''])
+# 5863a was removed as it was out of date re: fixing #9858
 test('T7959', normal, compile_fail, [''])
 
 test('T1496', normal, compile_fail, [''])
 test('T4846', normal, compile_fail, [''])
 test('T7148', normal, compile_fail, [''])
 test('T7148a', normal, compile_fail, [''])
-test('T7800', normal, multimod_compile_fail, ['T7800',''])
+# T7800 was removed as it was out of date re: fixing #9858
 test('T5498', normal, compile_fail, [''])
 test('T6147', normal, compile_fail, [''])
 test('T8851', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci.debugger/scripts/print019.stderr b/testsuite/tests/ghci.debugger/scripts/print019.stderr
index 139ce8d111..0c92dba4e4 100644
--- a/testsuite/tests/ghci.debugger/scripts/print019.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/print019.stderr
@@ -5,12 +5,8 @@
     Use :print or :force to determine these types
     Relevant bindings include it :: a1 (bound at <interactive>:11:1)
     Note: there are several potential instances:
-      instance forall (k :: BOX) (s :: k). Show (Proxy s)
-        -- Defined in ‘Data.Proxy’
-      instance forall (k :: BOX) (a :: k) (b :: k).
-               Show (Data.Type.Coercion.Coercion a b)
-        -- Defined in ‘Data.Type.Coercion’
-      instance forall (k :: BOX) (a :: k) (b :: k). Show (a :~: b)
-        -- Defined in ‘Data.Type.Equality’
-      ...plus 47 others
+      instance Show TyCon -- Defined in ‘Data.Typeable.Internal’
+      instance Show TypeRep -- Defined in ‘Data.Typeable.Internal’
+      instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+      ...plus 30 others
     In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/polykinds/T8132.stderr b/testsuite/tests/polykinds/T8132.stderr
index 6c567de60a..e4c46591c3 100644
--- a/testsuite/tests/polykinds/T8132.stderr
+++ b/testsuite/tests/polykinds/T8132.stderr
@@ -1,5 +1,3 @@
 
 T8132.hs:6:10:
-    Typeable instances can only be derived
-      Try ‘deriving instance Typeable K’
-      (requires StandaloneDeriving)
+    Class `Typeable` does not support user-specified instances.
diff --git a/testsuite/tests/typecheck/should_compile/T9999.hs b/testsuite/tests/typecheck/should_compile/T9999.hs
deleted file mode 100644
index 656e913043..0000000000
--- a/testsuite/tests/typecheck/should_compile/T9999.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# LANGUAGE AutoDeriveTypeable, PolyKinds, TypeFamilies, StandaloneDeriving #-}
-
-module T9999 where
-
-import Data.Typeable
-
-data family F a
-
-class C a where
-  data F1 a
-  type F2 a
-
-main = typeRep (Proxy :: Proxy F) == typeRep (Proxy :: Proxy F1)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c1ed5790b4..7b3fb9f981 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -440,7 +440,6 @@ test('T9892', normal, compile, [''])
 test('T9939', normal, compile, [''])
 test('T9973', normal, compile, [''])
 test('T9971', normal, compile, [''])
-test('T9999', normal, compile, [''])
 test('T10031', normal, compile, [''])
 test('T10072', normal, compile_fail, [''])
 test('T10100', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/TcStaticPointersFail02.stderr b/testsuite/tests/typecheck/should_fail/TcStaticPointersFail02.stderr
index ead183c7a1..3989ea4936 100644
--- a/testsuite/tests/typecheck/should_fail/TcStaticPointersFail02.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcStaticPointersFail02.stderr
@@ -1,14 +1,14 @@
-

-TcStaticPointersFail02.hs:9:6:

-    No instance for (Data.Typeable.Internal.Typeable b)

-      arising from a static form

-    In the expression: static (undefined :: (forall a. a -> a) -> b)

-    In an equation for ‘f1’:

-        f1 = static (undefined :: (forall a. a -> a) -> b)

-

-TcStaticPointersFail02.hs:12:6:

-    No instance for (Data.Typeable.Internal.Typeable Monad)

-      (maybe you haven't applied a function to enough arguments?)

-      arising from a static form

-    In the expression: static return

-    In an equation for ‘f2’: f2 = static return

+
+TcStaticPointersFail02.hs:9:6:
+    No instance for (Data.Typeable.Internal.Typeable b)
+      arising from a static form
+    In the expression: static (undefined :: (forall a. a -> a) -> b)
+    In an equation for ‘f1’:
+        f1 = static (undefined :: (forall a. a -> a) -> b)
+
+TcStaticPointersFail02.hs:12:6:
+    No instance for (Data.Typeable.Internal.Typeable m)
+      (maybe you haven't applied a function to enough arguments?)
+      arising from a static form
+    In the expression: static return
+    In an equation for ‘f2’: f2 = static return
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 20eede0f96..1ebb0a718f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -353,3 +353,4 @@ test('T9497d', normal, compile_fail, ['-fdefer-type-errors -fno-defer-typed-hole
 test('T8044', normal, compile_fail, [''])
 test('T4921', normal, compile_fail, [''])
 test('T9605', normal, compile_fail, [''])
+test('T9999', normal, compile_fail, [''])