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.

20 files changed, 1033 insertions, 386 deletions

diff --git a/libraries/base/Data/Dynamic.hs b/libraries/base/Data/Dynamic.hs
index 218bdc1f1e..5a4f3f9a08 100644
--- a/libraries/base/Data/Dynamic.hs
+++ b/libraries/base/Data/Dynamic.hs
@@ -1,51 +1,55 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Dynamic
 -- Copyright   :  (c) The University of Glasgow 2001
 -- License     :  BSD-style (see the file libraries/base/LICENSE)
--- 
+--
 -- Maintainer  :  libraries@haskell.org
 -- Stability   :  experimental
 -- Portability :  portable
 --
 -- The Dynamic interface provides basic support for dynamic types.
--- 
+--
 -- Operations for injecting values of arbitrary type into
 -- a dynamically typed value, Dynamic, are provided, together
 -- with operations for converting dynamic values into a concrete
 -- (monomorphic) type.
--- 
+--
 -----------------------------------------------------------------------------
 
 module Data.Dynamic
   (
 
-        -- * Module Data.Typeable re-exported for convenience
-        module Data.Typeable,
-
         -- * The @Dynamic@ type
-        Dynamic,        -- abstract, instance of: Show, Typeable
+        Dynamic(..),
 
         -- * Converting to and from @Dynamic@
         toDyn,
         fromDyn,
         fromDynamic,
-        
+
         -- * Applying functions of dynamic type
         dynApply,
         dynApp,
-        dynTypeRep
+        dynTypeRep,
+
+        -- * Convenience re-exports
+        Typeable
 
   ) where
 
 
-import Data.Typeable
+import Data.Type.Equality
+import Type.Reflection
 import Data.Maybe
-import Unsafe.Coerce
 
 import GHC.Base
 import GHC.Show
@@ -67,30 +71,30 @@ import GHC.Exception
   'Show'ing a value of type 'Dynamic' returns a pretty-printed representation
   of the object\'s type; useful for debugging.
 -}
-data Dynamic = Dynamic TypeRep Obj
+data Dynamic where
+    Dynamic :: forall a. TypeRep a -> a -> Dynamic
 
 -- | @since 2.01
 instance Show Dynamic where
    -- the instance just prints the type representation.
-   showsPrec _ (Dynamic t _) = 
-          showString "<<" . 
-          showsPrec 0 t   . 
+   showsPrec _ (Dynamic t _) =
+          showString "<<" .
+          showsPrec 0 t   .
           showString ">>"
 
 -- here so that it isn't an orphan:
 -- | @since 4.0.0.0
 instance Exception Dynamic
 
-type Obj = Any
  -- Use GHC's primitive 'Any' type to hold the dynamically typed value.
  --
  -- In GHC's new eval/apply execution model this type must not look
- -- like a data type.  If it did, GHC would use the constructor convention 
- -- when evaluating it, and this will go wrong if the object is really a 
+ -- like a data type.  If it did, GHC would use the constructor convention
+ -- when evaluating it, and this will go wrong if the object is really a
  -- function.  Using Any forces GHC to use
  -- a fallback convention for evaluating it that works for all types.
 
--- | Converts an arbitrary value into an object of type 'Dynamic'.  
+-- | Converts an arbitrary value into an object of type 'Dynamic'.
 --
 -- The type of the object must be an instance of 'Typeable', which
 -- ensures that only monomorphically-typed objects may be converted to
@@ -100,47 +104,48 @@ type Obj = Any
 -- >    toDyn (id :: Int -> Int)
 --
 toDyn :: Typeable a => a -> Dynamic
-toDyn v = Dynamic (typeOf v) (unsafeCoerce v)
+toDyn v = Dynamic typeRep v
 
 -- | Converts a 'Dynamic' object back into an ordinary Haskell value of
 -- the correct type.  See also 'fromDynamic'.
 fromDyn :: Typeable a
         => Dynamic      -- ^ the dynamically-typed object
-        -> a            -- ^ a default value 
+        -> a            -- ^ a default value
         -> a            -- ^ returns: the value of the first argument, if
                         -- it has the correct type, otherwise the value of
                         -- the second argument.
 fromDyn (Dynamic t v) def
-  | typeOf def == t = unsafeCoerce v
-  | otherwise       = def
+  | Just HRefl <- t `eqTypeRep` typeOf def = v
+  | otherwise                              = def
 
 -- | Converts a 'Dynamic' object back into an ordinary Haskell value of
 -- the correct type.  See also 'fromDyn'.
 fromDynamic
-        :: Typeable a
+        :: forall a. Typeable a
         => Dynamic      -- ^ the dynamically-typed object
         -> Maybe a      -- ^ returns: @'Just' a@, if the dynamically-typed
-                        -- object has the correct type (and @a@ is its value), 
+                        -- object has the correct type (and @a@ is its value),
                         -- or 'Nothing' otherwise.
-fromDynamic (Dynamic t v) =
-  case unsafeCoerce v of 
-    r | t == typeOf r -> Just r
-      | otherwise     -> Nothing
+fromDynamic (Dynamic t v)
+  | Just HRefl <- t `eqTypeRep` rep = Just v
+  | otherwise                       = Nothing
+  where rep = typeRep :: TypeRep a
 
 -- (f::(a->b)) `dynApply` (x::a) = (f a)::b
 dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
-dynApply (Dynamic t1 f) (Dynamic t2 x) =
-  case funResultTy t1 t2 of
-    Just t3 -> Just (Dynamic t3 ((unsafeCoerce f) x))
-    Nothing -> Nothing
+dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x)
+  | Just HRefl <- ta `eqTypeRep` ta'
+  , Just HRefl <- typeRep @Type `eqTypeRep` typeRepKind tr
+  = Just (Dynamic tr (f x))
+dynApply _ _
+  = Nothing
 
 dynApp :: Dynamic -> Dynamic -> Dynamic
-dynApp f x = case dynApply f x of 
+dynApp f x = case dynApply f x of
              Just r -> r
              Nothing -> errorWithoutStackTrace ("Type error in dynamic application.\n" ++
                                "Can't apply function " ++ show f ++
                                " to argument " ++ show x)
 
-dynTypeRep :: Dynamic -> TypeRep
-dynTypeRep (Dynamic tr _) = tr 
-
+dynTypeRep :: Dynamic -> SomeTypeRep
+dynTypeRep (Dynamic tr _) = SomeTypeRep tr
diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs
index 233020081b..73f8407cb0 100644
--- a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ -34,6 +34,7 @@
 module Data.Type.Equality (
   -- * The equality types
   (:~:)(..), type (~~),
+  (:~~:)(..),
 
   -- * Working with equality
   sym, trans, castWith, gcastWith, apply, inner, outer,
@@ -137,6 +138,13 @@ instance a ~ b => Enum (a :~: b) where
 -- | @since 4.7.0.0
 deriving instance a ~ b => Bounded (a :~: b)
 
+-- | Kind heterogeneous propositional equality. Like '(:~:)', @a :~~: b@ is
+-- inhabited by a terminating value if and only if @a@ is the same type as @b@.
+--
+-- @since 4.10.0.0
+data (a :: k1) :~~: (b :: k2) where
+   HRefl :: a :~~: a
+
 -- | This class contains types where you can learn the equality of two types
 -- from information contained in /terms/. Typically, only singleton types should
 -- inhabit this class.
diff --git a/libraries/base/Data/Typeable.hs b/libraries/base/Data/Typeable.hs
index d7225196de..8a6422ec14 100644
--- a/libraries/base/Data/Typeable.hs
+++ b/libraries/base/Data/Typeable.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeOperators #-}
 
 -----------------------------------------------------------------------------
@@ -10,7 +12,7 @@
 -- Module      :  Data.Typeable
 -- Copyright   :  (c) The University of Glasgow, CWI 2001--2004
 -- License     :  BSD-style (see the file libraries/base/LICENSE)
--- 
+--
 -- Maintainer  :  libraries@haskell.org
 -- Stability   :  experimental
 -- Portability :  portable
@@ -26,6 +28,11 @@
 --
 -- == Compatibility Notes
 --
+-- Since GHC 8.2, GHC has supported type-indexed type representations.
+-- "Data.Typeable" provides type representations which are qualified over this
+-- index, providing an interface very similar to the "Typeable" notion seen in
+-- previous releases. For the type-indexed interface, see "Data.Reflection".
+--
 -- Since GHC 7.8, 'Typeable' is poly-kinded. The changes required for this might
 -- break some old programs involving 'Typeable'. More details on this, including
 -- how to fix your code, can be found on the
@@ -34,85 +41,99 @@
 -----------------------------------------------------------------------------
 
 module Data.Typeable
-  (
-        -- * The Typeable class
-        Typeable,
-        typeRep,
-
-        -- * Propositional equality
-        (:~:)(Refl),
-
-        -- * For backwards compatibility
-        typeOf, typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7,
-        Typeable1, Typeable2, Typeable3, Typeable4, Typeable5, Typeable6,
-        Typeable7,
-
-        -- * Type-safe cast
-        cast,
-        eqT,
-        gcast,                  -- a generalisation of cast
-
-        -- * Generalized casts for higher-order kinds
-        gcast1,                 -- :: ... => c (t a) -> Maybe (c (t' a))
-        gcast2,                 -- :: ... => c (t a b) -> Maybe (c (t' a b))
-
-        -- * A canonical proxy type
-        Proxy (..),
-
-        -- * Type representations
-        TypeRep,        -- abstract, instance of: Eq, Show, Typeable
-        typeRepFingerprint,
-        rnfTypeRep,
-        showsTypeRep,
-
-        TyCon,          -- abstract, instance of: Eq, Show, Typeable
-                        -- For now don't export Module, to avoid name clashes
-        tyConFingerprint,
-        tyConPackage,
-        tyConModule,
-        tyConName,
-        rnfTyCon,
-
-        -- * Construction of type representations
-        -- mkTyCon,        -- :: String  -> TyCon
-        mkTyCon3,       -- :: String  -> String -> String -> TyCon
-        mkTyConApp,     -- :: TyCon   -> [TypeRep] -> TypeRep
-        mkAppTy,        -- :: TypeRep -> TypeRep   -> TypeRep
-        mkFunTy,        -- :: TypeRep -> TypeRep   -> TypeRep
-
-        -- * Observation of type representations
-        splitTyConApp,  -- :: TypeRep -> (TyCon, [TypeRep])
-        funResultTy,    -- :: TypeRep -> TypeRep   -> Maybe TypeRep
-        typeRepTyCon,   -- :: TypeRep -> TyCon
-        typeRepArgs,    -- :: TypeRep -> [TypeRep]
-  ) where
-
-import Data.Typeable.Internal
+    ( -- * The Typeable class
+      Typeable
+    , typeOf
+    , typeRep
+    , I.withTypeable
+
+      -- * Propositional equality
+    , (:~:)(Refl)
+    , (:~~:)(HRefl)
+
+      -- * Type-safe cast
+    , cast
+    , eqT
+    , gcast                -- a generalisation of cast
+
+      -- * Generalized casts for higher-order kinds
+    , gcast1               -- :: ... => c (t a) -> Maybe (c (t' a))
+    , gcast2               -- :: ... => c (t a b) -> Maybe (c (t' a b))
+
+      -- * A canonical proxy type
+    , Proxy (..)
+
+      -- * Type representations
+    , TypeRep
+    , typeRepTyCon
+    , rnfTypeRep
+    , showsTypeRep
+    , mkFunTy
+
+      -- * Observing type representations
+    , funResultTy
+    , I.typeRepFingerprint
+
+      -- * Type constructors
+    , I.TyCon          -- abstract, instance of: Eq, Show, Typeable
+                       -- For now don't export Module to avoid name clashes
+    , I.tyConPackage
+    , I.tyConModule
+    , I.tyConName
+    , I.rnfTyCon
+
+      -- * For backwards compatibility
+    , typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7
+    , Typeable1, Typeable2, Typeable3, Typeable4
+    , Typeable5, Typeable6, Typeable7
+    ) where
+
+import qualified Data.Typeable.Internal as I
+import Data.Typeable.Internal (Typeable)
 import Data.Type.Equality
 
-import Unsafe.Coerce
 import Data.Maybe
+import Data.Proxy
+import GHC.Show
 import GHC.Base
 
--------------------------------------------------------------
---
---              Type-safe cast
+-- | A quantified type representation.
+type TypeRep = I.SomeTypeRep
+
+-- | Observe a type representation for the type of a value.
+typeOf :: forall a. Typeable a => a -> TypeRep
+typeOf _ = I.typeRepX (Proxy :: Proxy a)
+
+-- | Takes a value of type @a@ and returns a concrete representation
+-- of that type.
 --
--------------------------------------------------------------
+-- @since 4.7.0.0
+typeRep :: forall proxy a. Typeable a => proxy a -> TypeRep
+typeRep = I.typeRepX
+
+-- | Show a type representation
+showsTypeRep :: I.SomeTypeRep -> ShowS
+showsTypeRep = shows
 
 -- | The type-safe cast operation
 cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
-cast x = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)
-           then Just $ unsafeCoerce x
-           else Nothing
+cast x
+  | Just HRefl <- ta `I.eqTypeRep` tb = Just x
+  | otherwise                         = Nothing
+  where
+    ta = I.typeRep :: I.TypeRep a
+    tb = I.typeRep :: I.TypeRep b
 
 -- | Extract a witness of equality of two types
 --
 -- @since 4.7.0.0
 eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
-eqT = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)
-      then Just $ unsafeCoerce Refl
-      else Nothing
+eqT
+  | Just HRefl <- ta `I.eqTypeRep` tb = Just Refl
+  | otherwise                         = Nothing
+  where
+    ta = I.typeRep :: I.TypeRep a
+    tb = I.typeRep :: I.TypeRep b
 
 -- | A flexible variation parameterised in a type constructor
 gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
@@ -120,11 +141,86 @@ gcast x = fmap (\Refl -> x) (eqT :: Maybe (a :~: b))
 
 -- | Cast over @k1 -> k2@
 gcast1 :: forall c t t' a. (Typeable t, Typeable t')
-       => c (t a) -> Maybe (c (t' a)) 
+       => c (t a) -> Maybe (c (t' a))
 gcast1 x = fmap (\Refl -> x) (eqT :: Maybe (t :~: t'))
 
 -- | Cast over @k1 -> k2 -> k3@
 gcast2 :: forall c t t' a b. (Typeable t, Typeable t')
-       => c (t a b) -> Maybe (c (t' a b)) 
+       => c (t a b) -> Maybe (c (t' a b))
 gcast2 x = fmap (\Refl -> x) (eqT :: Maybe (t :~: t'))
 
+-- | Observe the type constructor of a quantified type representation.
+typeRepTyCon :: TypeRep -> TyCon
+typeRepTyCon = I.typeRepXTyCon
+
+-- | Applies a type to a function type. Returns: @Just u@ if the first argument
+-- represents a function of type @t -> u@ and the second argument represents a
+-- function of type @t@. Otherwise, returns @Nothing@.
+funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep
+funResultTy (I.SomeTypeRep f) (I.SomeTypeRep x)
+  | Just HRefl <- (I.typeRep :: I.TypeRep Type) `I.eqTypeRep` I.typeRepKind f
+  , I.Fun arg res <- f
+  , Just HRefl <- arg `I.eqTypeRep` x
+  = Just (I.SomeTypeRep res)
+  | otherwise = Nothing
+
+-- | Build a function type.
+mkFunTy :: TypeRep -> TypeRep -> TypeRep
+mkFunTy (I.SomeTypeRep arg) (I.SomeTypeRep res)
+  | Just HRefl <- I.typeRepKind arg `I.eqTypeRep` liftedTy
+  , Just HRefl <- I.typeRepKind res `I.eqTypeRep` liftedTy
+  = I.SomeTypeRep (I.Fun arg res)
+  | otherwise
+  = error $ "mkFunTy: Attempted to construct function type from non-lifted "++
+            "type: arg="++show arg++", res="++show res
+  where liftedTy = I.typeRep :: I.TypeRep *
+  -- TODO: We should be able to support this but the kind of (->) must be
+  -- generalized
+
+-- | Force a 'TypeRep' to normal form.
+rnfTypeRep :: TypeRep -> ()
+rnfTypeRep = I.rnfSomeTypeRep
+
+
+-- Keeping backwards-compatibility
+typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep
+typeOf1 _ = I.typeRepX (Proxy :: Proxy t)
+
+typeOf2 :: forall t (a :: *) (b :: *). Typeable t => t a b -> TypeRep
+typeOf2 _ = I.typeRepX (Proxy :: Proxy t)
+
+typeOf3 :: forall t (a :: *) (b :: *) (c :: *). Typeable t
+        => t a b c -> TypeRep
+typeOf3 _ = I.typeRepX (Proxy :: Proxy t)
+
+typeOf4 :: forall t (a :: *) (b :: *) (c :: *) (d :: *). Typeable t
+        => t a b c d -> TypeRep
+typeOf4 _ = I.typeRepX (Proxy :: Proxy t)
+
+typeOf5 :: forall t (a :: *) (b :: *) (c :: *) (d :: *) (e :: *). Typeable t
+        => t a b c d e -> TypeRep
+typeOf5 _ = I.typeRepX (Proxy :: Proxy t)
+
+typeOf6 :: forall t (a :: *) (b :: *) (c :: *) (d :: *) (e :: *) (f :: *).
+                Typeable t => t a b c d e f -> TypeRep
+typeOf6 _ = I.typeRepX (Proxy :: Proxy t)
+
+typeOf7 :: forall t (a :: *) (b :: *) (c :: *) (d :: *) (e :: *) (f :: *)
+                (g :: *). Typeable t => t a b c d e f g -> TypeRep
+typeOf7 _ = I.typeRepX (Proxy :: Proxy t)
+
+type Typeable1 (a :: * -> *)                               = Typeable a
+type Typeable2 (a :: * -> * -> *)                          = Typeable a
+type Typeable3 (a :: * -> * -> * -> *)                     = Typeable a
+type Typeable4 (a :: * -> * -> * -> * -> *)                = Typeable a
+type Typeable5 (a :: * -> * -> * -> * -> * -> *)           = Typeable a
+type Typeable6 (a :: * -> * -> * -> * -> * -> * -> *)      = Typeable a
+type Typeable7 (a :: * -> * -> * -> * -> * -> * -> * -> *) = Typeable a
+
+{-# DEPRECATED Typeable1 "renamed to 'Typeable'" #-} -- deprecated in 7.8
+{-# DEPRECATED Typeable2 "renamed to 'Typeable'" #-} -- deprecated in 7.8
+{-# DEPRECATED Typeable3 "renamed to 'Typeable'" #-} -- deprecated in 7.8
+{-# DEPRECATED Typeable4 "renamed to 'Typeable'" #-} -- deprecated in 7.8
+{-# DEPRECATED Typeable5 "renamed to 'Typeable'" #-} -- deprecated in 7.8
+{-# DEPRECATED Typeable6 "renamed to 'Typeable'" #-} -- deprecated in 7.8
+{-# DEPRECATED Typeable7 "renamed to 'Typeable'" #-} -- deprecated in 7.8
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 7746bfbe6c..800dc2a66f 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -1,9 +1,16 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
@@ -25,12 +32,11 @@
 -----------------------------------------------------------------------------
 
 module Data.Typeable.Internal (
-    Proxy (..),
     Fingerprint(..),
 
     -- * Typeable class
-    typeOf, typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7,
-    Typeable1, Typeable2, Typeable3, Typeable4, Typeable5, Typeable6, Typeable7,
+    Typeable(..),
+    withTypeable,
 
     -- * Module
     Module,  -- Abstract
@@ -38,37 +44,45 @@ module Data.Typeable.Internal (
 
     -- * TyCon
     TyCon,   -- Abstract
-    tyConPackage, tyConModule, tyConName, tyConFingerprint,
-    mkTyCon3, mkTyCon3#,
+    tyConPackage, tyConModule, tyConName, tyConKindArgs, tyConKindRep,
+    KindRep(.., KindRepTypeLit), TypeLitSort(..),
     rnfTyCon,
 
     -- * TypeRep
-    TypeRep(..), KindRep,
+    TypeRep,
+    pattern App, pattern Con, pattern Con', pattern Fun,
     typeRep,
-    mkTyConApp,
-    mkPolyTyConApp,
-    mkAppTy,
+    typeOf,
     typeRepTyCon,
-    Typeable(..),
-    mkFunTy,
-    splitTyConApp,
-    splitPolyTyConApp,
-    funResultTy,
-    typeRepArgs,
     typeRepFingerprint,
     rnfTypeRep,
-    showsTypeRep,
-    typeRepKinds,
-    typeSymbolTypeRep, typeNatTypeRep
+    eqTypeRep,
+    typeRepKind,
+
+    -- * SomeTypeRep
+    SomeTypeRep(..),
+    typeRepX,
+    typeRepXTyCon,
+    typeRepXFingerprint,
+    rnfSomeTypeRep,
+
+    -- * Construction
+    -- | These are for internal use only
+    mkTrCon, mkTrApp, mkTrFun,
+    mkTyCon, mkTyCon#,
+    typeSymbolTypeRep, typeNatTypeRep,
   ) where
 
 import GHC.Base
-import GHC.Types (TYPE)
+import qualified GHC.Arr as A
+import GHC.Types ( TYPE )
+import Data.Type.Equality
+import GHC.List ( splitAt, foldl )
 import GHC.Word
 import GHC.Show
-import Data.Proxy
 import GHC.TypeLits ( KnownSymbol, symbolVal' )
 import GHC.TypeNats ( KnownNat, natVal' )
+import Unsafe.Coerce ( unsafeCoerce )
 
 import GHC.Fingerprint.Type
 import {-# SOURCE #-} GHC.Fingerprint
@@ -92,52 +106,27 @@ moduleName :: Module -> String
 moduleName (Module _ m) = trNameString m
 
 tyConPackage :: TyCon -> String
-tyConPackage (TyCon _ _ m _) = modulePackage m
+tyConPackage (TyCon _ _ m _ _ _) = modulePackage m
 
 tyConModule :: TyCon -> String
-tyConModule (TyCon _ _ m _) = moduleName m
+tyConModule (TyCon _ _ m _ _ _) = moduleName m
 
 tyConName :: TyCon -> String
-tyConName (TyCon _ _ _ n) = trNameString n
+tyConName (TyCon _ _ _ n _ _) = trNameString n
 
 trNameString :: TrName -> String
 trNameString (TrNameS s) = unpackCString# s
 trNameString (TrNameD s) = s
 
 tyConFingerprint :: TyCon -> Fingerprint
-tyConFingerprint (TyCon hi lo _ _)
+tyConFingerprint (TyCon hi lo _ _ _ _)
   = Fingerprint (W64# hi) (W64# lo)
 
-mkTyCon3# :: Addr#       -- ^ package name
-          -> Addr#       -- ^ module name
-          -> Addr#       -- ^ the name of the type constructor
-          -> TyCon       -- ^ A unique 'TyCon' object
-mkTyCon3# pkg modl name
-  | Fingerprint (W64# hi) (W64# lo) <- fingerprint
-  = TyCon hi lo (Module (TrNameS pkg) (TrNameS modl)) (TrNameS name)
-  where
-    fingerprint :: Fingerprint
-    fingerprint = fingerprintString (unpackCString# pkg
-                                    ++ (' ': unpackCString# modl)
-                                    ++ (' ' : unpackCString# name))
-
-mkTyCon3 :: String       -- ^ package name
-         -> String       -- ^ module name
-         -> String       -- ^ the name of the type constructor
-         -> TyCon        -- ^ A unique 'TyCon' object
--- Used when the strings are dynamically allocated,
--- eg from binary deserialisation
-mkTyCon3 pkg modl name
-  | Fingerprint (W64# hi) (W64# lo) <- fingerprint
-  = TyCon hi lo (Module (TrNameD pkg) (TrNameD modl)) (TrNameD name)
-  where
-    fingerprint :: Fingerprint
-    fingerprint = fingerprintString (pkg ++ (' ':modl) ++ (' ':name))
+tyConKindArgs :: TyCon -> Int
+tyConKindArgs (TyCon _ _ _ _ n _) = I# n
 
-isTupleTyCon :: TyCon -> Bool
-isTupleTyCon tc
-  | ('(':',':_) <- tyConName tc = True
-  | otherwise                   = False
+tyConKindRep :: TyCon -> KindRep
+tyConKindRep (TyCon _ _ _ _ _ k) = k
 
 -- | Helper to fully evaluate 'TyCon' for use as @NFData(rnf)@ implementation
 --
@@ -149,12 +138,28 @@ rnfTrName :: TrName -> ()
 rnfTrName (TrNameS _) = ()
 rnfTrName (TrNameD n) = rnfString n
 
-rnfTyCon :: TyCon -> ()
-rnfTyCon (TyCon _ _ m n) = rnfModule m `seq` rnfTrName n
+rnfKindRep :: KindRep -> ()
+rnfKindRep (KindRepTyConApp tc args) = rnfTyCon tc `seq` rnfList rnfKindRep args
+rnfKindRep (KindRepVar _)   = ()
+rnfKindRep (KindRepApp a b) = rnfKindRep a `seq` rnfKindRep b
+rnfKindRep (KindRepFun a b) = rnfKindRep a `seq` rnfKindRep b
+rnfKindRep (KindRepTYPE rr) = rnfRuntimeRep rr
+rnfKindRep (KindRepTypeLitS _ _) = ()
+rnfKindRep (KindRepTypeLitD _ t) = rnfString t
+
+rnfRuntimeRep :: RuntimeRep -> ()
+rnfRuntimeRep (VecRep !_ !_) = ()
+rnfRuntimeRep !_             = ()
+
+rnfList :: (a -> ()) -> [a] -> ()
+rnfList _     []     = ()
+rnfList force (x:xs) = force x `seq` rnfList force xs
 
 rnfString :: [Char] -> ()
-rnfString [] = ()
-rnfString (c:cs) = c `seq` rnfString cs
+rnfString = rnfList (`seq` ())
+
+rnfTyCon :: TyCon -> ()
+rnfTyCon (TyCon _ _ m n _ k) = rnfModule m `seq` rnfTrName n `seq` rnfKindRep k
 
 
 {- *********************************************************************
@@ -165,118 +170,279 @@ rnfString (c:cs) = c `seq` rnfString cs
 
 -- | A concrete representation of a (monomorphic) type.
 -- 'TypeRep' supports reasonably efficient equality.
-data TypeRep = TypeRep {-# UNPACK #-} !Fingerprint TyCon [KindRep] [TypeRep]
-     -- NB: For now I've made this lazy so that it's easy to
-     -- optimise code that constructs and deconstructs TypeReps
-     -- perf/should_run/T9203 is a good example
-     -- Also note that mkAppTy does discards the fingerprint,
-     -- so it's a waste to compute it
-
-type KindRep = TypeRep
+data TypeRep (a :: k) where
+    TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep]
+            -> TypeRep (a :: k)
+    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
+               {-# UNPACK #-} !Fingerprint
+            -> TypeRep (a :: k1 -> k2)
+            -> TypeRep (b :: k1)
+            -> TypeRep (a b)
+    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                      (a :: TYPE r1) (b :: TYPE r2).
+               {-# UNPACK #-} !Fingerprint
+            -> TypeRep a
+            -> TypeRep b
+            -> TypeRep (a -> b)
+
+on :: (a -> a -> r) -> (b -> a) -> (b -> b -> r)
+on f g = \ x y -> g x `f` g y
 
 -- Compare keys for equality
+
 -- | @since 2.01
-instance Eq TypeRep where
-  TypeRep x _ _ _ == TypeRep y _ _ _ = x == y
+instance Eq (TypeRep a) where
+  _ == _  = True
+  {-# INLINABLE (==) #-}
+
+instance TestEquality TypeRep where
+  a `testEquality` b
+    | Just HRefl <- eqTypeRep a b
+    = Just Refl
+    | otherwise
+    = Nothing
+  {-# INLINEABLE testEquality #-}
 
 -- | @since 4.4.0.0
-instance Ord TypeRep where
-  TypeRep x _ _ _ <= TypeRep y _ _ _ = x <= y
+instance Ord (TypeRep a) where
+  compare = compare `on` typeRepFingerprint
+
+-- | A non-indexed type representation.
+data SomeTypeRep where
+    SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep
+
+instance Eq SomeTypeRep where
+  SomeTypeRep a == SomeTypeRep b =
+      case a `eqTypeRep` b of
+          Just _  -> True
+          Nothing -> False
+
+instance Ord SomeTypeRep where
+  SomeTypeRep a `compare` SomeTypeRep b =
+    typeRepFingerprint a `compare` typeRepFingerprint b
+
+pattern Fun :: 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 Fun arg res <- TrFun _ arg res
+  where Fun arg res = mkTrFun arg res
 
 -- | Observe the 'Fingerprint' of a type representation
 --
 -- @since 4.8.0.0
-typeRepFingerprint :: TypeRep -> Fingerprint
-typeRepFingerprint (TypeRep fpr _ _ _) = fpr
-
--- | Applies a kind-polymorphic type constructor to a sequence of kinds and
--- types
-mkPolyTyConApp :: TyCon -> [KindRep] -> [TypeRep] -> TypeRep
-{-# INLINE mkPolyTyConApp #-}
-mkPolyTyConApp tc kinds types
-  = TypeRep (fingerprintFingerprints sub_fps) tc kinds types
+typeRepFingerprint :: TypeRep a -> Fingerprint
+typeRepFingerprint (TrTyCon fpr _ _) = fpr
+typeRepFingerprint (TrApp fpr _ _) = fpr
+typeRepFingerprint (TrFun fpr _ _) = fpr
+
+-- | Construct a representation for a type constructor
+-- applied at a monomorphic kind.
+--
+-- Note that this is unsafe as it allows you to construct
+-- ill-kinded types.
+mkTrCon :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
+mkTrCon tc kind_vars = TrTyCon fpr tc kind_vars
   where
-    !kt_fps = typeRepFingerprints kinds types
-    sub_fps = tyConFingerprint tc : kt_fps
+    fpr_tc  = tyConFingerprint tc
+    fpr_kvs = map typeRepXFingerprint kind_vars
+    fpr     = fingerprintFingerprints (fpr_tc:fpr_kvs)
 
-typeRepFingerprints :: [KindRep] -> [TypeRep] -> [Fingerprint]
--- Builds no thunks
-typeRepFingerprints kinds types
-  = go1 [] kinds
+-- | Construct a representation for a type application.
+--
+-- Note that this is known-key to the compiler, which uses it in desugar
+-- 'Typeable' evidence.
+mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
+           TypeRep (a :: k1 -> k2)
+        -> TypeRep (b :: k1)
+        -> TypeRep (a b)
+mkTrApp a b = TrApp fpr a b
   where
-    go1 acc []     = go2 acc types
-    go1 acc (k:ks) = let !fp = typeRepFingerprint k
-                     in go1 (fp:acc) ks
-    go2 acc []     = acc
-    go2 acc (t:ts) = let !fp = typeRepFingerprint t
-                     in go2 (fp:acc) ts
-
--- | Applies a kind-monomorphic type constructor to a sequence of types
-mkTyConApp  :: TyCon -> [TypeRep] -> TypeRep
-mkTyConApp tc = mkPolyTyConApp tc []
-
--- | A special case of 'mkTyConApp', which applies the function
--- type constructor to a pair of types.
-mkFunTy  :: TypeRep -> TypeRep -> TypeRep
-mkFunTy f a = mkTyConApp tcFun [f,a]
-
--- | Splits a type constructor application.
--- Note that if the type constructor is polymorphic, this will
--- not return the kinds that were used.
--- See 'splitPolyTyConApp' if you need all parts.
-splitTyConApp :: TypeRep -> (TyCon,[TypeRep])
-splitTyConApp (TypeRep _ tc _ trs) = (tc,trs)
-
--- | Split a type constructor application
-splitPolyTyConApp :: TypeRep -> (TyCon,[KindRep],[TypeRep])
-splitPolyTyConApp (TypeRep _ tc ks trs) = (tc,ks,trs)
-
--- | Applies a type to a function type.  Returns: @'Just' u@ if the
--- first argument represents a function of type @t -> u@ and the
--- second argument represents a function of type @t@.  Otherwise,
--- returns 'Nothing'.
-funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep
-funResultTy trFun trArg
-  = case splitTyConApp trFun of
-      (tc, [t1,t2]) | tc == tcFun && t1 == trArg -> Just t2
-      _ -> Nothing
-
-tyConOf :: Typeable a => Proxy a -> TyCon
-tyConOf = typeRepTyCon . typeRep
-
-tcFun :: TyCon
-tcFun = tyConOf (Proxy :: Proxy (Int -> Int))
-
--- | Adds a TypeRep argument to a TypeRep.
-mkAppTy :: TypeRep -> TypeRep -> TypeRep
-{-# INLINE mkAppTy #-}
-mkAppTy (TypeRep _ tc ks trs) arg_tr = mkPolyTyConApp tc ks (trs ++ [arg_tr])
-   -- Notice that we call mkTyConApp to construct the fingerprint from tc and
-   -- the arg fingerprints.  Simply combining the current fingerprint with
-   -- the new one won't give the same answer, but of course we want to
-   -- ensure that a TypeRep of the same shape has the same fingerprint!
-   -- See Trac #5962
+    fpr_a = typeRepFingerprint a
+    fpr_b = typeRepFingerprint b
+    fpr   = fingerprintFingerprints [fpr_a, fpr_b]
+
+-- | Pattern match on a type application
+pattern App :: forall k2 (t :: k2). ()
+            => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
+            => TypeRep a -> TypeRep b -> TypeRep t
+pattern App f x <- TrApp _ f x
+  where App f x = mkTrApp f x
+
+-- | Use a 'TypeRep' as 'Typeable' evidence.
+withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
+withTypeable rep k = unsafeCoerce k' rep
+  where k' :: Gift a r
+        k' = Gift k
+
+-- | A helper to satisfy the type checker in 'withTypeable'.
+newtype Gift a r = Gift (Typeable a => r)
+
+-- | Pattern match on a type constructor
+pattern Con :: forall k (a :: k). TyCon -> TypeRep a
+pattern Con con <- TrTyCon _ con _
+
+-- | Pattern match on a type constructor including its instantiated kind
+-- variables.
+pattern Con' :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
+pattern Con' con ks <- TrTyCon _ con ks
 
 ----------------- Observation ---------------------
 
+-- | Observe the type constructor of a quantified type representation.
+typeRepXTyCon :: SomeTypeRep -> TyCon
+typeRepXTyCon (SomeTypeRep t) = typeRepTyCon t
+
 -- | Observe the type constructor of a type representation
-typeRepTyCon :: TypeRep -> TyCon
-typeRepTyCon (TypeRep _ tc _ _) = tc
+typeRepTyCon :: TypeRep a -> TyCon
+typeRepTyCon (TrTyCon _ tc _) = tc
+typeRepTyCon (TrApp _ a _)    = typeRepTyCon a
+typeRepTyCon (TrFun _ _ _)    = error "typeRepTyCon: FunTy" -- TODO
 
--- | Observe the argument types of a type representation
-typeRepArgs :: TypeRep -> [TypeRep]
-typeRepArgs (TypeRep _ _ _ tys) = tys
+-- | Type equality
+--
+-- @since TODO
+eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
+             TypeRep a -> TypeRep b -> Maybe (a :~~: b)
+eqTypeRep a b
+  | typeRepFingerprint a == typeRepFingerprint b = Just (unsafeCoerce# HRefl)
+  | otherwise                                    = Nothing
 
--- | Observe the argument kinds of a type representation
-typeRepKinds :: TypeRep -> [KindRep]
-typeRepKinds (TypeRep _ _ ks _) = ks
 
+-------------------------------------------------------------
+--
+--      Computing kinds
+--
+-------------------------------------------------------------
 
-{- *********************************************************************
-*                                                                      *
-                The Typeable class
-*                                                                      *
-********************************************************************* -}
+-- | Observe the kind of a type.
+typeRepKind :: TypeRep (a :: k) -> TypeRep k
+typeRepKind (TrTyCon _ tc args)
+  = unsafeCoerceRep $ tyConKind tc args
+typeRepKind (TrApp _ f _)
+  | Fun _ res <- typeRepKind f
+  = res
+  | otherwise
+  = error ("Ill-kinded type application: " ++ show (typeRepKind f))
+typeRepKind (TrFun _ _ _) = typeRep @Type
+
+tyConKind :: TyCon -> [SomeTypeRep] -> SomeTypeRep
+tyConKind (TyCon _ _ _ _ nKindVars# kindRep) kindVars =
+    let kindVarsArr :: A.Array KindBndr SomeTypeRep
+        kindVarsArr = A.listArray (0, I# (nKindVars# -# 1#)) kindVars
+    in instantiateKindRep kindVarsArr kindRep
+
+instantiateKindRep :: A.Array KindBndr SomeTypeRep -> KindRep -> SomeTypeRep
+instantiateKindRep vars = go
+  where
+    go :: KindRep -> SomeTypeRep
+    go (KindRepTyConApp tc args)
+      = let n_kind_args = tyConKindArgs tc
+            (kind_args, ty_args) = splitAt n_kind_args args
+            -- First instantiate tycon kind arguments
+            tycon_app = SomeTypeRep $ mkTrCon tc (map go kind_args)
+            -- Then apply remaining type arguments
+            applyTy :: SomeTypeRep -> KindRep -> SomeTypeRep
+            applyTy (SomeTypeRep acc) ty
+              | SomeTypeRep ty' <- go ty
+              = SomeTypeRep $ mkTrApp (unsafeCoerce acc) (unsafeCoerce ty')
+        in foldl applyTy tycon_app ty_args
+    go (KindRepVar var)
+      = vars A.! var
+    go (KindRepApp f a)
+      = SomeTypeRep $ App (unsafeCoerceRep $ go f) (unsafeCoerceRep $ go a)
+    go (KindRepFun a b)
+      = SomeTypeRep $ Fun (unsafeCoerceRep $ go a) (unsafeCoerceRep $ go b)
+    go (KindRepTYPE r) = unkindedTypeRep $ tYPE `kApp` runtimeRepTypeRep r
+    go (KindRepTypeLitS sort s)
+      = mkTypeLitFromString sort (unpackCString# s)
+    go (KindRepTypeLitD sort s)
+      = mkTypeLitFromString sort s
+
+    tYPE = kindedTypeRep @(RuntimeRep -> Type) @TYPE
+
+unsafeCoerceRep :: SomeTypeRep -> TypeRep a
+unsafeCoerceRep (SomeTypeRep r) = unsafeCoerce r
+
+unkindedTypeRep :: SomeKindedTypeRep k -> SomeTypeRep
+unkindedTypeRep (SomeKindedTypeRep x) = SomeTypeRep x
+
+data SomeKindedTypeRep k where
+    SomeKindedTypeRep :: forall (a :: k). TypeRep a
+                      -> SomeKindedTypeRep k
+
+kApp :: SomeKindedTypeRep (k -> k')
+     -> SomeKindedTypeRep k
+     -> SomeKindedTypeRep k'
+kApp (SomeKindedTypeRep f) (SomeKindedTypeRep a) =
+    SomeKindedTypeRep (App f a)
+
+kindedTypeRep :: forall (a :: k). Typeable a => SomeKindedTypeRep k
+kindedTypeRep = SomeKindedTypeRep (typeRep @a)
+
+buildList :: forall k. Typeable k
+          => [SomeKindedTypeRep k]
+          -> SomeKindedTypeRep [k]
+buildList = foldr cons nil
+  where
+    nil = kindedTypeRep @[k] @'[]
+    cons x rest = SomeKindedTypeRep (typeRep @'(:)) `kApp` x `kApp` rest
+
+runtimeRepTypeRep :: RuntimeRep -> SomeKindedTypeRep RuntimeRep
+runtimeRepTypeRep r =
+    case r of
+      LiftedRep   -> rep @'LiftedRep
+      UnliftedRep -> rep @'UnliftedRep
+      VecRep c e  -> kindedTypeRep @_ @'VecRep
+                     `kApp` vecCountTypeRep c
+                     `kApp` vecElemTypeRep e
+      TupleRep rs -> kindedTypeRep @_ @'TupleRep
+                     `kApp` buildList (map runtimeRepTypeRep rs)
+      SumRep rs   -> kindedTypeRep @_ @'SumRep
+                     `kApp` buildList (map runtimeRepTypeRep rs)
+      IntRep      -> rep @'IntRep
+      WordRep     -> rep @'WordRep
+      Int64Rep    -> rep @'Int64Rep
+      Word64Rep   -> rep @'Word64Rep
+      AddrRep     -> rep @'AddrRep
+      FloatRep    -> rep @'FloatRep
+      DoubleRep   -> rep @'DoubleRep
+  where
+    rep :: forall (a :: RuntimeRep). Typeable a => SomeKindedTypeRep RuntimeRep
+    rep = kindedTypeRep @RuntimeRep @a
+
+vecCountTypeRep :: VecCount -> SomeKindedTypeRep VecCount
+vecCountTypeRep c =
+    case c of
+      Vec2  -> rep @'Vec2
+      Vec4  -> rep @'Vec4
+      Vec8  -> rep @'Vec8
+      Vec16 -> rep @'Vec16
+      Vec32 -> rep @'Vec32
+      Vec64 -> rep @'Vec64
+  where
+    rep :: forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
+    rep = kindedTypeRep @VecCount @a
+
+vecElemTypeRep :: VecElem -> SomeKindedTypeRep VecElem
+vecElemTypeRep e =
+    case e of
+      Int8ElemRep     -> rep @'Int8ElemRep
+      Int16ElemRep    -> rep @'Int16ElemRep
+      Int32ElemRep    -> rep @'Int32ElemRep
+      Int64ElemRep    -> rep @'Int64ElemRep
+      Word8ElemRep    -> rep @'Word8ElemRep
+      Word16ElemRep   -> rep @'Word16ElemRep
+      Word32ElemRep   -> rep @'Word32ElemRep
+      Word64ElemRep   -> rep @'Word64ElemRep
+      FloatElemRep    -> rep @'FloatElemRep
+      DoubleElemRep   -> rep @'DoubleElemRep
+  where
+    rep :: forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
+    rep = kindedTypeRep @VecElem @a
 
 -------------------------------------------------------------
 --
@@ -286,115 +452,103 @@ typeRepKinds (TypeRep _ _ ks _) = ks
 
 -- | The class 'Typeable' allows a concrete representation of a type to
 -- be calculated.
-class Typeable a where
-  typeRep# :: Proxy# a -> TypeRep
+class Typeable (a :: k) where
+  typeRep# :: TypeRep a
+
+typeRep :: Typeable a => TypeRep a
+typeRep = typeRep#
+
+typeOf :: Typeable a => a -> TypeRep a
+typeOf _ = typeRep
 
 -- | Takes a value of type @a@ and returns a concrete representation
 -- of that type.
 --
 -- @since 4.7.0.0
-typeRep :: forall proxy a. Typeable a => proxy a -> TypeRep
-typeRep _ = typeRep# (proxy# :: Proxy# a)
+typeRepX :: forall proxy a. Typeable a => proxy a -> SomeTypeRep
+typeRepX _ = SomeTypeRep (typeRep :: TypeRep a)
 {-# INLINE typeRep #-}
 
--- Keeping backwards-compatibility
-typeOf :: forall a. Typeable a => a -> TypeRep
-typeOf _ = typeRep (Proxy :: Proxy a)
-
-typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep
-typeOf1 _ = typeRep (Proxy :: Proxy t)
-
-typeOf2 :: forall t (a :: *) (b :: *). Typeable t => t a b -> TypeRep
-typeOf2 _ = typeRep (Proxy :: Proxy t)
-
-typeOf3 :: forall t (a :: *) (b :: *) (c :: *). Typeable t
-        => t a b c -> TypeRep
-typeOf3 _ = typeRep (Proxy :: Proxy t)
-
-typeOf4 :: forall t (a :: *) (b :: *) (c :: *) (d :: *). Typeable t
-        => t a b c d -> TypeRep
-typeOf4 _ = typeRep (Proxy :: Proxy t)
-
-typeOf5 :: forall t (a :: *) (b :: *) (c :: *) (d :: *) (e :: *). Typeable t
-        => t a b c d e -> TypeRep
-typeOf5 _ = typeRep (Proxy :: Proxy t)
-
-typeOf6 :: forall t (a :: *) (b :: *) (c :: *) (d :: *) (e :: *) (f :: *).
-                Typeable t => t a b c d e f -> TypeRep
-typeOf6 _ = typeRep (Proxy :: Proxy t)
-
-typeOf7 :: forall t (a :: *) (b :: *) (c :: *) (d :: *) (e :: *) (f :: *)
-                (g :: *). Typeable t => t a b c d e f g -> TypeRep
-typeOf7 _ = typeRep (Proxy :: Proxy t)
-
-type Typeable1 (a :: * -> *)                               = Typeable a
-type Typeable2 (a :: * -> * -> *)                          = Typeable a
-type Typeable3 (a :: * -> * -> * -> *)                     = Typeable a
-type Typeable4 (a :: * -> * -> * -> * -> *)                = Typeable a
-type Typeable5 (a :: * -> * -> * -> * -> * -> *)           = Typeable a
-type Typeable6 (a :: * -> * -> * -> * -> * -> * -> *)      = Typeable a
-type Typeable7 (a :: * -> * -> * -> * -> * -> * -> * -> *) = Typeable a
-
-{-# DEPRECATED Typeable1 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-{-# DEPRECATED Typeable2 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-{-# DEPRECATED Typeable3 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-{-# DEPRECATED Typeable4 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-{-# DEPRECATED Typeable5 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-{-# DEPRECATED Typeable6 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-{-# DEPRECATED Typeable7 "renamed to 'Typeable'" #-} -- deprecated in 7.8
-
+typeRepXFingerprint :: SomeTypeRep -> Fingerprint
+typeRepXFingerprint (SomeTypeRep t) = typeRepFingerprint t
 
 ----------------- Showing TypeReps --------------------
 
--- | @since 2.01
-instance Show TypeRep where
-  showsPrec p (TypeRep _ tycon kinds tys) =
-    case tys of
-      [] -> showsPrec p tycon
-      [x]
-        | tycon == tcList -> showChar '[' . shows x . showChar ']'
-        where
-          tcList = tyConOf @[] Proxy
-      [TypeRep _ ptrRepCon _ []]
-        | tycon == tcTYPE && ptrRepCon == tc'LiftedRep
-          -> showChar '*'
-        where
-          tcTYPE         = tyConOf @TYPE            Proxy
-          tc'LiftedRep   = tyConOf @'LiftedRep      Proxy
-      [a,r] | tycon == tcFun  -> showParen (p > 8) $
-                                 showsPrec 9 a .
-                                 showString " -> " .
-                                 showsPrec 8 r
-      xs | isTupleTyCon tycon -> showTuple xs
-         | otherwise         ->
-            showParen (p > 9) $
-            showsPrec p tycon .
-            showChar ' '      .
-            showArgs (showChar ' ') (kinds ++ tys)
-
-showsTypeRep :: TypeRep -> ShowS
-showsTypeRep = shows
-
--- | Helper to fully evaluate 'TypeRep' for use as @NFData(rnf)@ implementation
---
--- @since 4.8.0.0
-rnfTypeRep :: TypeRep -> ()
-rnfTypeRep (TypeRep _ tyc krs tyrs) = rnfTyCon tyc `seq` go krs `seq` go tyrs
+-- This follows roughly the precedence structure described in Note [Precedence
+-- in types].
+instance Show (TypeRep (a :: k)) where
+    showsPrec = showTypeable
+
+
+showTypeable :: Int -> TypeRep (a :: k) -> ShowS
+showTypeable _ rep
+  | Just HRefl <- rep `eqTypeRep` (typeRep :: TypeRep Type) =
+    showChar '*'
+  | isListTyCon tc, [ty] <- tys =
+    showChar '[' . shows ty . showChar ']'
+  | isTupleTyCon tc =
+    showChar '(' . showArgs (showChar ',') tys . showChar ')'
+  where (tc, tys) = splitApps rep
+showTypeable p (TrTyCon _ tycon [])
+  = showsPrec p tycon
+showTypeable p (TrTyCon _ tycon args)
+  = showParen (p > 9) $
+    showsPrec p tycon .
+    showChar ' ' .
+    showArgs (showChar ' ') args
+showTypeable p (TrFun _ x r)
+  = showParen (p > 8) $
+    showsPrec 9 x . showString " -> " . showsPrec 8 r
+showTypeable p (TrApp _ f x)
+  = showParen (p > 9) $
+    showsPrec 8 f .
+    showChar ' ' .
+    showsPrec 10 x
+
+-- | @since 4.10.0.0
+instance Show SomeTypeRep where
+  showsPrec p (SomeTypeRep ty) = showsPrec p ty
+
+splitApps :: TypeRep a -> (TyCon, [SomeTypeRep])
+splitApps = go []
   where
-    go [] = ()
-    go (x:xs) = rnfTypeRep x `seq` go xs
+    go :: [SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
+    go xs (TrTyCon _ tc _) = (tc, xs)
+    go xs (TrApp _ f x)    = go (SomeTypeRep x : xs) f
+    go [] (TrFun _ a b)    = (funTyCon, [SomeTypeRep a, SomeTypeRep b])
+    go _  (TrFun _ _ _)    =
+        error "Data.Typeable.Internal.splitApps: Impossible"
+
+funTyCon :: TyCon
+funTyCon = typeRepTyCon (typeRep @(->))
+
+isListTyCon :: TyCon -> Bool
+isListTyCon tc = tc == typeRepTyCon (typeRep :: TypeRep [Int])
 
--- Some (Show.TypeRep) helpers:
+isTupleTyCon :: TyCon -> Bool
+isTupleTyCon tc
+  | ('(':',':_) <- tyConName tc = True
+  | otherwise                   = False
 
 showArgs :: Show a => ShowS -> [a] -> ShowS
 showArgs _   []     = id
 showArgs _   [a]    = showsPrec 10 a
 showArgs sep (a:as) = showsPrec 10 a . sep . showArgs sep as
 
-showTuple :: [TypeRep] -> ShowS
-showTuple args = showChar '('
-               . showArgs (showChar ',') args
-               . showChar ')'
+-- | Helper to fully evaluate 'TypeRep' for use as @NFData(rnf)@ implementation
+--
+-- @since 4.8.0.0
+rnfTypeRep :: TypeRep a -> ()
+rnfTypeRep (TrTyCon _ tyc _) = rnfTyCon tyc
+rnfTypeRep (TrApp _ f x)     = rnfTypeRep f `seq` rnfTypeRep x
+rnfTypeRep (TrFun _ x y)     = rnfTypeRep x `seq` rnfTypeRep y
+
+-- | Helper to fully evaluate 'SomeTypeRep' for use as @NFData(rnf)@
+-- implementation
+--
+-- @since 4.10.0.0
+rnfSomeTypeRep :: SomeTypeRep -> ()
+rnfSomeTypeRep (SomeTypeRep r) = rnfTypeRep r
 
 {- *********************************************************
 *                                                          *
@@ -403,18 +557,102 @@ showTuple args = showChar '('
 *                                                          *
 ********************************************************* -}
 
-
-mkTypeLitTyCon :: String -> TyCon
-mkTypeLitTyCon name = mkTyCon3 "base" "GHC.TypeLits" name
+pattern KindRepTypeLit :: TypeLitSort -> String -> KindRep
+pattern KindRepTypeLit sort t <- (getKindRepTypeLit -> Just (sort, t))
+  where
+    KindRepTypeLit sort t = KindRepTypeLitD sort t
+
+{-# COMPLETE KindRepTyConApp, KindRepVar, KindRepApp, KindRepFun,
+             KindRepTYPE, KindRepTypeLit #-}
+
+getKindRepTypeLit :: KindRep -> Maybe (TypeLitSort, String)
+getKindRepTypeLit (KindRepTypeLitS sort t) = Just (sort, unpackCString# t)
+getKindRepTypeLit (KindRepTypeLitD sort t) = Just (sort, t)
+getKindRepTypeLit _                        = Nothing
+
+-- | Exquisitely unsafe.
+mkTyCon# :: Addr#       -- ^ package name
+         -> Addr#       -- ^ module name
+         -> Addr#       -- ^ the name of the type constructor
+         -> Int#        -- ^ number of kind variables
+         -> KindRep     -- ^ kind representation
+         -> TyCon       -- ^ A unique 'TyCon' object
+mkTyCon# pkg modl name n_kinds kind_rep
+  | Fingerprint (W64# hi) (W64# lo) <- fingerprint
+  = TyCon hi lo mod (TrNameS name) n_kinds kind_rep
+  where
+    mod = Module (TrNameS pkg) (TrNameS modl)
+    fingerprint :: Fingerprint
+    fingerprint = mkTyConFingerprint (unpackCString# pkg)
+                                     (unpackCString# modl)
+                                     (unpackCString# name)
+
+-- it is extremely important that this fingerprint computation
+-- remains in sync with that in TcTypeable to ensure that type
+-- equality is correct.
+
+-- | Exquisitely unsafe.
+mkTyCon :: String       -- ^ package name
+        -> String       -- ^ module name
+        -> String       -- ^ the name of the type constructor
+        -> Int         -- ^ number of kind variables
+        -> KindRep     -- ^ kind representation
+        -> TyCon        -- ^ A unique 'TyCon' object
+-- Used when the strings are dynamically allocated,
+-- eg from binary deserialisation
+mkTyCon pkg modl name (I# n_kinds) kind_rep
+  | Fingerprint (W64# hi) (W64# lo) <- fingerprint
+  = TyCon hi lo mod (TrNameD name) n_kinds kind_rep
+  where
+    mod = Module (TrNameD pkg) (TrNameD modl)
+    fingerprint :: Fingerprint
+    fingerprint = mkTyConFingerprint pkg modl name
+
+-- This must match the computation done in TcTypeable.mkTyConRepTyConRHS.
+mkTyConFingerprint :: String -- ^ package name
+                   -> String -- ^ module name
+                   -> String -- ^ tycon name
+                   -> Fingerprint
+mkTyConFingerprint pkg_name mod_name tycon_name =
+        fingerprintFingerprints
+        [ fingerprintString pkg_name
+        , fingerprintString mod_name
+        , fingerprintString tycon_name
+        ]
+
+mkTypeLitTyCon :: String -> TyCon -> TyCon
+mkTypeLitTyCon name kind_tycon
+  = mkTyCon "base" "GHC.TypeLits" name 0 kind
+  where kind = KindRepTyConApp kind_tycon []
 
 -- | Used to make `'Typeable' instance for things of kind Nat
-typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep
-typeNatTypeRep p = typeLitTypeRep (show (natVal' p))
+typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep a
+typeNatTypeRep p = typeLitTypeRep (show (natVal' p)) tcNat
 
 -- | Used to make `'Typeable' instance for things of kind Symbol
-typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep
-typeSymbolTypeRep p = typeLitTypeRep (show (symbolVal' p))
+typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep a
+typeSymbolTypeRep p = typeLitTypeRep (show (symbolVal' p)) tcSymbol
+
+mkTypeLitFromString :: TypeLitSort -> String -> SomeTypeRep
+mkTypeLitFromString TypeLitSymbol s =
+    SomeTypeRep $ (typeLitTypeRep s tcSymbol :: TypeRep Symbol)
+mkTypeLitFromString TypeLitNat s =
+    SomeTypeRep $ (typeLitTypeRep s tcSymbol :: TypeRep Nat)
+
+tcSymbol :: TyCon
+tcSymbol = typeRepTyCon (typeRep @Symbol)
+
+tcNat :: TyCon
+tcNat = typeRepTyCon (typeRep @Nat)
 
 -- | An internal function, to make representations for type literals.
-typeLitTypeRep :: String -> TypeRep
-typeLitTypeRep nm = mkTyConApp (mkTypeLitTyCon nm) []
+typeLitTypeRep :: forall (a :: k). (Typeable k) => String -> TyCon -> TypeRep a
+typeLitTypeRep nm kind_tycon = mkTrCon (mkTypeLitTyCon nm kind_tycon) []
+
+-- | For compiler use.
+mkTrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                  (a :: TYPE r1) (b :: TYPE r2).
+           TypeRep a -> TypeRep b -> TypeRep ((a -> b) :: Type)
+mkTrFun arg res = TrFun fpr arg res
+  where fpr = fingerprintFingerprints [ typeRepFingerprint arg
+                                      , typeRepFingerprint res]
diff --git a/libraries/base/GHC/Conc/Sync.hs b/libraries/base/GHC/Conc/Sync.hs
index a9629c41bb..e8823e55f0 100644
--- a/libraries/base/GHC/Conc/Sync.hs
+++ b/libraries/base/GHC/Conc/Sync.hs
@@ -99,11 +99,7 @@ module GHC.Conc.Sync
 import Foreign
 import Foreign.C
 
-#ifndef mingw32_HOST_OS
-import Data.Dynamic
-#else
 import Data.Typeable
-#endif
 import Data.Maybe
 
 import GHC.Base
diff --git a/libraries/base/GHC/Show.hs b/libraries/base/GHC/Show.hs
index 46fc8fe307..510c655a11 100644
--- a/libraries/base/GHC/Show.hs
+++ b/libraries/base/GHC/Show.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE CPP, NoImplicitPrelude, BangPatterns, StandaloneDeriving,
-             MagicHash, UnboxedTuples #-}
+             MagicHash, UnboxedTuples, PolyKinds #-}
 {-# OPTIONS_HADDOCK hide #-}
 
 #include "MachDeps.h"
@@ -201,7 +201,7 @@ deriving instance Show a => Show (Maybe a)
 
 -- | @since 2.01
 instance Show TyCon where
-  showsPrec p (TyCon _ _ _ tc_name) = showsPrec p tc_name
+  showsPrec p (TyCon _ _ _ tc_name _ _) = showsPrec p tc_name
 
 -- | @since 4.9.0.0
 instance Show TrName where
diff --git a/libraries/base/Type/Reflection.hs b/libraries/base/Type/Reflection.hs
new file mode 100644
index 0000000000..37efcba489
--- /dev/null
+++ b/libraries/base/Type/Reflection.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Type.Reflection
+-- Copyright   :  (c) The University of Glasgow, CWI 2001--2017
+-- License     :  BSD-style (see the file libraries/base/LICENSE)
+--
+-- Maintainer  :  libraries@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable (requires GADTs and compiler support)
+--
+-- This provides a type-indexed type representation mechanism, similar to that
+-- described by,
+--
+-- * Simon Peyton-Jones, Stephanie Weirich, Richard Eisenberg,
+-- Dimitrios Vytiniotis. "A reflection on types." /Proc. Philip Wadler's 60th
+-- birthday Festschrift/, Edinburgh (April 2016).
+--
+-- The interface provides 'TypeRep', a type representation which can
+-- be safely decomposed and composed. See "Data.Dynamic" for an example of this.
+--
+-- @since 4.10.0.0
+--
+-----------------------------------------------------------------------------
+module Type.Reflection
+    ( -- * The Typeable class
+      I.Typeable
+    , I.typeRep
+    , I.withTypeable
+
+      -- * Propositional equality
+    , (:~:)(Refl)
+    , (:~~:)(HRefl)
+
+      -- * Type representations
+      -- ** Type-Indexed
+    , I.TypeRep
+    , I.typeOf
+    , pattern I.App, pattern I.Con, pattern I.Con', pattern I.Fun
+    , I.typeRepFingerprint
+    , I.typeRepTyCon
+    , I.rnfTypeRep
+    , I.eqTypeRep
+    , I.typeRepKind
+
+      -- ** Quantified
+      --
+      -- "Data.Typeable" exports a variant of this interface (named differently
+      -- for backwards compatibility).
+    , I.SomeTypeRep(..)
+    , I.typeRepXTyCon
+    , I.rnfSomeTypeRep
+
+      -- * Type constructors
+    , I.TyCon           -- abstract, instance of: Eq, Show, Typeable
+                        -- For now don't export Module, to avoid name clashes
+    , I.tyConPackage
+    , I.tyConModule
+    , I.tyConName
+    , I.rnfTyCon
+    ) where
+
+import qualified Data.Typeable.Internal as I
+import Data.Type.Equality
diff --git a/libraries/base/Type/Reflection/Unsafe.hs b/libraries/base/Type/Reflection/Unsafe.hs
new file mode 100644
index 0000000000..4e367f5722
--- /dev/null
+++ b/libraries/base/Type/Reflection/Unsafe.hs
@@ -0,0 +1,22 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Type.Reflection.Unsafe
+-- Copyright   :  (c) The University of Glasgow, CWI 2001--2015
+-- License     :  BSD-style (see the file libraries/base/LICENSE)
+--
+-- The representations of the types TyCon and TypeRep, and the
+-- function mkTyCon which is used by derived instances of Typeable to
+-- construct a TyCon.
+--
+-- Be warned, these functions can be used to construct ill-typed
+-- type representations.
+--
+-----------------------------------------------------------------------------
+
+module Type.Reflection.Unsafe (
+    tyConKindRep, tyConKindArgs,
+    KindRep(..), TypeLitSort(..),
+    mkTrCon, mkTrApp, mkTyCon
+  ) where
+
+import Data.Typeable.Internal
diff --git a/libraries/base/base.cabal b/libraries/base/base.cabal
index 49e23e5c97..2649173a41 100644
--- a/libraries/base/base.cabal
+++ b/libraries/base/base.cabal
@@ -174,7 +174,6 @@ Library
         Data.Type.Coercion
         Data.Type.Equality
         Data.Typeable
-        Data.Typeable.Internal
         Data.Unique
         Data.Version
         Data.Void
@@ -306,6 +305,8 @@ Library
         Text.Read.Lex
         Text.Show
         Text.Show.Functions
+        Type.Reflection
+        Type.Reflection.Unsafe
         Unsafe.Coerce
 
     other-modules:
@@ -313,6 +314,7 @@ Library
         Control.Monad.ST.Lazy.Imp
         Data.Functor.Utils
         Data.OldList
+        Data.Typeable.Internal
         Foreign.ForeignPtr.Imp
         GHC.StaticPtr.Internal
         System.Environment.ExecutablePath
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index aa7302db0b..fd8f188628 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -56,6 +56,15 @@
     imported from `Control.Applicative`. It is likely to be added to the
     `Prelude` in the future. (#13191)
 
+  * A new module exposing GHC's new type-indexed type representation
+    mechanism, `Type.Reflection`, is now provided.
+
+  * `Data.Dynamic` now exports the `Dyn` data constructor, enabled by the new
+    type-indexed type representation mechanism.
+
+  * `Data.Type.Equality` now provides a kind heterogeneous type equality type,
+    `(:~~:)`.
+
 ## 4.9.0.0  *May 2016*
 
   * Bundled with GHC 8.0
diff --git a/libraries/base/tests/T11334a.stdout b/libraries/base/tests/T11334a.stdout
index caeb85bf44..c2d860d653 100644
--- a/libraries/base/tests/T11334a.stdout
+++ b/libraries/base/tests/T11334a.stdout
@@ -1,3 +1,3 @@
-Proxy (* -> Maybe *) 'Just
+Proxy (* -> Maybe *) ('Just *)
 Proxy * *
 Proxy * (TYPE 'UnliftedRep)
diff --git a/libraries/base/tests/all.T b/libraries/base/tests/all.T
index 8e5125fc3b..7125b636f8 100644
--- a/libraries/base/tests/all.T
+++ b/libraries/base/tests/all.T
@@ -119,7 +119,7 @@ test('T2528', normal, compile_and_run, [''])
 test('T4006', normal, compile_and_run, [''])
 
 test('T5943', normal, compile_and_run, [''])
-test('T5962', expect_broken(10343), compile_and_run, [''])
+test('T5962', normal, compile_and_run, [''])
 test('T7034', normal, compile_and_run, [''])
 
 test('qsem001', normal, compile_and_run, [''])
diff --git a/libraries/base/tests/dynamic002.hs b/libraries/base/tests/dynamic002.hs
index 6d53d2ed1e..3904b45cb7 100644
--- a/libraries/base/tests/dynamic002.hs
+++ b/libraries/base/tests/dynamic002.hs
@@ -1,7 +1,12 @@
+{-# LANGUAGE CPP #-}
+
 -- !!! Testing Typeable instances
 module Main(main) where
 
 import Data.Dynamic
+#if MIN_VERSION_base(4,10,0)
+import Data.Typeable (TyCon, TypeRep, typeOf)
+#endif
 import Data.Array
 import Data.Array.MArray
 import Data.Array.ST
diff --git a/libraries/base/tests/dynamic002.stdout b/libraries/base/tests/dynamic002.stdout
index 8b55566ada..24266824fb 100644
--- a/libraries/base/tests/dynamic002.stdout
+++ b/libraries/base/tests/dynamic002.stdout
@@ -28,7 +28,7 @@ ST () ()
 StableName ()
 StablePtr ()
 TyCon
-TypeRep
+SomeTypeRep
 Word8
 Word16
 Word32
diff --git a/libraries/base/tests/dynamic004.hs b/libraries/base/tests/dynamic004.hs
index e6b7a82bfd..2091646736 100644
--- a/libraries/base/tests/dynamic004.hs
+++ b/libraries/base/tests/dynamic004.hs
@@ -1,7 +1,6 @@
 module Main where
 
 import Data.Typeable
-import Data.Typeable.Internal
 import GHC.Fingerprint
 import Text.Printf
 
diff --git a/libraries/ghc-boot/GHC/Serialized.hs b/libraries/ghc-boot/GHC/Serialized.hs
index fbb96849fb..42a9604c08 100644
--- a/libraries/ghc-boot/GHC/Serialized.hs
+++ b/libraries/ghc-boot/GHC/Serialized.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
 
@@ -26,15 +28,24 @@ import Data.Data
 data Serialized = Serialized TypeRep [Word8]
 
 -- | Put a Typeable value that we are able to actually turn into bytes into a 'Serialized' value ready for deserialization later
-toSerialized :: Typeable a => (a -> [Word8]) -> a -> Serialized
-toSerialized serialize what = Serialized (typeOf what) (serialize what)
+toSerialized :: forall a. Typeable a => (a -> [Word8]) -> a -> Serialized
+toSerialized serialize what = Serialized rep (serialize what)
+  where
+    rep = typeOf what
 
 -- | If the 'Serialized' value contains something of the given type, then use the specified deserializer to return @Just@ that.
 -- Otherwise return @Nothing@.
 fromSerialized :: forall a. Typeable a => ([Word8] -> a) -> Serialized -> Maybe a
+#if MIN_VERSION_base(4,10,0)
+fromSerialized deserialize (Serialized the_type bytes)
+  | the_type == rep = Just (deserialize bytes)
+  | otherwise       = Nothing
+  where rep = typeRep (Proxy :: Proxy a)
+#else
 fromSerialized deserialize (Serialized the_type bytes)
   | the_type == typeOf (undefined :: a) = Just (deserialize bytes)
   | otherwise                           = Nothing
+#endif
 
 -- | Use a 'Data' instance to implement a serialization scheme dual to that of 'deserializeWithData'
 serializeWithData :: Data a => a -> [Word8]
diff --git a/libraries/ghc-prim/GHC/Classes.hs b/libraries/ghc-prim/GHC/Classes.hs
index 5fa118a7f6..3fd4bc06b0 100644
--- a/libraries/ghc-prim/GHC/Classes.hs
+++ b/libraries/ghc-prim/GHC/Classes.hs
@@ -226,10 +226,10 @@ eqInt, neInt :: Int -> Int -> Bool
 
 #if WORD_SIZE_IN_BITS < 64
 instance Eq TyCon where
-  (==) (TyCon hi1 lo1 _ _) (TyCon hi2 lo2 _ _)
+  (==) (TyCon hi1 lo1 _ _ _ _) (TyCon hi2 lo2 _ _ _ _)
        = isTrue# (hi1 `eqWord64#` hi2) && isTrue# (lo1 `eqWord64#` lo2)
 instance Ord TyCon where
-  compare (TyCon hi1 lo1 _ _) (TyCon hi2 lo2 _ _)
+  compare (TyCon hi1 lo1 _ _ _ _) (TyCon hi2 lo2 _ _ _ _)
     | isTrue# (hi1 `gtWord64#` hi2) = GT
     | isTrue# (hi1 `ltWord64#` hi2) = LT
     | isTrue# (lo1 `gtWord64#` lo2) = GT
@@ -237,10 +237,10 @@ instance Ord TyCon where
     | True                = EQ
 #else
 instance Eq TyCon where
-  (==) (TyCon hi1 lo1 _ _) (TyCon hi2 lo2 _ _)
+  (==) (TyCon hi1 lo1 _ _ _ _) (TyCon hi2 lo2 _ _ _ _)
        = isTrue# (hi1 `eqWord#` hi2) && isTrue# (lo1 `eqWord#` lo2)
 instance Ord TyCon where
-  compare (TyCon hi1 lo1 _ _) (TyCon hi2 lo2 _ _)
+  compare (TyCon hi1 lo1 _ _ _ _) (TyCon hi2 lo2 _ _ _ _)
     | isTrue# (hi1 `gtWord#` hi2) = GT
     | isTrue# (hi1 `ltWord#` hi2) = LT
     | isTrue# (lo1 `gtWord#` lo2) = GT
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index c913af6fdb..a4b7a91b59 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -39,17 +39,14 @@ module GHC.Types (
         VecCount(..), VecElem(..),
 
         -- * Runtime type representation
-        Module(..), TrName(..), TyCon(..)
+        Module(..), TrName(..), TyCon(..), TypeLitSort(..),
+        KindRep(..), KindBndr
     ) where
 
 import GHC.Prim
 
 infixr 5 :
 
--- Take note: All types defined here must have associated type representations
--- defined in Data.Typeable.Internal.
--- See Note [Representation of types defined in GHC.Types] below.
-
 {- *********************************************************************
 *                                                                      *
                   Kinds
@@ -443,14 +440,31 @@ data TrName
   = TrNameS Addr#  -- Static
   | TrNameD [Char] -- Dynamic
 
+-- | A de Bruijn index for a binder within a 'KindRep'.
+type KindBndr = Int
+
 #if WORD_SIZE_IN_BITS < 64
-data TyCon = TyCon
-                Word64#  Word64#   -- Fingerprint
-                Module             -- Module in which this is defined
-                TrName              -- Type constructor name
+#define WORD64_TY Word64#
 #else
-data TyCon = TyCon
-                Word#    Word#
-                Module
-                TrName
+#define WORD64_TY Word#
 #endif
+
+-- | The representation produced by GHC for conjuring up the kind of a
+-- 'TypeRep'.
+data KindRep = KindRepTyConApp TyCon [KindRep]
+             | KindRepVar !KindBndr
+             | KindRepApp KindRep KindRep
+             | KindRepFun KindRep KindRep
+             | KindRepTYPE !RuntimeRep
+             | KindRepTypeLitS TypeLitSort Addr#
+             | KindRepTypeLitD TypeLitSort [Char]
+
+data TypeLitSort = TypeLitSymbol
+                 | TypeLitNat
+
+-- Show instance for TyCon found in GHC.Show
+data TyCon = TyCon WORD64_TY WORD64_TY   -- Fingerprint
+                   Module                -- Module in which this is defined
+                   TrName                -- Type constructor name
+                   Int#                  -- How many kind variables do we accept?
+                   KindRep               -- A representation of the type's kind
diff --git a/libraries/ghci/GHCi/Message.hs b/libraries/ghci/GHCi/Message.hs
index 71da2287bb..80a495f9f4 100644
--- a/libraries/ghci/GHCi/Message.hs
+++ b/libraries/ghci/GHCi/Message.hs
@@ -40,6 +40,10 @@ import Data.ByteString (ByteString)
 import qualified Data.ByteString as B
 import qualified Data.ByteString.Lazy as LB
 import Data.Dynamic
+#if MIN_VERSION_base(4,10,0)
+-- Previously this was re-exported by Data.Dynamic
+import Data.Typeable (TypeRep)
+#endif
 import Data.IORef
 import Data.Map (Map)
 import GHC.Generics
@@ -380,7 +384,7 @@ fromSerializableException (EOtherException str) = toException (ErrorCall str)
 -- as the minimum
 instance Binary ExitCode where
   put ExitSuccess      = putWord8 0
-  put (ExitFailure ec) = putWord8 1 `mappend` put ec
+  put (ExitFailure ec) = putWord8 1 >> put ec
   get = do
     w <- getWord8
     case w of
diff --git a/libraries/ghci/GHCi/TH/Binary.hs b/libraries/ghci/GHCi/TH/Binary.hs
index e93095662e..fcff168a9c 100644
--- a/libraries/ghci/GHCi/TH/Binary.hs
+++ b/libraries/ghci/GHCi/TH/Binary.hs
@@ -1,10 +1,23 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+
 -- This module is full of orphans, unfortunately
 module GHCi.TH.Binary () where
 
 import Data.Binary
 import qualified Data.ByteString as B
+#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 GHC.Serialized
 import qualified Language.Haskell.TH        as TH
 import qualified Language.Haskell.TH.Syntax as TH
@@ -66,6 +79,163 @@ instance Binary TH.PatSynArgs
 
 -- We need Binary TypeRep for serializing annotations
 
+#if MIN_VERSION_base(4,10,0)
+instance Binary VecCount where
+    put = putWord8 . fromIntegral . fromEnum
+    get = toEnum . fromIntegral <$> getWord8
+
+instance Binary VecElem where
+    put = putWord8 . fromIntegral . fromEnum
+    get = toEnum . fromIntegral <$> getWord8
+
+instance Binary RuntimeRep where
+    put (VecRep a b)    = putWord8 0 >> put a >> put b
+    put (TupleRep reps) = putWord8 1 >> put reps
+    put (SumRep reps)   = putWord8 2 >> put reps
+    put LiftedRep       = putWord8 3
+    put UnliftedRep     = putWord8 4
+    put IntRep          = putWord8 5
+    put WordRep         = putWord8 6
+    put Int64Rep        = putWord8 7
+    put Word64Rep       = putWord8 8
+    put AddrRep         = putWord8 9
+    put FloatRep        = putWord8 10
+    put DoubleRep       = putWord8 11
+
+    get = do
+        tag <- getWord8
+        case tag of
+          0  -> VecRep <$> get <*> get
+          1  -> TupleRep <$> get
+          2  -> SumRep <$> get
+          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 "GHCi.TH.Binary.putRuntimeRep: invalid tag"
+
+instance Binary TyCon where
+    put tc = do
+        put (tyConPackage tc)
+        put (tyConModule tc)
+        put (tyConName tc)
+        put (tyConKindArgs tc)
+        put (tyConKindRep tc)
+    get = mkTyCon <$> get <*> get <*> get <*> get <*> get
+
+instance Binary KindRep where
+    put (KindRepTyConApp tc k) = putWord8 0 >> put tc >> put k
+    put (KindRepVar bndr) = putWord8 1 >> put bndr
+    put (KindRepApp a b) = putWord8 2 >> put a >> put b
+    put (KindRepFun a b) = putWord8 3 >> put a >> put b
+    put (KindRepTYPE r) = putWord8 4 >> put r
+    put (KindRepTypeLit sort r) = putWord8 5 >> put sort >> put r
+    put _ = fail "GHCi.TH.Binary.putKindRep: Impossible"
+
+    get = do
+        tag <- getWord8
+        case tag of
+          0 -> KindRepTyConApp <$> get <*> get
+          1 -> KindRepVar <$> get
+          2 -> KindRepApp <$> get <*> get
+          3 -> KindRepFun <$> get <*> get
+          4 -> KindRepTYPE <$> get
+          5 -> KindRepTypeLit <$> get <*> get
+          _ -> fail "GHCi.TH.Binary.putKindRep: invalid tag"
+
+instance Binary TypeLitSort where
+    put TypeLitSymbol = putWord8 0
+    put TypeLitNat = putWord8 1
+    get = do
+        tag <- getWord8
+        case tag of
+          0 -> pure TypeLitSymbol
+          1 -> pure TypeLitNat
+          _ -> fail "GHCi.TH.Binary.putTypeLitSort: invalid tag"
+
+putTypeRep :: TypeRep a -> Put
+-- Special handling for TYPE, (->), and RuntimeRep due to recursive kind
+-- relations.
+-- See Note [Mutually recursive representations of primitive types]
+putTypeRep rep  -- Handle Type specially since it's so common
+  | Just HRefl <- rep `eqTypeRep` (typeRep :: TypeRep Type)
+  = put (0 :: Word8)
+putTypeRep (Con' con ks) = do
+    put (1 :: Word8)
+    put con
+    put ks
+putTypeRep (App f x) = do
+    put (2 :: Word8)
+    putTypeRep f
+    putTypeRep x
+putTypeRep (Fun arg res) = do
+    put (3 :: Word8)
+    putTypeRep arg
+    putTypeRep res
+putTypeRep _ = fail "GHCi.TH.Binary.putTypeRep: Impossible"
+
+getSomeTypeRep :: Get SomeTypeRep
+getSomeTypeRep = do
+    tag <- get :: Get Word8
+    case tag of
+        0 -> return $ SomeTypeRep (typeRep :: TypeRep Type)
+        1 -> do con <- get :: Get TyCon
+                ks <- get :: Get [SomeTypeRep]
+                return $ SomeTypeRep $ mkTrCon con ks
+        2 -> do SomeTypeRep f <- getSomeTypeRep
+                SomeTypeRep x <- getSomeTypeRep
+                case typeRepKind f of
+                  Fun arg res ->
+                      case arg `eqTypeRep` typeRepKind x of
+                        Just HRefl -> do
+                            case typeRepKind res `eqTypeRep` (typeRep :: TypeRep Type) of
+                                Just HRefl -> return $ SomeTypeRep $ mkTrApp f x
+                                _ -> failure "Kind mismatch" []
+                        _ -> failure "Kind mismatch"
+                             [ "Found argument of kind:      " ++ show (typeRepKind x)
+                             , "Where the constructor:       " ++ show f
+                             , "Expects an argument of kind: " ++ show arg
+                             ]
+                  _ -> failure "Applied non-arrow type"
+                       [ "Applied type: " ++ show f
+                       , "To argument:  " ++ show x
+                       ]
+        3 -> do SomeTypeRep arg <- getSomeTypeRep
+                SomeTypeRep res <- getSomeTypeRep
+                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" []
+                  Nothing -> failure "Kind mismatch" []
+        _ -> failure "Invalid SomeTypeRep" []
+  where
+    failure description info =
+        fail $ unlines $ [ "GHCi.TH.Binary.getSomeTypeRep: "++description ]
+                      ++ map ("    "++) info
+
+instance Typeable a => Binary (TypeRep (a :: k)) where
+    put = putTypeRep
+    get = do
+        SomeTypeRep rep <- getSomeTypeRep
+        case rep `eqTypeRep` expected of
+          Just HRefl -> pure rep
+          Nothing    -> fail $ unlines
+                        [ "GHCi.TH.Binary: Type mismatch"
+                        , "    Deserialized type: " ++ show rep
+                        , "    Expected type:     " ++ show expected
+                        ]
+     where expected = typeRep :: TypeRep a
+
+instance Binary SomeTypeRep where
+    put (SomeTypeRep rep) = putTypeRep rep
+    get = getSomeTypeRep
+#else
 instance Binary TyCon where
     put tc = put (tyConPackage tc) >> put (tyConModule tc) >> put (tyConName tc)
     get = mkTyCon3 <$> get <*> get <*> get
@@ -75,6 +245,7 @@ instance Binary TypeRep where
     get = do
         (ty_con, child_type_reps) <- get
         return (mkTyConApp ty_con child_type_reps)
+#endif
 
 instance Binary Serialized where
     put (Serialized tyrep wds) = put tyrep >> put (B.pack wds)