Type-indexed Typeable

This at long last realizes the ideas for type-indexed Typeable discussed in A
Reflection on Types (#11011). The general sketch of the project is described on
the Wiki (Typeable/BenGamari). The general idea is that we are adding a type
index to `TypeRep`,

    data TypeRep (a :: k)

This index allows the typechecker to reason about the type represented by the `TypeRep`.
This index representation mechanism is exposed as `Type.Reflection`, which also provides
a number of patterns for inspecting `TypeRep`s,

```lang=haskell
pattern TRFun :: forall k (fun :: k). ()
              => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                        (arg :: TYPE r1) (res :: TYPE r2).
                 (k ~ Type, fun ~~ (arg -> res))
              => TypeRep arg
              -> TypeRep res
              -> TypeRep fun

pattern TRApp :: forall k2 (t :: k2). ()
              => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
              => TypeRep a -> TypeRep b -> TypeRep t

-- | Pattern match on a type constructor.
pattern TRCon :: forall k (a :: k). TyCon -> TypeRep a

-- | Pattern match on a type constructor including its instantiated kind
-- variables.
pattern TRCon' :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
```

In addition, we give the user access to the kind of a `TypeRep` (#10343),

    typeRepKind :: TypeRep (a :: k) -> TypeRep k

Moreover, all of this plays nicely with 8.2's levity polymorphism, including the
newly levity polymorphic (->) type constructor.

Library changes
---------------

The primary change here is the introduction of a Type.Reflection module to base.
This module provides access to the new type-indexed TypeRep introduced in this
patch. We also continue to provide the unindexed Data.Typeable interface, which
is simply a type synonym for the existentially quantified SomeTypeRep,

    data SomeTypeRep where SomeTypeRep :: TypeRep a -> SomeTypeRep

Naturally, this change also touched Data.Dynamic, which can now export the
Dynamic data constructor. Moreover, I removed a blanket reexport of
Data.Typeable from Data.Dynamic (which itself doesn't even import Data.Typeable
now).

We also add a kind heterogeneous type equality type, (:~~:), to
Data.Type.Equality.

Implementation
--------------

The implementation strategy is described in Note [Grand plan for Typeable] in
TcTypeable. None of it was difficult, but it did exercise a number of parts of
the new levity polymorphism story which had not yet been exercised, which took
some sorting out.

The rough idea is that we augment the TyCon produced for each type constructor
with information about the constructor's kind (which we call a KindRep). This
allows us to reconstruct the monomorphic result kind of an particular
instantiation of a type constructor given its kind arguments.

Unfortunately all of this takes a fair amount of work to generate and send
through the compilation pipeline. In particular, the KindReps can unfortunately
get quite large. Moreover, the simplifier will float out various pieces of them,
resulting in numerous top-level bindings. Consequently we mark the KindRep
bindings as noinline, ensuring that the float-outs don't make it into the
interface file. This is important since there is generally little benefit to
inlining KindReps and they would otherwise strongly affect compiler performance.

Performance
-----------

Initially I was hoping to also clear up the remaining holes in Typeable's
coverage by adding support for both unboxed tuples (#12409) and unboxed sums
(#13276). While the former was fairly straightforward, the latter ended up being
quite difficult: while the implementation can support them easily, enabling this
support causes thousands of Typeable bindings to be emitted to the GHC.Types as
each arity-N sum tycon brings with it N promoted datacons, each of which has a
KindRep whose size which itself scales with N. Doing this was simply too
expensive to be practical; consequently I've disabled support for the time
being.

Even after disabling sums this change regresses compiler performance far more
than I would like. In particular there are several testcases in the testsuite
which consist mostly of types which regress by over 30% in compiler allocations.
These include (considering the "bytes allocated" metric),

 * T1969:  +10%
 * T10858: +23%
 * T3294:  +19%
 * T5631:  +41%
 * T6048:  +23%
 * T9675:  +20%
 * T9872a: +5.2%
 * T9872d: +12%
 * T9233:  +10%
 * T10370: +34%
 * T12425: +30%
 * T12234: +16%
 * 13035:  +17%
 * T4029:  +6.1%

I've spent quite some time chasing down the source of this regression and while
I was able to make som improvements, I think this approach of generating
Typeable bindings at time of type definition is doomed to give us unnecessarily
large compile-time overhead.

In the future I think we should consider moving some of all of the Typeable
binding generation logic back to the solver (where it was prior to
91c6b1f54aea658b0056caec45655475897f1972). I've opened #13261 documenting this
proposal.

22 files changed, 902 insertions, 266 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index d77d061fb9..1b11a0f900 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -405,6 +405,9 @@ rnIfaceDecl d@IfaceId{} = do
                       IfDFunId -> rnIfaceNeverExported (ifName d)
                       _ | isDefaultMethodOcc (occName (ifName d))
                         -> rnIfaceNeverExported (ifName d)
+                      -- Typeable bindings. See Note [Grand plan for Typeable].
+                      _ | isTypeableBindOcc (occName (ifName d))
+                        -> rnIfaceNeverExported (ifName d)
                         | otherwise -> rnIfaceGlobal (ifName d)
             ty <- rnIfaceType (ifType d)
             details <- rnIfaceIdDetails (ifIdDetails d)
diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 65860d9045..8a204be421 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -31,7 +31,7 @@ module MkId (
         voidPrimId, voidArgId,
         nullAddrId, seqId, lazyId, lazyIdKey, runRWId,
         coercionTokenId, magicDictId, coerceId,
-        proxyHashId, noinlineIdName,
+        proxyHashId, noinlineId, noinlineIdName,
 
         -- Re-export error Ids
         module PrelRules
diff --git a/compiler/basicTypes/OccName.hs b/compiler/basicTypes/OccName.hs
index 0de9801117..cde7cc569b 100644
--- a/compiler/basicTypes/OccName.hs
+++ b/compiler/basicTypes/OccName.hs
@@ -57,7 +57,7 @@ module OccName (
         isDerivedOccName,
         mkDataConWrapperOcc, mkWorkerOcc,
         mkMatcherOcc, mkBuilderOcc,
-        mkDefaultMethodOcc, isDefaultMethodOcc,
+        mkDefaultMethodOcc, isDefaultMethodOcc, isTypeableBindOcc,
         mkNewTyCoOcc, mkClassOpAuxOcc,
         mkCon2TagOcc, mkTag2ConOcc, mkMaxTagOcc,
         mkClassDataConOcc, mkDictOcc, mkIPOcc,
@@ -601,6 +601,16 @@ isDefaultMethodOcc occ =
      '$':'d':'m':_ -> True
      _ -> False
 
+-- | Is an 'OccName' one of a Typeable @TyCon@ or @Module@ binding?
+-- This is needed as these bindings are renamed differently.
+-- See Note [Grand plan for Typeable] in TcTypeable.
+isTypeableBindOcc :: OccName -> Bool
+isTypeableBindOcc occ =
+   case occNameString occ of
+     '$':'t':'c':_ -> True  -- mkTyConRepOcc
+     '$':'t':'r':_ -> True  -- Module binding
+     _ -> False
+
 mkDataConWrapperOcc, mkWorkerOcc,
         mkMatcherOcc, mkBuilderOcc,
         mkDefaultMethodOcc,
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 2f34046d6a..4aa7d44713 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1031,7 +1031,7 @@ lintTyKind tyvar arg_ty
         -- and then apply it to both boxed and unboxed types.
   = do { arg_kind <- lintType arg_ty
        ; unless (arg_kind `eqType` tyvar_kind)
-                (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
+                (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) }
   where
     tyvar_kind = tyVarKind tyvar
 
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index b367d69a02..efe3e7a8da 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -38,7 +38,6 @@ import CoreFVs
 import Digraph
 
 import PrelNames
-import TysPrim ( mkProxyPrimTy )
 import TyCon
 import TcEvidence
 import TcType
@@ -1195,49 +1194,71 @@ dsEvTypeable :: Type -> EvTypeable -> DsM CoreExpr
 -- This code is tightly coupled to the representation
 -- of TypeRep, in base library Data.Typeable.Internals
 dsEvTypeable ty ev
-  = do { tyCl <- dsLookupTyCon typeableClassName   -- Typeable
+  = do { tyCl <- dsLookupTyCon typeableClassName    -- Typeable
        ; let kind = typeKind ty
              Just typeable_data_con
-                 = tyConSingleDataCon_maybe tyCl      -- "Data constructor"
-                                                      -- for Typeable
+                 = tyConSingleDataCon_maybe tyCl    -- "Data constructor"
+                                                    -- for Typeable
 
-       ; rep_expr <- ds_ev_typeable ty ev
-
-       -- Build Core for (let r::TypeRep = rep in \proxy. rep)
-       -- See Note [Memoising typeOf]
-       ; repName <- newSysLocalDs (exprType rep_expr)
-       ; let proxyT = mkProxyPrimTy kind ty
-             method = bindNonRec repName rep_expr
-                      $ mkLams [mkWildValBinder proxyT] (Var repName)
+       ; rep_expr <- ds_ev_typeable ty ev           -- :: TypeRep a
 
        -- Package up the method as `Typeable` dictionary
-       ; return $ mkConApp typeable_data_con [Type kind, Type ty, method] }
+       ; return $ mkConApp typeable_data_con [Type kind, Type ty, rep_expr] }
 
+type TypeRepExpr = CoreExpr
 
+-- | Returns a @CoreExpr :: TypeRep ty@
 ds_ev_typeable :: Type -> EvTypeable -> DsM CoreExpr
--- Returns a CoreExpr :: TypeRep ty
-ds_ev_typeable ty (EvTypeableTyCon evs)
-  | Just (tc, ks) <- splitTyConApp_maybe ty
-  = do { ctr <- dsLookupGlobalId mkPolyTyConAppName
-                    -- mkPolyTyConApp :: TyCon -> [KindRep] -> [TypeRep] -> TypeRep
-       ; tyRepTc <- dsLookupTyCon typeRepTyConName  -- TypeRep (the TyCon)
-       ; let tyRepType = mkTyConApp tyRepTc []      -- TypeRep (the Type)
-             mkRep cRep kReps tReps
-               = mkApps (Var ctr) [ cRep
-                                  , mkListExpr tyRepType kReps
-                                  , mkListExpr tyRepType tReps ]
-
-
-       ; tcRep <- tyConRep tc
-       ; kReps <- zipWithM getRep evs ks
-       ; return (mkRep tcRep kReps []) }
+ds_ev_typeable ty (EvTypeableTyCon tc kind_ev)
+  = do { mkTrCon <- dsLookupGlobalId mkTrConName
+                    -- mkTrCon :: forall k (a :: k). TyCon -> TypeRep k -> TypeRep a
+       ; someTypeRepTyCon <- dsLookupTyCon someTypeRepTyConName
+       ; someTypeRepDataCon <- dsLookupDataCon someTypeRepDataConName
+                    -- SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep
+
+       ; tc_rep <- tyConRep tc                      -- :: TyCon
+       ; let ks = tyConAppArgs ty
+             -- Construct a SomeTypeRep
+             toSomeTypeRep :: Type -> EvTerm -> DsM CoreExpr
+             toSomeTypeRep t ev = do
+                 rep <- getRep ev t
+                 return $ mkCoreConApps someTypeRepDataCon [Type (typeKind t), Type t, rep]
+       ; kind_arg_reps <- sequence $ zipWith toSomeTypeRep ks kind_ev   -- :: TypeRep t
+       ; let -- :: [SomeTypeRep]
+             kind_args = mkListExpr (mkTyConTy someTypeRepTyCon) kind_arg_reps
+
+         -- Note that we use the kind of the type, not the TyCon from which it
+         -- is constructed since the latter may be kind polymorphic whereas the
+         -- former we know is not (we checked in the solver).
+       ; return $ mkApps (Var mkTrCon) [ Type (typeKind ty)
+                                       , Type ty
+                                       , tc_rep
+                                       , kind_args ]
+       }
 
 ds_ev_typeable ty (EvTypeableTyApp ev1 ev2)
   | Just (t1,t2) <- splitAppTy_maybe ty
   = do { e1  <- getRep ev1 t1
        ; e2  <- getRep ev2 t2
-       ; ctr <- dsLookupGlobalId mkAppTyName
-       ; return ( mkApps (Var ctr) [ e1, e2 ] ) }
+       ; mkTrApp <- dsLookupGlobalId mkTrAppName
+                    -- mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
+                    --            TypeRep a -> TypeRep b -> TypeRep (a b)
+       ; let (k1, k2) = splitFunTy (typeKind t1)
+       ; return $ mkApps (mkTyApps (Var mkTrApp) [ k1, k2, t1, t2 ])
+                         [ e1, e2 ] }
+
+ds_ev_typeable ty (EvTypeableTrFun ev1 ev2)
+  | Just (t1,t2) <- splitFunTy_maybe ty
+  = do { e1 <- getRep ev1 t1
+       ; e2 <- getRep ev2 t2
+       ; mkTrFun <- dsLookupGlobalId mkTrFunName
+                    -- mkTrFun :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2).
+                    --            TypeRep a -> TypeRep b -> TypeRep (a -> b)
+       ; let r1 = getRuntimeRep "ds_ev_typeable" t1
+             r2 = getRuntimeRep "ds_ev_typeable" t2
+       ; return $ mkApps (mkTyApps (Var mkTrFun) [r1, r2, t1, t2])
+                         [ e1, e2 ]
+       }
 
 ds_ev_typeable ty (EvTypeableTyLit ev)
   = do { fun  <- dsLookupGlobalId tr_fun
@@ -1248,28 +1269,26 @@ ds_ev_typeable ty (EvTypeableTyLit ev)
     ty_kind = typeKind ty
 
     -- tr_fun is the Name of
-    --       typeNatTypeRep    :: KnownNat    a => Proxy# a -> TypeRep
-    -- of    typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep
+    --       typeNatTypeRep    :: KnownNat    a => Proxy# a -> TypeRep a
+    -- of    typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep a
     tr_fun | ty_kind `eqType` typeNatKind    = typeNatTypeRepName
            | ty_kind `eqType` typeSymbolKind = typeSymbolTypeRepName
            | otherwise = panic "dsEvTypeable: unknown type lit kind"
 
-
 ds_ev_typeable ty ev
   = pprPanic "dsEvTypeable" (ppr ty $$ ppr ev)
 
-getRep :: EvTerm -> Type  -- EvTerm for Typeable ty, and ty
-       -> DsM CoreExpr    -- Return CoreExpr :: TypeRep (of ty)
-                          -- namely (typeRep# dict proxy)
+getRep :: EvTerm          -- ^ EvTerm for @Typeable ty@
+       -> Type            -- ^ The type @ty@
+       -> DsM TypeRepExpr -- ^ Return @CoreExpr :: TypeRep ty@
+                          -- namely @typeRep# dict@
 -- Remember that
---   typeRep# :: forall k (a::k). Typeable k a -> Proxy k a -> TypeRep
+--   typeRep# :: forall k (a::k). Typeable k a -> TypeRep a
 getRep ev ty
   = do { typeable_expr <- dsEvTerm ev
        ; typeRepId     <- dsLookupGlobalId typeRepIdName
        ; let ty_args = [typeKind ty, ty]
-       ; return (mkApps (mkTyApps (Var typeRepId) ty_args)
-                        [ typeable_expr
-                        , mkTyApps (Var proxyHashId) ty_args ]) }
+       ; return (mkApps (mkTyApps (Var typeRepId) ty_args) [ typeable_expr ]) }
 
 tyConRep :: TyCon -> DsM CoreExpr
 -- Returns CoreExpr :: TyCon
diff --git a/compiler/prelude/KnownUniques.hs b/compiler/prelude/KnownUniques.hs
index 2dc6f8388d..8f1b0b6347 100644
--- a/compiler/prelude/KnownUniques.hs
+++ b/compiler/prelude/KnownUniques.hs
@@ -58,32 +58,57 @@ knownUniqueName u =
 -- Anonymous sums
 --
 -- Sum arities start from 2. The encoding is a bit funny: we break up the
--- integral part into bitfields for the arity and alternative index (which is
--- taken to be 0xff in the case of the TyCon)
+-- integral part into bitfields for the arity, an alternative index (which is
+-- taken to be 0xff in the case of the TyCon), and, in the case of a datacon, a
+-- tag (used to identify the sum's TypeRep binding).
+--
+-- This layout is chosen to remain compatible with the usual unique allocation
+-- for wired-in data constructors described in Unique.hs
 --
 -- TyCon for sum of arity k:
---   00000000 kkkkkkkk 11111111
+--   00000000 kkkkkkkk 11111100
+
+-- TypeRep of TyCon for sum of arity k:
+--   00000000 kkkkkkkk 11111101
+--
 -- DataCon for sum of arity k and alternative n (zero-based):
---   00000000 kkkkkkkk nnnnnnnn
+--   00000000 kkkkkkkk nnnnnn00
+--
+-- TypeRep for sum DataCon of arity k and alternative n (zero-based):
+--   00000000 kkkkkkkk nnnnnn10
 
 mkSumTyConUnique :: Arity -> Unique
 mkSumTyConUnique arity =
     ASSERT(arity < 0xff)
-    mkUnique 'z' (arity `shiftL` 8 .|. 0xff)
+    mkUnique 'z' (arity `shiftL` 8 .|. 0xfc)
 
 mkSumDataConUnique :: ConTagZ -> Arity -> Unique
 mkSumDataConUnique alt arity
   | alt >= arity
   = panic ("mkSumDataConUnique: " ++ show alt ++ " >= " ++ show arity)
   | otherwise
-  = mkUnique 'z' (arity `shiftL` 8 + alt) {- skip the tycon -}
+  = mkUnique 'z' (arity `shiftL` 8 + alt `shiftL` 2) {- skip the tycon -}
 
 getUnboxedSumName :: Int -> Name
-getUnboxedSumName n =
-    case n .&. 0xff of
-      0xff -> tyConName $ sumTyCon arity
-      alt  -> dataConName $ sumDataCon (alt + 1) arity
-  where arity = n `shiftR` 8
+getUnboxedSumName n
+  | n .&. 0xfc == 0xfc
+  = case tag of
+      0x0 -> tyConName $ sumTyCon arity
+      0x1 -> getRep $ sumTyCon arity
+      _   -> pprPanic "getUnboxedSumName: invalid tag" (ppr tag)
+  | tag == 0x0
+  = dataConName $ sumDataCon (alt + 1) arity
+  | tag == 0x2
+  = getRep $ promoteDataCon $ sumDataCon (alt + 1) arity
+  | otherwise
+  = pprPanic "getUnboxedSumName" (ppr n)
+  where
+    arity = n `shiftR` 8
+    alt = (n .&. 0xff) `shiftR` 2
+    tag = 0x3 .&. n
+    getRep tycon =
+        fromMaybe (pprPanic "getUnboxedSumName" (ppr tycon))
+        $ tyConRepName_maybe tycon
 
 -- Note [Uniques for tuple type and data constructors]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs
index 47b78f1d14..470b736286 100644
--- a/compiler/prelude/PrelNames.hs
+++ b/compiler/prelude/PrelNames.hs
@@ -224,9 +224,23 @@ basicKnownKeyNames
         -- Typeable
         typeableClassName,
         typeRepTyConName,
+        someTypeRepTyConName,
+        someTypeRepDataConName,
+        kindRepTyConName,
+        kindRepTyConAppDataConName,
+        kindRepVarDataConName,
+        kindRepAppDataConName,
+        kindRepFunDataConName,
+        kindRepTYPEDataConName,
+        kindRepTypeLitSDataConName,
+        kindRepTypeLitDDataConName,
+        typeLitSortTyConName,
+        typeLitSymbolDataConName,
+        typeLitNatDataConName,
         typeRepIdName,
-        mkPolyTyConAppName,
-        mkAppTyName,
+        mkTrConName,
+        mkTrAppName,
+        mkTrFunName,
         typeSymbolTypeRepName, typeNatTypeRepName,
         trGhcPrimModuleName,
 
@@ -1200,11 +1214,40 @@ trNameDDataConName    = dcQual gHC_TYPES          (fsLit "TrNameD")        trNam
 trTyConTyConName      = tcQual gHC_TYPES          (fsLit "TyCon")          trTyConTyConKey
 trTyConDataConName    = dcQual gHC_TYPES          (fsLit "TyCon")          trTyConDataConKey
 
+kindRepTyConName
+  , kindRepTyConAppDataConName
+  , kindRepVarDataConName
+  , kindRepAppDataConName
+  , kindRepFunDataConName
+  , kindRepTYPEDataConName
+  , kindRepTypeLitSDataConName
+  , kindRepTypeLitDDataConName
+  :: Name
+kindRepTyConName      = tcQual gHC_TYPES          (fsLit "KindRep")        kindRepTyConKey
+kindRepTyConAppDataConName = dcQual gHC_TYPES     (fsLit "KindRepTyConApp") kindRepTyConAppDataConKey
+kindRepVarDataConName = dcQual gHC_TYPES          (fsLit "KindRepVar")     kindRepVarDataConKey
+kindRepAppDataConName = dcQual gHC_TYPES          (fsLit "KindRepApp")     kindRepAppDataConKey
+kindRepFunDataConName = dcQual gHC_TYPES          (fsLit "KindRepFun")     kindRepFunDataConKey
+kindRepTYPEDataConName = dcQual gHC_TYPES         (fsLit "KindRepTYPE")    kindRepTYPEDataConKey
+kindRepTypeLitSDataConName = dcQual gHC_TYPES     (fsLit "KindRepTypeLitS") kindRepTypeLitSDataConKey
+kindRepTypeLitDDataConName = dcQual gHC_TYPES     (fsLit "KindRepTypeLitD") kindRepTypeLitDDataConKey
+
+typeLitSortTyConName
+  , typeLitSymbolDataConName
+  , typeLitNatDataConName
+  :: Name
+typeLitSortTyConName     = tcQual gHC_TYPES       (fsLit "TypeLitSort")    typeLitSortTyConKey
+typeLitSymbolDataConName = dcQual gHC_TYPES       (fsLit "TypeLitSymbol")  typeLitSymbolDataConKey
+typeLitNatDataConName    = dcQual gHC_TYPES       (fsLit "TypeLitNat")     typeLitNatDataConKey
+
 -- Class Typeable, and functions for constructing `Typeable` dictionaries
 typeableClassName
   , typeRepTyConName
-  , mkPolyTyConAppName
-  , mkAppTyName
+  , someTypeRepTyConName
+  , someTypeRepDataConName
+  , mkTrConName
+  , mkTrAppName
+  , mkTrFunName
   , typeRepIdName
   , typeNatTypeRepName
   , typeSymbolTypeRepName
@@ -1212,9 +1255,12 @@ typeableClassName
   :: Name
 typeableClassName     = clsQual tYPEABLE_INTERNAL (fsLit "Typeable")       typeableClassKey
 typeRepTyConName      = tcQual  tYPEABLE_INTERNAL (fsLit "TypeRep")        typeRepTyConKey
+someTypeRepTyConName   = tcQual tYPEABLE_INTERNAL (fsLit "SomeTypeRep")    someTypeRepTyConKey
+someTypeRepDataConName = dcQual tYPEABLE_INTERNAL (fsLit "SomeTypeRep")    someTypeRepDataConKey
 typeRepIdName         = varQual tYPEABLE_INTERNAL (fsLit "typeRep#")       typeRepIdKey
-mkPolyTyConAppName    = varQual tYPEABLE_INTERNAL (fsLit "mkPolyTyConApp") mkPolyTyConAppKey
-mkAppTyName           = varQual tYPEABLE_INTERNAL (fsLit "mkAppTy")        mkAppTyKey
+mkTrConName           = varQual tYPEABLE_INTERNAL (fsLit "mkTrCon")        mkTrConKey
+mkTrAppName           = varQual tYPEABLE_INTERNAL (fsLit "mkTrApp")        mkTrAppKey
+mkTrFunName           = varQual tYPEABLE_INTERNAL (fsLit "mkTrFun")        mkTrFunKey
 typeNatTypeRepName    = varQual tYPEABLE_INTERNAL (fsLit "typeNatTypeRep") typeNatTypeRepKey
 typeSymbolTypeRepName = varQual tYPEABLE_INTERNAL (fsLit "typeSymbolTypeRep") typeSymbolTypeRepKey
 -- this is the Typeable 'Module' for GHC.Prim (which has no code, so we place in GHC.Types)
@@ -1802,11 +1848,14 @@ callStackTyConKey :: Unique
 callStackTyConKey = mkPreludeTyConUnique 183
 
 -- Typeables
-typeRepTyConKey :: Unique
-typeRepTyConKey = mkPreludeTyConUnique 184
+typeRepTyConKey, someTypeRepTyConKey, someTypeRepDataConKey :: Unique
+typeRepTyConKey       = mkPreludeTyConUnique 184
+someTypeRepTyConKey   = mkPreludeTyConUnique 185
+someTypeRepDataConKey = mkPreludeTyConUnique 186
+
 
 typeSymbolAppendFamNameKey :: Unique
-typeSymbolAppendFamNameKey = mkPreludeTyConUnique 185
+typeSymbolAppendFamNameKey = mkPreludeTyConUnique 187
 
 ---------------- Template Haskell -------------------
 --      THNames.hs: USES TyConUniques 200-299
@@ -1888,15 +1937,18 @@ srcLocDataConKey                        = mkPreludeDataConUnique 37
 trTyConTyConKey, trTyConDataConKey,
   trModuleTyConKey, trModuleDataConKey,
   trNameTyConKey, trNameSDataConKey, trNameDDataConKey,
-  trGhcPrimModuleKey :: Unique
-trTyConTyConKey                         = mkPreludeDataConUnique 41
-trTyConDataConKey                       = mkPreludeDataConUnique 42
-trModuleTyConKey                        = mkPreludeDataConUnique 43
-trModuleDataConKey                      = mkPreludeDataConUnique 44
-trNameTyConKey                          = mkPreludeDataConUnique 45
-trNameSDataConKey                       = mkPreludeDataConUnique 46
-trNameDDataConKey                       = mkPreludeDataConUnique 47
-trGhcPrimModuleKey                      = mkPreludeDataConUnique 48
+  trGhcPrimModuleKey, kindRepTyConKey,
+  typeLitSortTyConKey :: Unique
+trTyConTyConKey                         = mkPreludeDataConUnique 40
+trTyConDataConKey                       = mkPreludeDataConUnique 41
+trModuleTyConKey                        = mkPreludeDataConUnique 42
+trModuleDataConKey                      = mkPreludeDataConUnique 43
+trNameTyConKey                          = mkPreludeDataConUnique 44
+trNameSDataConKey                       = mkPreludeDataConUnique 45
+trNameDDataConKey                       = mkPreludeDataConUnique 46
+trGhcPrimModuleKey                      = mkPreludeDataConUnique 47
+kindRepTyConKey                         = mkPreludeDataConUnique 48
+typeLitSortTyConKey                     = mkPreludeDataConUnique 49
 
 typeErrorTextDataConKey,
   typeErrorAppendDataConKey,
@@ -1955,8 +2007,26 @@ vecCountDataConKeys = map mkPreludeDataConUnique [83..88]
 vecElemDataConKeys :: [Unique]
 vecElemDataConKeys = map mkPreludeDataConUnique [89..98]
 
+-- Typeable things
+kindRepTyConAppDataConKey, kindRepVarDataConKey, kindRepAppDataConKey,
+    kindRepFunDataConKey, kindRepTYPEDataConKey,
+    kindRepTypeLitSDataConKey, kindRepTypeLitDDataConKey
+    :: Unique
+kindRepTyConAppDataConKey = mkPreludeDataConUnique 100
+kindRepVarDataConKey      = mkPreludeDataConUnique 101
+kindRepAppDataConKey      = mkPreludeDataConUnique 102
+kindRepFunDataConKey      = mkPreludeDataConUnique 103
+kindRepTYPEDataConKey     = mkPreludeDataConUnique 104
+kindRepTypeLitSDataConKey = mkPreludeDataConUnique 105
+kindRepTypeLitDDataConKey = mkPreludeDataConUnique 106
+
+typeLitSymbolDataConKey, typeLitNatDataConKey :: Unique
+typeLitSymbolDataConKey   = mkPreludeDataConUnique 107
+typeLitNatDataConKey      = mkPreludeDataConUnique 108
+
+
 ---------------- Template Haskell -------------------
---      THNames.hs: USES DataUniques 100-150
+--      THNames.hs: USES DataUniques 200-250
 -----------------------------------------------------
 
 
@@ -2229,41 +2299,54 @@ proxyHashKey = mkPreludeMiscIdUnique 502
 
 -- Used to make `Typeable` dictionaries
 mkTyConKey
-  , mkPolyTyConAppKey
-  , mkAppTyKey
+  , mkTrConKey
+  , mkTrAppKey
+  , mkTrFunKey
   , typeNatTypeRepKey
   , typeSymbolTypeRepKey
   , typeRepIdKey
   :: Unique
 mkTyConKey            = mkPreludeMiscIdUnique 503
-mkPolyTyConAppKey     = mkPreludeMiscIdUnique 504
-mkAppTyKey            = mkPreludeMiscIdUnique 505
+mkTrConKey            = mkPreludeMiscIdUnique 504
+mkTrAppKey            = mkPreludeMiscIdUnique 505
 typeNatTypeRepKey     = mkPreludeMiscIdUnique 506
 typeSymbolTypeRepKey  = mkPreludeMiscIdUnique 507
 typeRepIdKey          = mkPreludeMiscIdUnique 508
+mkTrFunKey            = mkPreludeMiscIdUnique 509
+
+-- Representations for primitive types
+trTYPEKey
+  ,trTYPE'PtrRepLiftedKey
+  , trRuntimeRepKey
+  , tr'PtrRepLiftedKey
+  :: Unique
+trTYPEKey              = mkPreludeMiscIdUnique 510
+trTYPE'PtrRepLiftedKey = mkPreludeMiscIdUnique 511
+trRuntimeRepKey        = mkPreludeMiscIdUnique 512
+tr'PtrRepLiftedKey     = mkPreludeMiscIdUnique 513
 
 -- Dynamic
 toDynIdKey :: Unique
-toDynIdKey            = mkPreludeMiscIdUnique 509
+toDynIdKey            = mkPreludeMiscIdUnique 550
 
 bitIntegerIdKey :: Unique
-bitIntegerIdKey       = mkPreludeMiscIdUnique 510
+bitIntegerIdKey       = mkPreludeMiscIdUnique 551
 
 heqSCSelIdKey, coercibleSCSelIdKey :: Unique
-heqSCSelIdKey       = mkPreludeMiscIdUnique 511
-coercibleSCSelIdKey = mkPreludeMiscIdUnique 512
+heqSCSelIdKey       = mkPreludeMiscIdUnique 552
+coercibleSCSelIdKey = mkPreludeMiscIdUnique 553
 
 sappendClassOpKey :: Unique
-sappendClassOpKey = mkPreludeMiscIdUnique 513
+sappendClassOpKey = mkPreludeMiscIdUnique 554
 
 memptyClassOpKey, mappendClassOpKey, mconcatClassOpKey :: Unique
-memptyClassOpKey  = mkPreludeMiscIdUnique 514
-mappendClassOpKey = mkPreludeMiscIdUnique 515
-mconcatClassOpKey = mkPreludeMiscIdUnique 516
+memptyClassOpKey  = mkPreludeMiscIdUnique 555
+mappendClassOpKey = mkPreludeMiscIdUnique 556
+mconcatClassOpKey = mkPreludeMiscIdUnique 557
 
 emptyCallStackKey, pushCallStackKey :: Unique
-emptyCallStackKey = mkPreludeMiscIdUnique 517
-pushCallStackKey  = mkPreludeMiscIdUnique 518
+emptyCallStackKey = mkPreludeMiscIdUnique 558
+pushCallStackKey  = mkPreludeMiscIdUnique 559
 
 fromStaticPtrClassOpKey :: Unique
 fromStaticPtrClassOpKey = mkPreludeMiscIdUnique 519
diff --git a/compiler/prelude/THNames.hs b/compiler/prelude/THNames.hs
index 253a89b6e3..1b9e624c67 100644
--- a/compiler/prelude/THNames.hs
+++ b/compiler/prelude/THNames.hs
@@ -678,40 +678,40 @@ derivStrategyTyConKey   = mkPreludeTyConUnique 235
 
 -- data Inline = ...
 noInlineDataConKey, inlineDataConKey, inlinableDataConKey :: Unique
-noInlineDataConKey  = mkPreludeDataConUnique 100
-inlineDataConKey    = mkPreludeDataConUnique 101
-inlinableDataConKey = mkPreludeDataConUnique 102
+noInlineDataConKey  = mkPreludeDataConUnique 200
+inlineDataConKey    = mkPreludeDataConUnique 201
+inlinableDataConKey = mkPreludeDataConUnique 202
 
 -- data RuleMatch = ...
 conLikeDataConKey, funLikeDataConKey :: Unique
-conLikeDataConKey = mkPreludeDataConUnique 103
-funLikeDataConKey = mkPreludeDataConUnique 104
+conLikeDataConKey = mkPreludeDataConUnique 203
+funLikeDataConKey = mkPreludeDataConUnique 204
 
 -- data Phases = ...
 allPhasesDataConKey, fromPhaseDataConKey, beforePhaseDataConKey :: Unique
-allPhasesDataConKey   = mkPreludeDataConUnique 105
-fromPhaseDataConKey   = mkPreludeDataConUnique 106
-beforePhaseDataConKey = mkPreludeDataConUnique 107
+allPhasesDataConKey   = mkPreludeDataConUnique 205
+fromPhaseDataConKey   = mkPreludeDataConUnique 206
+beforePhaseDataConKey = mkPreludeDataConUnique 207
 
 -- newtype TExp a = ...
 tExpDataConKey :: Unique
-tExpDataConKey = mkPreludeDataConUnique 108
+tExpDataConKey = mkPreludeDataConUnique 208
 
 -- data Overlap = ..
 overlappableDataConKey,
   overlappingDataConKey,
   overlapsDataConKey,
   incoherentDataConKey :: Unique
-overlappableDataConKey = mkPreludeDataConUnique 109
-overlappingDataConKey  = mkPreludeDataConUnique 110
-overlapsDataConKey     = mkPreludeDataConUnique 111
-incoherentDataConKey   = mkPreludeDataConUnique 112
+overlappableDataConKey = mkPreludeDataConUnique 209
+overlappingDataConKey  = mkPreludeDataConUnique 210
+overlapsDataConKey     = mkPreludeDataConUnique 211
+incoherentDataConKey   = mkPreludeDataConUnique 212
 
 -- data DerivStrategy = ...
 stockDataConKey, anyclassDataConKey, newtypeDataConKey :: Unique
-stockDataConKey    = mkPreludeDataConUnique 113
-anyclassDataConKey = mkPreludeDataConUnique 114
-newtypeDataConKey  = mkPreludeDataConUnique 115
+stockDataConKey    = mkPreludeDataConUnique 213
+anyclassDataConKey = mkPreludeDataConUnique 214
+newtypeDataConKey  = mkPreludeDataConUnique 215
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 0eeb5e323a..85771a0da2 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -865,7 +865,7 @@ mk_tuple Unboxed arity = (tycon, tuple_con)
     tc_res_kind = unboxedTupleKind rr_tys
 
     tc_arity    = arity * 2
-    flavour     = UnboxedAlgTyCon
+    flavour     = UnboxedAlgTyCon (mkPrelTyConRepName tc_name)
 
     dc_tvs               = binderVars tc_binders
     (rr_tys, dc_arg_tys) = splitAt arity (mkTyVarTys dc_tvs)
@@ -974,7 +974,7 @@ mk_sum :: Arity -> (TyCon, Array ConTagZ DataCon)
 mk_sum arity = (tycon, sum_cons)
   where
     tycon   = mkSumTyCon tc_name tc_binders tc_res_kind (arity * 2) tyvars (elems sum_cons)
-                         UnboxedAlgTyCon
+                         (UnboxedAlgTyCon (mkPrelTyConRepName tc_name))
 
     tc_binders = mkTemplateTyConBinders (nOfThem arity runtimeRepTy)
                                         (\ks -> map tYPE ks)
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 65acf808ab..3e462744e1 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -60,25 +60,22 @@ import Data.List ( sortBy, mapAccumL )
 import Data.Maybe ( isJust )
 import qualified Data.Set as Set ( difference, fromList, toList, null )
 
-{-
-@rnSourceDecl@ `renames' declarations.
+{- | @rnSourceDecl@ "renames" declarations.
 It simultaneously performs dependency analysis and precedence parsing.
 It also does the following error checks:
-\begin{enumerate}
-\item
-Checks that tyvars are used properly. This includes checking
-for undefined tyvars, and tyvars in contexts that are ambiguous.
-(Some of this checking has now been moved to module @TcMonoType@,
-since we don't have functional dependency information at this point.)
-\item
-Checks that all variable occurrences are defined.
-\item
-Checks the @(..)@ etc constraints in the export list.
-\end{enumerate}
--}
 
--- Brings the binders of the group into scope in the appropriate places;
--- does NOT assume that anything is in scope already
+* Checks that tyvars are used properly. This includes checking
+  for undefined tyvars, and tyvars in contexts that are ambiguous.
+  (Some of this checking has now been moved to module @TcMonoType@,
+  since we don't have functional dependency information at this point.)
+
+* Checks that all variable occurrences are defined.
+
+* Checks the @(..)@ etc constraints in the export list.
+
+Brings the binders of the group into scope in the appropriate places;
+does NOT assume that anything is in scope already
+-}
 rnSrcDecls :: HsGroup RdrName -> RnM (TcGblEnv, HsGroup Name)
 -- Rename a top-level HsGroup; used for normal source files *and* hs-boot files
 rnSrcDecls group@(HsGroup { hs_valds   = val_decls,
diff --git a/compiler/typecheck/TcBackpack.hs b/compiler/typecheck/TcBackpack.hs
index a2e5abef9e..2b4b05cd9b 100644
--- a/compiler/typecheck/TcBackpack.hs
+++ b/compiler/typecheck/TcBackpack.hs
@@ -438,8 +438,8 @@ inheritedSigPvpWarning =
 -- the export lists of two signatures is just merging the declarations
 -- of two signatures writ small.  Of course, in GHC Haskell, there are a
 -- few important things which are not explicitly exported but still can
--- be used:  in particular, dictionary functions for instances and
--- coercion axioms for type families also count.
+-- be used:  in particular, dictionary functions for instances, Typeable
+-- TyCon bindings, and coercion axioms for type families also count.
 --
 -- When handling these non-exported things, there two primary things
 -- we need to watch out for:
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 2de2223ed6..4455c9bd6a 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -493,19 +493,24 @@ data EvTerm
 -- | Instructions on how to make a 'Typeable' dictionary.
 -- See Note [Typeable evidence terms]
 data EvTypeable
-  = EvTypeableTyCon [EvTerm]  -- ^ Dictionary for @Typeable (T k1..kn)@.
-                              -- The EvTerms are for the arguments
+  = EvTypeableTyCon TyCon [EvTerm]
+    -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
+    -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
+    -- the applied kinds..
 
   | EvTypeableTyApp EvTerm EvTerm
     -- ^ Dictionary for @Typeable (s t)@,
-    -- given a dictionaries for @s@ and @t@
+    -- given a dictionaries for @s@ and @t@.
+
+  | EvTypeableTrFun EvTerm EvTerm
+    -- ^ Dictionary for @Typeable (s -> t)@,
+    -- given a dictionaries for @s@ and @t@.
 
   | EvTypeableTyLit EvTerm
     -- ^ Dictionary for a type literal,
     -- e.g. @Typeable "foo"@ or @Typeable 3@
     -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
     -- (see Trac #10348)
-
   deriving Data.Data
 
 data EvLit
@@ -817,8 +822,9 @@ evVarsOfCallStack cs = case cs of
 evVarsOfTypeable :: EvTypeable -> VarSet
 evVarsOfTypeable ev =
   case ev of
-    EvTypeableTyCon es    -> evVarsOfTerms es
+    EvTypeableTyCon _ e   -> mapUnionVarSet evVarsOfTerm e
     EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
+    EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
     EvTypeableTyLit e     -> evVarsOfTerm e
 
 {-
@@ -908,8 +914,9 @@ instance Outputable EvCallStack where
     = ppr (name,loc) <+> text ":" <+> ppr tm
 
 instance Outputable EvTypeable where
-  ppr (EvTypeableTyCon ts)    = text "TC" <+> ppr ts
+  ppr (EvTypeableTyCon ts _)  = text "TyCon" <+> ppr ts
   ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
+  ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
   ppr (EvTypeableTyLit t1)    = text "TyLit" <> ppr t1
 
 
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 6061eccf60..6ad2b281f9 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -615,7 +615,7 @@ zonkLExprs env exprs = mapM (zonkLExpr env) exprs
 zonkLExpr  env expr  = wrapLocM (zonkExpr env) expr
 
 zonkExpr env (HsVar (L l id))
-  = ASSERT( isNothing (isDataConId_maybe id) )
+  = ASSERT2( isNothing (isDataConId_maybe id), ppr id )
     return (HsVar (L l (zonkIdOcc env id)))
 
 zonkExpr _ e@(HsConLikeOut {}) = return e
@@ -1451,13 +1451,17 @@ zonkEvTerm env (EvSelector sel_id tys tms)
        ; return (EvSelector sel_id' tys' tms') }
 
 zonkEvTypeable :: ZonkEnv -> EvTypeable -> TcM EvTypeable
-zonkEvTypeable env (EvTypeableTyCon ts)
-  = do { ts' <- mapM (zonkEvTerm env) ts
-       ; return $ EvTypeableTyCon ts' }
+zonkEvTypeable env (EvTypeableTyCon tycon e)
+  = do { e'  <- mapM (zonkEvTerm env) e
+       ; return $ EvTypeableTyCon tycon e' }
 zonkEvTypeable env (EvTypeableTyApp t1 t2)
   = do { t1' <- zonkEvTerm env t1
        ; t2' <- zonkEvTerm env t2
        ; return (EvTypeableTyApp t1' t2') }
+zonkEvTypeable env (EvTypeableTrFun t1 t2)
+  = do { t1' <- zonkEvTerm env t1
+       ; t2' <- zonkEvTerm env t2
+       ; return (EvTypeableTrFun t1' t2') }
 zonkEvTypeable env (EvTypeableTyLit t1)
   = do { t1' <- zonkEvTerm env t1
        ; return (EvTypeableTyLit t1') }
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index e01bd64f36..e1ad484d58 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -2403,28 +2403,41 @@ matchTypeable clas [k,t]  -- clas = Typeable
   | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
 
   -- Now cases that do work
-  | k `eqType` typeNatKind                 = doTyLit knownNatClassName    t
-  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName t
+  | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
+  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
+  | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
   | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
-  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t ks
+  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
   | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
 
 matchTypeable _ _ = return NoInstance
 
-doTyConApp :: Class -> Type -> [Kind] -> TcS LookupInstResult
--- Representation for type constructor applied to some kinds
-doTyConApp clas ty args
-  = return $ GenInst (map (mk_typeable_pred clas) args)
-                     (\tms -> EvTypeable ty $ EvTypeableTyCon tms)
+-- | Representation for a type @ty@ of the form @arg -> ret@.
+doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
+doFunTy clas ty arg_ty ret_ty
+  = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
+             build_ev [arg_ev, ret_ev] =
+                 EvTypeable ty $ EvTypeableTrFun arg_ev ret_ev
+             build_ev _ = panic "TcInteract.doFunTy"
+       ; return $ GenInst preds build_ev True
+       }
+
+-- | Representation for type constructor applied to some kinds.
+-- 'onlyNamedBndrsApplied' has ensured that this application results in a type
+-- of monomorphic kind (e.g. all kind variables have been instantiated).
+doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
+doTyConApp clas ty tc kind_args
+  = return $ GenInst (map (mk_typeable_pred clas) kind_args)
+                     (\kinds -> EvTypeable ty $ EvTypeableTyCon tc kinds)
                      True
 
--- Representation for concrete kinds.  We just use the kind itself,
--- but first we must make sure that we've instantiated all kind-
+-- | Representation for TyCon applications of a concrete kind. We just use the
+-- kind itself, but first we must make sure that we've instantiated all kind-
 -- polymorphism, but no more.
 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
 onlyNamedBndrsApplied tc ks
- = all isNamedTyConBinder         used_bndrs &&
-   all (not . isNamedTyConBinder) leftover_bndrs
+ = all isNamedTyConBinder used_bndrs &&
+   not (any isNamedTyConBinder leftover_bndrs)
  where
    bndrs                        = tyConBinders tc
    (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
@@ -2441,10 +2454,9 @@ doTyApp clas ty f tk
   | isForAllTy (typeKind f)
   = return NoInstance -- We can't solve until we know the ctr.
   | otherwise
-  = do { traceTcS "doTyApp" (ppr clas $$ ppr ty $$ ppr f $$ ppr tk)
-       ; return $ GenInst [mk_typeable_pred clas f, mk_typeable_pred clas tk]
+  = return $ GenInst (map (mk_typeable_pred clas) [f, tk])
                      (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2)
-                     True }
+                     True
 
 -- Emit a `Typeable` constraint for the given type.
 mk_typeable_pred :: Class -> Type -> PredType
@@ -2472,7 +2484,9 @@ To solve Typeable (Proxy (* -> *) Maybe) we
   - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
 
 If we attempt to short-cut by solving it all at once, via
-doTyCOnAPp
+doTyConApp
+
+(this note is sadly truncated FIXME)
 
 
 Note [No Typeable for polytypes or qualified types]
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 05ed92a0d1..082b2fd693 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -588,6 +588,10 @@ tcRnHsBootDecls hsc_src decls
              <- tcTyClsInstDecls tycl_decls deriv_decls val_binds
         ; setGblEnv tcg_env     $ do {
 
+        -- Emit Typeable bindings
+        ; tcg_env <- mkTypeableBinds
+        ; setGblEnv tcg_env $ do {
+
                 -- Typecheck value declarations
         ; traceTc "Tc5" empty
         ; val_ids <- tcHsBootSigs val_binds val_sigs
@@ -607,7 +611,7 @@ tcRnHsBootDecls hsc_src decls
               }
 
         ; setGlobalTypeEnv gbl_env type_env2
-   }}
+   }}}
    ; traceTc "boot" (ppr lie); return gbl_env }
 
 badBootDecl :: HscSource -> String -> Located decl -> TcM ()
diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs
index 86d1d1cb45..e7fe588f76 100644
--- a/compiler/typecheck/TcTypeable.hs
+++ b/compiler/typecheck/TcTypeable.hs
@@ -8,27 +8,39 @@
 module TcTypeable(mkTypeableBinds) where
 
 
-import BasicTypes ( SourceText(..) )
+import BasicTypes ( SourceText(..), Boxity(..), neverInlinePragma )
 import TcBinds( addTypecheckedBinds )
 import IfaceEnv( newGlobalBinder )
+import TyCoRep( Type(..), TyLit(..) )
 import TcEnv
+import TcEvidence ( mkWpTyApps )
 import TcRnMonad
+import TcMType ( zonkTcType )
+import HscTypes ( lookupId )
 import PrelNames
 import TysPrim ( primTyCons )
+import TysWiredIn ( tupleTyCon, sumTyCon, runtimeRepTyCon
+                  , vecCountTyCon, vecElemTyCon
+                  , nilDataCon, consDataCon )
 import Id
 import Type
+import Kind ( isTYPEApp )
 import TyCon
 import DataCon
-import Name( getOccName )
+import Name ( getOccName )
 import OccName
 import Module
 import HsSyn
 import DynFlags
 import Bag
-import Fingerprint(Fingerprint(..), fingerprintString)
+import Var ( TyVarBndr(..) )
+import VarEnv
+import Constants
+import Fingerprint(Fingerprint(..), fingerprintString, fingerprintFingerprints)
 import Outputable
-import FastString ( FastString, mkFastString )
+import FastString ( FastString, mkFastString, fsLit )
 
+import Data.Maybe ( isJust )
 import Data.Word( Word64 )
 
 {- Note [Grand plan for Typeable]
@@ -51,9 +63,22 @@ The overall plan is this:
        M.$tcT = TyCon ...fingerprint info...
                       $trModule
                       "T"
+                      0#
+                      kind_rep
+
+   Here 0# is the number of arguments expected by the tycon to fully determine
+   its kind. kind_rep is a value of type GHC.Types.KindRep, which gives a
+   recipe for computing the kind of an instantiation of the tycon (see
+   Note [Representing TyCon kinds] later in this file for details).
+
    We define (in TyCon)
-      type TyConRepName = Name
-   to use for these M.$tcT "tycon rep names".
+
+        type TyConRepName = Name
+
+   to use for these M.$tcT "tycon rep names". Note that these must be
+   treated as "never exported" names by Backpack (see
+   Note [Handling never-exported TyThings under Backpack]). Consequently
+   they get slightly special treatment in RnModIface.rnIfaceDecl.
 
 3. Record the TyConRepName in T's TyCon, including for promoted
    data and type constructors, and kinds like * and #.
@@ -86,6 +111,25 @@ There are many wrinkles:
   representations for TyCon and Module.  See GHC.Types
   Note [Runtime representation of modules and tycons]
 
+* The KindReps can unfortunately get quite large. Moreover, the simplifier will
+  float out various pieces of them, resulting in numerous top-level bindings.
+  Consequently we mark the KindRep bindings as noinline, ensuring that the
+  float-outs don't make it into the interface file. This is important since
+  there is generally little benefit to inlining KindReps and they would
+  otherwise strongly affect compiler performance.
+
+* Even KindReps aren't inlined this scheme still has more of an effect on
+  compilation time than I'd like. This is especially true in the case of
+  families of type constructors (e.g. tuples and unboxed sums). The problem is
+  particularly bad in the case of sums, since each arity-N tycon brings with it
+  N promoted datacons, each with a KindRep whose size also scales with N.
+  Consequently we currently simply don't allow sums to be Typeable.
+
+  In general we might consider moving some or all of this generation logic back
+  to the solver since the performance hit we take in doing this at
+  type-definition time is non-trivial and Typeable isn't very widely used. This
+  is discussed in #13261.
+
 -}
 
 -- | Generate the Typeable bindings for a module. This is the only
@@ -101,16 +145,24 @@ mkTypeableBinds
        ; tcg_env <- mkModIdBindings
          -- Now we can generate the TyCon representations...
          -- First we handle the primitive TyCons if we are compiling GHC.Types
-       ; tcg_env <- setGblEnv tcg_env mkPrimTypeableBinds
+       ; (tcg_env, prim_todos) <- setGblEnv tcg_env mkPrimTypeableTodos
+
          -- Then we produce bindings for the user-defined types in this module.
        ; setGblEnv tcg_env $
-
-    do { let tycons = filter needs_typeable_binds (tcg_tcs tcg_env)
+    do { mod <- getModule
+       ; let tycons = filter needs_typeable_binds (tcg_tcs tcg_env)
+             mod_id = case tcg_tr_module tcg_env of  -- Should be set by now
+                        Just mod_id -> mod_id
+                        Nothing     -> pprPanic "tcMkTypeableBinds" (ppr tycons)
        ; traceTc "mkTypeableBinds" (ppr tycons)
-       ; mkTypeableTyConBinds tycons
+       ; this_mod_todos <- todoForTyCons mod mod_id tycons
+       ; mkTypeableTyConBinds (this_mod_todos : prim_todos)
        } }
   where
-    needs_typeable_binds tc =
+    needs_typeable_binds tc
+      | tc `elem` [runtimeRepTyCon, vecCountTyCon, vecElemTyCon]
+      = False
+      | otherwise =
           (not (isFamInstTyCon tc) && isAlgTyCon tc)
        || isDataFamilyTyCon tc
        || isClassTyCon tc
@@ -140,8 +192,8 @@ mkModIdRHS mod
   = do { trModuleDataCon <- tcLookupDataCon trModuleDataConName
        ; trNameLit <- mkTrNameLit
        ; return $ nlHsDataCon trModuleDataCon
-                 `nlHsApp` (nlHsPar $ trNameLit (unitIdFS (moduleUnitId mod)))
-                 `nlHsApp` (nlHsPar $ trNameLit (moduleNameFS (moduleName mod)))
+                  `nlHsApp` trNameLit (unitIdFS (moduleUnitId mod))
+                  `nlHsApp` trNameLit (moduleNameFS (moduleName mod))
        }
 
 {- *********************************************************************
@@ -150,30 +202,93 @@ mkModIdRHS mod
 *                                                                      *
 ********************************************************************* -}
 
+-- | Information we need about a 'TyCon' to generate its representation.
+data TypeableTyCon
+    = TypeableTyCon
+      { tycon        :: !TyCon
+      , tycon_kind   :: !Kind
+      , tycon_rep_id :: !Id
+      }
+
+-- | A group of 'TyCon's in need of type-rep bindings.
+data TypeRepTodo
+    = TypeRepTodo
+      { mod_rep_expr    :: LHsExpr Id       -- ^ Module's typerep binding
+      , pkg_fingerprint :: !Fingerprint     -- ^ Package name fingerprint
+      , mod_fingerprint :: !Fingerprint     -- ^ Module name fingerprint
+      , todo_tycons     :: [TypeableTyCon]
+        -- ^ The 'TyCon's in need of bindings and their zonked kinds
+      }
+
+todoForTyCons :: Module -> Id -> [TyCon] -> TcM TypeRepTodo
+todoForTyCons mod mod_id tycons = do
+    trTyConTyCon <- tcLookupTyCon trTyConTyConName
+    let mkRepId :: TyConRepName -> Id
+        mkRepId rep_name = mkExportedVanillaId rep_name (mkTyConTy trTyConTyCon)
+
+    tycons <- sequence
+              [ do kind <- zonkTcType $ tyConKind tc''
+                   return TypeableTyCon { tycon = tc''
+                                        , tycon_kind = kind
+                                        , tycon_rep_id = mkRepId rep_name
+                                        }
+              | tc     <- tycons
+              , tc'    <- tc : tyConATs tc
+                -- If the tycon itself isn't typeable then we needn't look
+                -- at its promoted datacons as their kinds aren't Typeable
+              , Just _ <- pure $ tyConRepName_maybe tc'
+                -- We need type representations for any associated types
+              , let promoted = map promoteDataCon (tyConDataCons tc')
+              , tc''   <- tc' : promoted
+              , Just rep_name <- pure $ tyConRepName_maybe tc''
+              ]
+    let typeable_tycons = filter is_typeable tycons
+        is_typeable (TypeableTyCon {..}) =
+            --pprTrace "todoForTycons" (ppr tycon $$ ppr bare_kind $$ ppr is_typeable)
+            (typeIsTypeable bare_kind)
+          where bare_kind = dropForAlls tycon_kind
+    return TypeRepTodo { mod_rep_expr    = nlHsVar mod_id
+                       , pkg_fingerprint = pkg_fpr
+                       , mod_fingerprint = mod_fpr
+                       , todo_tycons     = typeable_tycons
+                       }
+  where
+    mod_fpr = fingerprintString $ moduleNameString $ moduleName mod
+    pkg_fpr = fingerprintString $ unitIdString $ moduleUnitId mod
+
 -- | Generate TyCon bindings for a set of type constructors
-mkTypeableTyConBinds :: [TyCon] -> TcM TcGblEnv
-mkTypeableTyConBinds tycons
-  = do { gbl_env <- getGblEnv
-       ; mod <- getModule
-       ; let mod_expr = case tcg_tr_module gbl_env of  -- Should be set by now
-                           Just mod_id -> nlHsVar mod_id
-                           Nothing     -> pprPanic "tcMkTypeableBinds" (ppr tycons)
-       ; stuff <- collect_stuff mod mod_expr
-       ; let all_tycons = [ tc' | tc <- tycons, tc' <- tc : tyConATs tc ]
-                             -- We need type representations for any associated types
-             tc_binds = map (mk_typeable_binds stuff) all_tycons
-             tycon_rep_ids = foldr ((++) . collectHsBindsBinders) [] tc_binds
-
-       ; gbl_env <- tcExtendGlobalValEnv tycon_rep_ids getGblEnv
-       ; return (gbl_env `addTypecheckedBinds` tc_binds) }
-
--- | Generate bindings for the type representation of a wired-in TyCon defined
--- by the virtual "GHC.Prim" module. This is where we inject the representation
--- bindings for primitive types into "GHC.Types"
+mkTypeableTyConBinds :: [TypeRepTodo] -> TcM TcGblEnv
+mkTypeableTyConBinds [] = getGblEnv
+mkTypeableTyConBinds todos
+  = do { stuff <- collect_stuff
+
+         -- First extend the type environment with all of the bindings which we
+         -- are going to produce since we may need to refer to them while
+         -- generating the kind representations of other types.
+       ; let tycon_rep_bndrs :: [Id]
+             tycon_rep_bndrs = [ tycon_rep_id
+                               | todo <- todos
+                               , TypeableTyCon {..} <- todo_tycons todo
+                               ]
+       ; gbl_env <- tcExtendGlobalValEnv tycon_rep_bndrs getGblEnv
+
+       ; setGblEnv gbl_env $ foldlM (mk_typeable_binds stuff) gbl_env todos }
+
+-- | Make bindings for the type representations of a 'TyCon' and its
+-- promoted constructors.
+mk_typeable_binds :: TypeableStuff -> TcGblEnv -> TypeRepTodo -> TcM TcGblEnv
+mk_typeable_binds stuff gbl_env todo
+  = do pairs <- mapM (mkTyConRepBinds stuff todo) (todo_tycons todo)
+       gbl_env <- tcExtendGlobalValEnv (map fst pairs) (return gbl_env)
+       return $ gbl_env `addTypecheckedBinds` map snd pairs
+
+-- | Generate bindings for the type representation of a wired-in 'TyCon's
+-- defined by the virtual "GHC.Prim" module. This is where we inject the
+-- representation bindings for these primitive types into "GHC.Types"
 --
 -- See Note [Grand plan for Typeable] in this module.
-mkPrimTypeableBinds :: TcM TcGblEnv
-mkPrimTypeableBinds
+mkPrimTypeableTodos :: TcM (TcGblEnv, [TypeRepTodo])
+mkPrimTypeableTodos
   = do { mod <- getModule
        ; if mod == gHC_TYPES
            then do { trModuleTyCon <- tcLookupTyCon trModuleTyConName
@@ -184,58 +299,66 @@ mkPrimTypeableBinds
                    ; ghc_prim_module_bind <- mkVarBind ghc_prim_module_id
                                              <$> mkModIdRHS gHC_PRIM
 
-                   ; stuff <- collect_stuff gHC_PRIM (nlHsVar ghc_prim_module_id)
-                   ; let prim_binds :: LHsBinds Id
-                         prim_binds = unitBag ghc_prim_module_bind
-                                      `unionBags` ghcPrimTypeableBinds stuff
-
-                         prim_rep_ids = collectHsBindsBinders prim_binds
-                   ; gbl_env <- tcExtendGlobalValEnv prim_rep_ids getGblEnv
-                   ; return (gbl_env `addTypecheckedBinds` [prim_binds])
+                   ; gbl_env <- tcExtendGlobalValEnv [ghc_prim_module_id] getGblEnv
+                   ; let gbl_env' = gbl_env `addTypecheckedBinds`
+                                    [unitBag ghc_prim_module_bind]
+                   ; todo <- todoForTyCons gHC_PRIM ghc_prim_module_id
+                                           ghcPrimTypeableTyCons
+                   ; return (gbl_env', [todo])
                    }
-           else getGblEnv
+           else do gbl_env <- getGblEnv
+                   return (gbl_env, [])
        }
   where
 
--- | Generate bindings for the type representation of the wired-in TyCons defined
--- by the virtual "GHC.Prim" module. This differs from the usual
--- @mkTypeableBinds@ path in that here we need to lie to 'mk_typeable_binds'
--- about the module we are compiling (since we are currently compiling
--- "GHC.Types" yet are producing representations for types in "GHC.Prim").
+-- | This is the list of primitive 'TyCon's for which we must generate bindings
+-- in "GHC.Types". This should include all types defined in "GHC.Prim".
 --
--- See Note [Grand plan for Typeable] in this module.
-ghcPrimTypeableBinds :: TypeableStuff -> LHsBinds Id
-ghcPrimTypeableBinds stuff
-  = unionManyBags (map mkBind all_prim_tys)
-  where
-    all_prim_tys :: [TyCon]
-    all_prim_tys = [ tc' | tc <- funTyCon : primTyCons
-                         , tc' <- tc : tyConATs tc ]
-
-    mkBind :: TyCon -> LHsBinds Id
-    mkBind = mk_typeable_binds stuff
+-- The majority of the types we need here are contained in 'primTyCons'.
+-- However, not all of them: in particular unboxed tuples are absent since we
+-- don't want to include them in the original name cache. See
+-- Note [Built-in syntax and the OrigNameCache] in IfaceEnv for more.
+ghcPrimTypeableTyCons :: [TyCon]
+ghcPrimTypeableTyCons = concat
+    [ [ runtimeRepTyCon, vecCountTyCon, vecElemTyCon
+      , funTyCon, tupleTyCon Unboxed 0]
+    , map (tupleTyCon Unboxed) [2..mAX_TUPLE_SIZE]
+    , map sumTyCon [2..mAX_SUM_SIZE]
+    , primTyCons
+    ]
 
 data TypeableStuff
     = Stuff { dflags         :: DynFlags
-            , mod_rep        :: LHsExpr Id  -- ^ Of type GHC.Types.Module
-            , pkg_str        :: String      -- ^ Package name
-            , mod_str        :: String      -- ^ Module name
-            , trTyConTyCon   :: TyCon       -- ^ of @TyCon@
-            , trTyConDataCon :: DataCon     -- ^ of @TyCon@
+            , trTyConDataCon :: DataCon         -- ^ of @TyCon@
             , trNameLit      :: FastString -> LHsExpr Id
-                                            -- ^ To construct @TrName@s
+                                                -- ^ To construct @TrName@s
+              -- The various TyCon and DataCons of KindRep
+            , kindRepTyCon           :: TyCon
+            , kindRepTyConAppDataCon :: DataCon
+            , kindRepVarDataCon      :: DataCon
+            , kindRepAppDataCon      :: DataCon
+            , kindRepFunDataCon      :: DataCon
+            , kindRepTYPEDataCon     :: DataCon
+            , kindRepTypeLitSDataCon :: DataCon
+            , typeLitSymbolDataCon   :: DataCon
+            , typeLitNatDataCon      :: DataCon
             }
 
 -- | Collect various tidbits which we'll need to generate TyCon representations.
-collect_stuff :: Module -> LHsExpr Id -> TcM TypeableStuff
-collect_stuff mod mod_rep = do
+collect_stuff :: TcM TypeableStuff
+collect_stuff = do
     dflags <- getDynFlags
-    let pkg_str  = unitIdString (moduleUnitId mod)
-        mod_str  = moduleNameString (moduleName mod)
-
-    trTyConTyCon   <- tcLookupTyCon trTyConTyConName
-    trTyConDataCon <- tcLookupDataCon trTyConDataConName
-    trNameLit      <- mkTrNameLit
+    trTyConDataCon         <- tcLookupDataCon trTyConDataConName
+    kindRepTyCon           <- tcLookupTyCon   kindRepTyConName
+    kindRepTyConAppDataCon <- tcLookupDataCon kindRepTyConAppDataConName
+    kindRepVarDataCon      <- tcLookupDataCon kindRepVarDataConName
+    kindRepAppDataCon      <- tcLookupDataCon kindRepAppDataConName
+    kindRepFunDataCon      <- tcLookupDataCon kindRepFunDataConName
+    kindRepTYPEDataCon     <- tcLookupDataCon kindRepTYPEDataConName
+    kindRepTypeLitSDataCon <- tcLookupDataCon kindRepTypeLitSDataConName
+    typeLitSymbolDataCon   <- tcLookupDataCon typeLitSymbolDataConName
+    typeLitNatDataCon      <- tcLookupDataCon typeLitNatDataConName
+    trNameLit              <- mkTrNameLit
     return Stuff {..}
 
 -- | Lookup the necessary pieces to construct the @trNameLit@. We do this so we
@@ -245,49 +368,207 @@ mkTrNameLit :: TcM (FastString -> LHsExpr Id)
 mkTrNameLit = do
     trNameSDataCon <- tcLookupDataCon trNameSDataConName
     let trNameLit :: FastString -> LHsExpr Id
-        trNameLit fs = nlHsDataCon trNameSDataCon
+        trNameLit fs = nlHsPar $ nlHsDataCon trNameSDataCon
                        `nlHsApp` nlHsLit (mkHsStringPrimLit fs)
     return trNameLit
 
--- | Make bindings for the type representations of a 'TyCon' and its
--- promoted constructors.
-mk_typeable_binds :: TypeableStuff -> TyCon -> LHsBinds Id
-mk_typeable_binds stuff tycon
-  = mkTyConRepBinds stuff tycon
-    `unionBags`
-    unionManyBags (map (mkTyConRepBinds stuff . promoteDataCon)
-                       (tyConDataCons tycon))
-
 -- | Make typeable bindings for the given 'TyCon'.
-mkTyConRepBinds :: TypeableStuff -> TyCon -> LHsBinds Id
-mkTyConRepBinds stuff@(Stuff {..}) tycon
-  = case tyConRepName_maybe tycon of
-      Just rep_name -> unitBag (mkVarBind rep_id rep_rhs)
-         where
-           rep_id  = mkExportedVanillaId rep_name (mkTyConTy trTyConTyCon)
-           rep_rhs = mkTyConRepRHS stuff tycon
-      _ -> emptyBag
+mkTyConRepBinds :: TypeableStuff -> TypeRepTodo
+                -> TypeableTyCon -> TcRn (Id, LHsBinds Id)
+mkTyConRepBinds stuff@(Stuff {..}) todo (TypeableTyCon {..})
+  = do -- Place a NOINLINE pragma on KindReps since they tend to be quite large
+       -- and bloat interface files.
+       kind_rep_id <- (`setInlinePragma` neverInlinePragma)
+                      <$> newSysLocalId (fsLit "krep") (mkTyConTy kindRepTyCon)
+       kind_rep <- mkTyConKindRep stuff tycon tycon_kind
+
+       tycon_rep_rhs <- mkTyConRepTyConRHS stuff todo tycon kind_rep_id
+       let tycon_rep_bind = mkVarBind tycon_rep_id tycon_rep_rhs
+           kind_rep_bind = mkVarBind kind_rep_id kind_rep
+       return (kind_rep_id, listToBag [tycon_rep_bind, kind_rep_bind])
+
+-- | Here is where we define the set of Typeable types. These exclude type
+-- families and polytypes.
+tyConIsTypeable :: TyCon -> Bool
+tyConIsTypeable tc =
+       isJust (tyConRepName_maybe tc)
+    && typeIsTypeable (dropForAlls $ tyConKind tc)
+      -- Ensure that the kind of the TyCon, with its initial foralls removed,
+      -- is representable (e.g. has no higher-rank polymorphism or type
+      -- synonyms).
+
+-- | Is a particular 'Type' representable by @Typeable@? Here we look for
+-- polytypes and types containing casts (which may be, for instance, a type
+-- family).
+typeIsTypeable :: Type -> Bool
+-- We handle types of the form (TYPE rep) specifically to avoid
+-- looping on (tyConIsTypeable RuntimeRep)
+typeIsTypeable ty
+  | Just ty' <- coreView ty         = typeIsTypeable ty'
+typeIsTypeable ty
+  | Just _ <- isTYPEApp ty          = True
+typeIsTypeable (TyVarTy _)          = True
+typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
+typeIsTypeable (FunTy a b)          = typeIsTypeable a && typeIsTypeable b
+typeIsTypeable (TyConApp tc args)   = tyConIsTypeable tc
+                                   && all typeIsTypeable args
+typeIsTypeable (ForAllTy{})         = False
+typeIsTypeable (LitTy _)            = True
+typeIsTypeable (CastTy{})           = False
+typeIsTypeable (CoercionTy{})       = panic "typeIsTypeable(Coercion)"
 
 -- | Produce the right-hand-side of a @TyCon@ representation.
-mkTyConRepRHS :: TypeableStuff -> TyCon -> LHsExpr Id
-mkTyConRepRHS (Stuff {..}) tycon = rep_rhs
+mkTyConRepTyConRHS :: TypeableStuff -> TypeRepTodo
+                   -> TyCon -> Id
+                   -> TcRn (LHsExpr Id)
+mkTyConRepTyConRHS (Stuff {..}) todo tycon kind_rep_id
+  = do let rep_rhs = nlHsDataCon trTyConDataCon
+                     `nlHsApp` nlHsLit (word64 dflags high)
+                     `nlHsApp` nlHsLit (word64 dflags low)
+                     `nlHsApp` mod_rep_expr todo
+                     `nlHsApp` trNameLit (mkFastString tycon_str)
+                     `nlHsApp` nlHsLit (int n_kind_vars)
+                     `nlHsApp` nlHsVar kind_rep_id
+       return rep_rhs
   where
-    rep_rhs = nlHsDataCon trTyConDataCon
-              `nlHsApp` nlHsLit (word64 high)
-              `nlHsApp` nlHsLit (word64 low)
-              `nlHsApp` mod_rep
-              `nlHsApp` (nlHsPar $ trNameLit (mkFastString tycon_str))
-
+    n_kind_vars = length $ filter isNamedTyConBinder (tyConBinders tycon)
     tycon_str = add_tick (occNameString (getOccName tycon))
     add_tick s | isPromotedDataCon tycon = '\'' : s
                | otherwise               = s
 
-    hashThis :: String
-    hashThis = unwords [pkg_str, mod_str, tycon_str]
+    -- This must match the computation done in
+    -- Data.Typeable.Internal.mkTyConFingerprint.
+    Fingerprint high low = fingerprintFingerprints [ pkg_fingerprint todo
+                                                   , mod_fingerprint todo
+                                                   , fingerprintString tycon_str
+                                                   ]
+
+    int :: Int -> HsLit
+    int n = HsIntPrim (SourceText $ show n) (toInteger n)
 
-    Fingerprint high low = fingerprintString hashThis
+word64 :: DynFlags -> Word64 -> HsLit
+word64 dflags n
+  | wORD_SIZE dflags == 4 = HsWord64Prim NoSourceText (toInteger n)
+  | otherwise             = HsWordPrim   NoSourceText (toInteger n)
 
-    word64 :: Word64 -> HsLit
-    word64
-      | wORD_SIZE dflags == 4 = \n -> HsWord64Prim NoSourceText (toInteger n)
-      | otherwise             = \n -> HsWordPrim   NoSourceText (toInteger n)
+{-
+Note [Representing TyCon kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+One of the operations supported by Typeable is typeRepKind,
+
+    typeRepKind :: TypeRep (a :: k) -> TypeRep k
+
+Implementing this is a bit tricky. To see why let's consider the TypeRep
+encoding of `Proxy Int` where
+
+    data Proxy (a :: k) :: Type
+
+which looks like,
+
+    $tcProxy :: TyCon
+    $trInt   :: TypeRep Int
+    $trType  :: TypeRep Type
+
+    $trProxyType :: TypeRep (Proxy :: Type -> Type)
+    $trProxyType = TrTyCon $tcProxy
+                           [$trType]  -- kind variable instantiation
+
+    $trProxy :: TypeRep (Proxy Int)
+    $trProxy = TrApp $trProxyType $trInt
+
+Note how $trProxyType encodes only the kind variables of the TyCon
+instantiation. To compute the kind (Proxy Int) we need to have a recipe to
+compute the kind of a concrete instantiation of Proxy. We call this recipe a
+KindRep and store it in the TyCon produced for Proxy,
+
+    type KindBndr = Int   -- de Bruijn index
+
+    data KindRep = KindRepTyConApp TyCon [KindRep]
+                 | KindRepVar !KindBndr
+                 | KindRepApp KindRep KindRep
+                 | KindRepFun KindRep KindRep
+
+The KindRep for Proxy would look like,
+
+    $tkProxy :: KindRep
+    $tkProxy = KindRepFun (KindRepVar 0) (KindRepTyConApp $trType [])
+
+
+data Maybe a = Nothing | Just a
+
+'Just :: a -> Maybe a
+
+F :: forall k. k -> forall k'. k' -> Type
+-}
+
+-- | Produce a @KindRep@ expression for the kind of the given 'TyCon'.
+mkTyConKindRep :: TypeableStuff -> TyCon -> Kind -> TcRn (LHsExpr Id)
+mkTyConKindRep (Stuff {..}) tycon tycon_kind = do
+    let (bndrs, kind) = splitForAllTyVarBndrs tycon_kind
+        bndr_idxs = mkVarEnv $ (`zip` [0..]) $ map binderVar bndrs
+    traceTc "mkTyConKindRepBinds"
+             (ppr tycon $$ ppr tycon_kind $$ ppr kind $$ ppr bndr_idxs)
+    go bndr_idxs kind
+  where
+    -- Compute RHS
+    go :: VarEnv Int -> Kind -> TcRn (LHsExpr Id)
+    go bndrs ty
+      | Just ty' <- coreView ty
+      = go bndrs ty'
+    go bndrs (TyVarTy v)
+      | Just idx <- lookupVarEnv bndrs v
+      = return $ nlHsDataCon kindRepVarDataCon
+                 `nlHsApp` nlHsIntLit (fromIntegral idx)
+      | otherwise
+      = pprPanic "mkTyConKindRepBinds.go(tyvar)" (ppr v $$ ppr bndrs)
+    go bndrs (AppTy t1 t2)
+      = do t1' <- go bndrs t1
+           t2' <- go bndrs t2
+           return $ nlHsDataCon kindRepAppDataCon
+                    `nlHsApp` t1' `nlHsApp` t2'
+    go _ ty | Just rr <- isTYPEApp ty
+      = return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon rr
+    go bndrs (TyConApp tc tys)
+      | Just rep_name <- tyConRepName_maybe tc
+      = do rep_id <- lookupId rep_name
+           tys' <- mapM (go bndrs) tys
+           return $ nlHsDataCon kindRepTyConAppDataCon
+                    `nlHsApp` nlHsVar rep_id
+                    `nlHsApp` mkList (mkTyConTy kindRepTyCon) tys'
+      | otherwise
+      = pprPanic "mkTyConKindRepBinds(TyConApp)"
+                 (ppr tc $$ ppr tycon_kind)
+    go _ (ForAllTy (TvBndr var _) ty)
+      -- = let bndrs' = extendVarEnv (mapVarEnv (+1) bndrs) var 0 in go bndrs' ty
+      = pprPanic "mkTyConKindRepBinds(ForAllTy)" (ppr var $$ ppr ty)
+    go bndrs (FunTy t1 t2)
+      = do t1' <- go bndrs t1
+           t2' <- go bndrs t2
+           return $ nlHsDataCon kindRepFunDataCon
+                    `nlHsApp` t1' `nlHsApp` t2'
+    go _ (LitTy (NumTyLit n))
+      = return $ nlHsDataCon kindRepTypeLitSDataCon
+                 `nlHsApp` nlHsDataCon typeLitNatDataCon
+                 `nlHsApp` nlHsLit (mkHsStringPrimLit $ mkFastString $ show n)
+    go _ (LitTy (StrTyLit s))
+      = return $ nlHsDataCon kindRepTypeLitSDataCon
+                 `nlHsApp` nlHsDataCon typeLitSymbolDataCon
+                 `nlHsApp` nlHsLit (mkHsStringPrimLit $ mkFastString $ show s)
+    go _ (CastTy ty co)
+      = pprPanic "mkTyConKindRepBinds.go(cast)" (ppr ty $$ ppr co)
+    go _ (CoercionTy co)
+      = pprPanic "mkTyConKindRepBinds.go(coercion)" (ppr co)
+
+    mkList :: Type -> [LHsExpr Id] -> LHsExpr Id
+    mkList ty = foldr consApp (nilExpr ty)
+      where
+        cons = consExpr ty
+        consApp :: LHsExpr Id -> LHsExpr Id -> LHsExpr Id
+        consApp x xs = cons `nlHsApp` x `nlHsApp` xs
+
+    nilExpr :: Type -> LHsExpr Id
+    nilExpr ty = mkLHsWrap (mkWpTyApps [ty]) (nlHsDataCon nilDataCon)
+
+    consExpr :: Type -> LHsExpr Id
+    consExpr ty = mkLHsWrap (mkWpTyApps [ty]) (nlHsDataCon consDataCon)
diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index b67eec0874..5fd17f9ee2 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -8,6 +8,7 @@ module Kind (
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind,
         isConstraintKind,
+        isTYPEApp,
         returnsTyCon, returnsConstraintKind,
         isConstraintKindCon,
         okArrowArgKind, okArrowResultKind,
@@ -19,7 +20,9 @@ module Kind (
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} Type       ( typeKind, coreViewOneStarKind )
+import {-# SOURCE #-} Type    ( typeKind, coreViewOneStarKind
+                              , splitTyConApp_maybe )
+import {-# SOURCE #-} DataCon ( DataCon )
 
 import TyCoRep
 import TyCon
@@ -68,6 +71,15 @@ isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
 isConstraintKind _               = False
 
+isTYPEApp :: Kind -> Maybe DataCon
+isTYPEApp (TyConApp tc args)
+  | tc `hasKey` tYPETyConKey
+  , [arg] <- args
+  , Just (tc, []) <- splitTyConApp_maybe arg
+  , Just dc <- isPromotedDataCon_maybe tc
+  = Just dc
+isTYPEApp _ = Nothing
+
 -- | Does the given type "end" in the given tycon? For example @k -> [a] -> *@
 -- ends in @*@ and @Maybe a -> [a]@ ends in @[]@.
 returnsTyCon :: Unique -> Type -> Bool
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 1b80d20ad4..71400099a6 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -898,6 +898,7 @@ data AlgTyConFlav
     -- | An unboxed type constructor. Note that this carries no TyConRepName
     -- as it is not representable.
   | UnboxedAlgTyCon
+       TyConRepName
 
   -- | Type constructors representing a class dictionary.
   -- See Note [ATyCon for classes] in TyCoRep
@@ -951,7 +952,7 @@ instance Outputable AlgTyConFlav where
 -- name, if any
 okParent :: Name -> AlgTyConFlav -> Bool
 okParent _       (VanillaAlgTyCon {})            = True
-okParent _       (UnboxedAlgTyCon)               = True
+okParent _       (UnboxedAlgTyCon {})            = True
 okParent tc_name (ClassTyCon cls _)              = tc_name == tyConName (classTyCon cls)
 okParent _       (DataFamInstTyCon _ fam_tc tys) = tyConArity fam_tc == length tys
 
@@ -1169,6 +1170,7 @@ tyConRepName_maybe (PrimTyCon  { primRepName = mb_rep_nm })
 tyConRepName_maybe (AlgTyCon { algTcParent = parent })
   | VanillaAlgTyCon rep_nm <- parent = Just rep_nm
   | ClassTyCon _ rep_nm    <- parent = Just rep_nm
+  | UnboxedAlgTyCon rep_nm    <- parent = Just rep_nm
 tyConRepName_maybe (FamilyTyCon { famTcFlav = DataFamilyTyCon rep_nm })
   = Just rep_nm
 tyConRepName_maybe (PromotedDataCon { tcRepName = rep_nm })
@@ -2057,7 +2059,7 @@ isTcTyCon _            = False
 -- Precondition: The fully-applied TyCon has kind (TYPE blah)
 isTcLevPoly :: TyCon -> Bool
 isTcLevPoly FunTyCon{}           = False
-isTcLevPoly (AlgTyCon { algTcParent = UnboxedAlgTyCon }) = True
+isTcLevPoly (AlgTyCon { algTcParent = UnboxedAlgTyCon _ }) = True
 isTcLevPoly AlgTyCon{}           = False
 isTcLevPoly SynonymTyCon{}       = True
 isTcLevPoly FamilyTyCon{}        = True
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index a50b76b2a3..460eb5e5e4 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1055,13 +1055,13 @@ splitTyConApp ty = case splitTyConApp_maybe ty of
 
 -- | Attempts to tease a type apart into a type constructor and the application
 -- of a number of arguments to that constructor
-splitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
 splitTyConApp_maybe ty                           = repSplitTyConApp_maybe ty
 
 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
 -- assumes the synonyms have already been dealt with.
-repSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 repSplitTyConApp_maybe (FunTy arg res)
   | Just rep1 <- getRuntimeRep_maybe arg
diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot
index 9436d195cc..560c251f1b 100644
--- a/compiler/types/Type.hs-boot
+++ b/compiler/types/Type.hs-boot
@@ -1,7 +1,10 @@
+{-# LANGUAGE FlexibleContexts #-}
+
 module Type where
 import TyCon
 import Var ( TyVar )
 import {-# SOURCE #-} TyCoRep( Type, Kind )
+import Util
 
 isPredTy     :: Type -> Bool
 isCoercionTy :: Type -> Bool
@@ -19,3 +22,5 @@ partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
 coreView :: Type -> Maybe Type
 
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
+
+splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
diff --git a/compiler/utils/Binary.hs b/compiler/utils/Binary.hs
index ffd1eb25fa..b10ab1d5f2 100644
--- a/compiler/utils/Binary.hs
+++ b/compiler/utils/Binary.hs
@@ -1,5 +1,8 @@
 {-# LANGUAGE CPP, MagicHash, UnboxedTuples #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
 
 {-# OPTIONS_GHC -O -funbox-strict-fields #-}
 -- We always optimise this, otherwise performance of a non-optimised
@@ -73,7 +76,14 @@ import qualified Data.ByteString.Unsafe   as BS
 import Data.IORef
 import Data.Char                ( ord, chr )
 import Data.Time
+#if MIN_VERSION_base(4,10,0)
+import Type.Reflection
+import Type.Reflection.Unsafe
+import Data.Kind (Type)
+import GHC.Exts (RuntimeRep(..), VecCount(..), VecElem(..))
+#else
 import Data.Typeable
+#endif
 import Control.Monad            ( when )
 import System.IO as IO
 import System.IO.Unsafe         ( unsafeInterleaveIO )
@@ -597,17 +607,175 @@ instance Binary (Bin a) where
 -- -----------------------------------------------------------------------------
 -- Instances for Data.Typeable stuff
 
+#if MIN_VERSION_base(4,10,0)
 instance Binary TyCon where
     put_ bh tc = do
         put_ bh (tyConPackage tc)
         put_ bh (tyConModule tc)
         put_ bh (tyConName tc)
+        put_ bh (tyConKindArgs tc)
+        put_ bh (tyConKindRep tc)
+    get bh =
+        mkTyCon <$> get bh <*> get bh <*> get bh <*> get bh <*> get bh
+#else
+instance Binary TyCon where
+    put_ bh tc = do
+        put_ bh (tyConPackage tc)
+        put_ bh (tyConModule tc)
+        put_ bh (tyConName tc)
+    get bh =
+        mkTyCon3 <$> get bh <*> get bh <*> get bh
+#endif
+
+#if MIN_VERSION_base(4,10,0)
+instance Binary VecCount where
+    put_ bh = putByte bh . fromIntegral . fromEnum
+    get bh = toEnum . fromIntegral <$> getByte bh
+
+instance Binary VecElem where
+    put_ bh = putByte bh . fromIntegral . fromEnum
+    get bh = toEnum . fromIntegral <$> getByte bh
+
+instance Binary RuntimeRep where
+    put_ bh (VecRep a b)    = putByte bh 0 >> put_ bh a >> put_ bh b
+    put_ bh (TupleRep reps) = putByte bh 1 >> put_ bh reps
+    put_ bh (SumRep reps)   = putByte bh 2 >> put_ bh reps
+    put_ bh LiftedRep       = putByte bh 3
+    put_ bh UnliftedRep     = putByte bh 4
+    put_ bh IntRep          = putByte bh 5
+    put_ bh WordRep         = putByte bh 6
+    put_ bh Int64Rep        = putByte bh 7
+    put_ bh Word64Rep       = putByte bh 8
+    put_ bh AddrRep         = putByte bh 9
+    put_ bh FloatRep        = putByte bh 10
+    put_ bh DoubleRep       = putByte bh 11
+
     get bh = do
-        p <- get bh
-        m <- get bh
-        n <- get bh
-        return (mkTyCon3 p m n)
+        tag <- getByte bh
+        case tag of
+          0  -> VecRep <$> get bh <*> get bh
+          1  -> TupleRep <$> get bh
+          2  -> SumRep <$> get bh
+          3  -> pure LiftedRep
+          4  -> pure UnliftedRep
+          5  -> pure IntRep
+          6  -> pure WordRep
+          7  -> pure Int64Rep
+          8  -> pure Word64Rep
+          9  -> pure AddrRep
+          10 -> pure FloatRep
+          11 -> pure DoubleRep
+          _  -> fail "Binary.putRuntimeRep: invalid tag"
+
+instance Binary KindRep where
+    put_ bh (KindRepTyConApp tc k) = putByte bh 0 >> put_ bh tc >> put_ bh k
+    put_ bh (KindRepVar bndr) = putByte bh 1 >> put_ bh bndr
+    put_ bh (KindRepApp a b) = putByte bh 2 >> put_ bh a >> put_ bh b
+    put_ bh (KindRepFun a b) = putByte bh 3 >> put_ bh a >> put_ bh b
+    put_ bh (KindRepTYPE r) = putByte bh 4 >> put_ bh r
+    put_ bh (KindRepTypeLit sort r) = putByte bh 5 >> put_ bh sort >> put_ bh r
+    put_ _  _ = fail "Binary.putKindRep: impossible"
 
+    get bh = do
+        tag <- getByte bh
+        case tag of
+          0 -> KindRepTyConApp <$> get bh <*> get bh
+          1 -> KindRepVar <$> get bh
+          2 -> KindRepApp <$> get bh <*> get bh
+          3 -> KindRepFun <$> get bh <*> get bh
+          4 -> KindRepTYPE <$> get bh
+          5 -> KindRepTypeLit <$> get bh <*> get bh
+          _ -> fail "Binary.putKindRep: invalid tag"
+
+instance Binary TypeLitSort where
+    put_ bh TypeLitSymbol = putByte bh 0
+    put_ bh TypeLitNat = putByte bh 1
+    get bh = do
+        tag <- getByte bh
+        case tag of
+          0 -> pure TypeLitSymbol
+          1 -> pure TypeLitNat
+          _ -> fail "Binary.putTypeLitSort: invalid tag"
+
+putTypeRep :: BinHandle -> TypeRep a -> IO ()
+-- Special handling for TYPE, (->), and RuntimeRep due to recursive kind
+-- relations.
+-- See Note [Mutually recursive representations of primitive types]
+putTypeRep bh rep
+  | Just HRefl <- rep `eqTypeRep` (typeRep :: TypeRep Type)
+  = put_ bh (0 :: Word8)
+putTypeRep bh (Con' con ks) = do
+    put_ bh (1 :: Word8)
+    put_ bh con
+    put_ bh ks
+putTypeRep bh (App f x) = do
+    put_ bh (2 :: Word8)
+    putTypeRep bh f
+    putTypeRep bh x
+putTypeRep bh (Fun arg res) = do
+    put_ bh (3 :: Word8)
+    putTypeRep bh arg
+    putTypeRep bh res
+putTypeRep _ _ = fail "Binary.putTypeRep: Impossible"
+
+getSomeTypeRep :: BinHandle -> IO SomeTypeRep
+getSomeTypeRep bh = do
+    tag <- get bh :: IO Word8
+    case tag of
+        0 -> return $ SomeTypeRep (typeRep :: TypeRep Type)
+        1 -> do con <- get bh :: IO TyCon
+                ks <- get bh :: IO [SomeTypeRep]
+                return $ SomeTypeRep $ mkTrCon con ks
+
+        2 -> do SomeTypeRep f <- getSomeTypeRep bh
+                SomeTypeRep x <- getSomeTypeRep bh
+                case typeRepKind f of
+                  Fun arg res ->
+                      case arg `eqTypeRep` typeRepKind x of
+                        Just HRefl ->
+                            case typeRepKind res `eqTypeRep` (typeRep :: TypeRep Type) of
+                              Just HRefl -> return $ SomeTypeRep $ mkTrApp f x
+                              _ -> failure "Kind mismatch in type application" []
+                        _ -> failure "Kind mismatch in type application"
+                             [ "    Found argument of kind: " ++ show (typeRepKind x)
+                             , "    Where the constructor:  " ++ show f
+                             , "    Expects kind:           " ++ show arg
+                             ]
+                  _ -> failure "Applied non-arrow"
+                       [ "    Applied type: " ++ show f
+                       , "    To argument:  " ++ show x
+                       ]
+        3 -> do SomeTypeRep arg <- getSomeTypeRep bh
+                SomeTypeRep res <- getSomeTypeRep bh
+                case typeRepKind arg `eqTypeRep` (typeRep :: TypeRep Type) of
+                  Just HRefl ->
+                      case typeRepKind res `eqTypeRep` (typeRep :: TypeRep Type) of
+                        Just HRefl -> return $ SomeTypeRep $ Fun arg res
+                        Nothing -> failure "Kind mismatch" []
+                  _ -> failure "Kind mismatch" []
+        _ -> failure "Invalid SomeTypeRep" []
+  where
+    failure description info =
+        fail $ unlines $ [ "Binary.getSomeTypeRep: "++description ]
+                      ++ map ("    "++) info
+
+instance Typeable a => Binary (TypeRep (a :: k)) where
+    put_ = putTypeRep
+    get bh = do
+        SomeTypeRep rep <- getSomeTypeRep bh
+        case rep `eqTypeRep` expected of
+            Just HRefl -> pure rep
+            Nothing    -> fail $ unlines
+                               [ "Binary: Type mismatch"
+                               , "    Deserialized type: " ++ show rep
+                               , "    Expected type:     " ++ show expected
+                               ]
+     where expected = typeRep :: TypeRep a
+
+instance Binary SomeTypeRep where
+    put_ bh (SomeTypeRep rep) = putTypeRep bh rep
+    get = getSomeTypeRep
+#else
 instance Binary TypeRep where
     put_ bh type_rep = do
         let (ty_con, child_type_reps) = splitTyConApp type_rep
@@ -617,6 +785,7 @@ instance Binary TypeRep where
         ty_con <- get bh
         child_type_reps <- get bh
         return (mkTyConApp ty_con child_type_reps)
+#endif
 
 -- -----------------------------------------------------------------------------
 -- Lazy reading/writing
diff --git a/compiler/utils/Fingerprint.hsc b/compiler/utils/Fingerprint.hsc
index f797654e0c..d4cee0e10b 100644
--- a/compiler/utils/Fingerprint.hsc
+++ b/compiler/utils/Fingerprint.hsc
@@ -15,6 +15,7 @@ module Fingerprint (
         fingerprintByteString,
         -- * Re-exported from GHC.Fingerprint
         Fingerprint(..), fingerprint0,
+        fingerprintFingerprints,
         fingerprintData,
         fingerprintString,
         getFileHash