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

10 files changed, 393 insertions, 225 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))
+
+