{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Trustworthy #-}
{-# 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 #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneKindSignatures #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Typeable.Internal
-- Copyright   :  (c) The University of Glasgow, CWI 2001--2011
-- 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.
--
-----------------------------------------------------------------------------

module Data.Typeable.Internal (
    -- * Typeable and kind polymorphism
    --
    -- #kind_instantiation

    -- * Miscellaneous
    Fingerprint(..),

    -- * Typeable class
    Typeable(..),
    withTypeable,

    -- * Module
    Module,  -- Abstract
    moduleName, modulePackage, rnfModule,

    -- * TyCon
    TyCon,   -- Abstract
    tyConPackage, tyConModule, tyConName, tyConKindArgs, tyConKindRep,
    tyConFingerprint,
    KindRep(.., KindRepTypeLit), TypeLitSort(..),
    rnfTyCon,

    -- * TypeRep
    TypeRep,
    pattern App, pattern Con, pattern Con', pattern Fun,
    typeRep,
    typeOf,
    typeRepTyCon,
    typeRepFingerprint,
    rnfTypeRep,
    eqTypeRep,
    typeRepKind,
    splitApps,

    -- * SomeTypeRep
    SomeTypeRep(..),
    someTypeRep,
    someTypeRepTyCon,
    someTypeRepFingerprint,
    rnfSomeTypeRep,

    -- * Construction
    -- | These are for internal use only
    mkTrType, mkTrCon, mkTrApp, mkTrAppChecked, mkTrFun,
    mkTyCon, mkTyCon#,
    typeSymbolTypeRep, typeNatTypeRep,
  ) where

import GHC.Base
import qualified GHC.Arr as A
import GHC.Types ( TYPE )
import Data.Type.Equality
import GHC.List ( splitAt, foldl', elem )
import GHC.Word
import GHC.Show
import GHC.TypeLits ( KnownSymbol, symbolVal', AppendSymbol )
import GHC.TypeNats ( KnownNat, natVal' )
import Unsafe.Coerce ( unsafeCoerce )

import GHC.Fingerprint.Type
import {-# SOURCE #-} GHC.Fingerprint
   -- loop: GHC.Fingerprint -> Foreign.Ptr -> Data.Typeable
   -- Better to break the loop here, because we want non-SOURCE imports
   -- of Data.Typeable as much as possible so we can optimise the derived
   -- instances.
-- import {-# SOURCE #-} Debug.Trace (trace)

#include "MachDeps.h"

{- *********************************************************************
*                                                                      *
                The TyCon type
*                                                                      *
********************************************************************* -}

modulePackage :: Module -> String
modulePackage :: Module -> String
modulePackage (Module TrName
p TrName
_) = TrName -> String
trNameString TrName
p

moduleName :: Module -> String
moduleName :: Module -> String
moduleName (Module TrName
_ TrName
m) = TrName -> String
trNameString TrName
m

tyConPackage :: TyCon -> String
tyConPackage :: TyCon -> String
tyConPackage (TyCon Word#
_ Word#
_ Module
m TrName
_ Int#
_ KindRep
_) = Module -> String
modulePackage Module
m

tyConModule :: TyCon -> String
tyConModule :: TyCon -> String
tyConModule (TyCon Word#
_ Word#
_ Module
m TrName
_ Int#
_ KindRep
_) = Module -> String
moduleName Module
m

tyConName :: TyCon -> String
tyConName :: TyCon -> String
tyConName (TyCon Word#
_ Word#
_ Module
_ TrName
n Int#
_ KindRep
_) = TrName -> String
trNameString TrName
n

trNameString :: TrName -> String
trNameString :: TrName -> String
trNameString (TrNameS Addr#
s) = Addr# -> String
unpackCStringUtf8# Addr#
s
trNameString (TrNameD String
s) = String
s

tyConFingerprint :: TyCon -> Fingerprint
tyConFingerprint :: TyCon -> Fingerprint
tyConFingerprint (TyCon Word#
hi Word#
lo Module
_ TrName
_ Int#
_ KindRep
_)
  = Word64 -> Word64 -> Fingerprint
Fingerprint (Word# -> Word64
W64# Word#
hi) (Word# -> Word64
W64# Word#
lo)

tyConKindArgs :: TyCon -> Int
tyConKindArgs :: TyCon -> Int
tyConKindArgs (TyCon Word#
_ Word#
_ Module
_ TrName
_ Int#
n KindRep
_) = Int# -> Int
I# Int#
n

tyConKindRep :: TyCon -> KindRep
tyConKindRep :: TyCon -> KindRep
tyConKindRep (TyCon Word#
_ Word#
_ Module
_ TrName
_ Int#
_ KindRep
k) = KindRep
k

-- | Helper to fully evaluate 'TyCon' for use as @NFData(rnf)@ implementation
--
-- @since 4.8.0.0
rnfModule :: Module -> ()
rnfModule :: Module -> ()
rnfModule (Module TrName
p TrName
m) = TrName -> ()
rnfTrName TrName
p () -> () -> ()
`seq` TrName -> ()
rnfTrName TrName
m

rnfTrName :: TrName -> ()
rnfTrName :: TrName -> ()
rnfTrName (TrNameS Addr#
_) = ()
rnfTrName (TrNameD String
n) = String -> ()
rnfString String
n

rnfKindRep :: KindRep -> ()
rnfKindRep :: KindRep -> ()
rnfKindRep (KindRepTyConApp TyCon
tc [KindRep]
args) = TyCon -> ()
rnfTyCon TyCon
tc () -> () -> ()
`seq` (KindRep -> ()) -> [KindRep] -> ()
forall a. (a -> ()) -> [a] -> ()
rnfList KindRep -> ()
rnfKindRep [KindRep]
args
rnfKindRep (KindRepVar Int
_)   = ()
rnfKindRep (KindRepApp KindRep
a KindRep
b) = KindRep -> ()
rnfKindRep KindRep
a () -> () -> ()
`seq` KindRep -> ()
rnfKindRep KindRep
b
rnfKindRep (KindRepFun KindRep
a KindRep
b) = KindRep -> ()
rnfKindRep KindRep
a () -> () -> ()
`seq` KindRep -> ()
rnfKindRep KindRep
b
rnfKindRep (KindRepTYPE RuntimeRep
rr) = RuntimeRep -> ()
rnfRuntimeRep RuntimeRep
rr
rnfKindRep (KindRepTypeLitS TypeLitSort
_ Addr#
_) = ()
rnfKindRep (KindRepTypeLitD TypeLitSort
_ String
t) = String -> ()
rnfString String
t

rnfRuntimeRep :: RuntimeRep -> ()
rnfRuntimeRep :: RuntimeRep -> ()
rnfRuntimeRep (VecRep !VecCount
_ !VecElem
_) = ()
rnfRuntimeRep !RuntimeRep
_             = ()

rnfList :: (a -> ()) -> [a] -> ()
rnfList :: (a -> ()) -> [a] -> ()
rnfList a -> ()
_     []     = ()
rnfList a -> ()
force (a
x:[a]
xs) = a -> ()
force a
x () -> () -> ()
`seq` (a -> ()) -> [a] -> ()
forall a. (a -> ()) -> [a] -> ()
rnfList a -> ()
force [a]
xs

rnfString :: [Char] -> ()
rnfString :: String -> ()
rnfString = (Char -> ()) -> String -> ()
forall a. (a -> ()) -> [a] -> ()
rnfList (Char -> () -> ()
`seq` ())

rnfTyCon :: TyCon -> ()
rnfTyCon :: TyCon -> ()
rnfTyCon (TyCon Word#
_ Word#
_ Module
m TrName
n Int#
_ KindRep
k) = Module -> ()
rnfModule Module
m () -> () -> ()
`seq` TrName -> ()
rnfTrName TrName
n () -> () -> ()
`seq` KindRep -> ()
rnfKindRep KindRep
k


{- *********************************************************************
*                                                                      *
                The TypeRep type
*                                                                      *
********************************************************************* -}

-- | A concrete representation of a (monomorphic) type.
-- 'TypeRep' supports reasonably efficient equality.
type TypeRep :: k -> Type
data TypeRep a where
    -- The TypeRep of Type. See Note [Kind caching], Wrinkle 2
    TrType :: TypeRep Type
    TrTyCon :: { -- See Note [TypeRep fingerprints]
                 TypeRep a -> Fingerprint
trTyConFingerprint :: {-# UNPACK #-} !Fingerprint

                 -- The TypeRep represents the application of trTyCon
                 -- to the kind arguments trKindVars. So for
                 -- 'Just :: Bool -> Maybe Bool, the trTyCon will be
                 -- 'Just and the trKindVars will be [Bool].
               , TypeRep a -> TyCon
trTyCon :: !TyCon
               , TypeRep a -> [SomeTypeRep]
trKindVars :: [SomeTypeRep]
               , TypeRep a -> TypeRep k
trTyConKind :: !(TypeRep k) }  -- See Note [Kind caching]
            -> TypeRep (a :: k)

    -- | Invariant: Saturated arrow types (e.g. things of the form @a -> b@)
    -- are represented with @'TrFun' a b@, not @TrApp (TrApp funTyCon a) b@.
    TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               { -- See Note [TypeRep fingerprints]
                 TypeRep (a b) -> Fingerprint
trAppFingerprint :: {-# UNPACK #-} !Fingerprint

                 -- The TypeRep represents the application of trAppFun
                 -- to trAppArg. For Maybe Int, the trAppFun will be Maybe
                 -- and the trAppArg will be Int.
               , TypeRep (a b) -> TypeRep a
trAppFun :: !(TypeRep (a :: k1 -> k2))
               , TypeRep (a b) -> TypeRep b
trAppArg :: !(TypeRep (b :: k1))
               , TypeRep (a b) -> TypeRep k2
trAppKind :: !(TypeRep k2) }   -- See Note [Kind caching]
            -> TypeRep (a b)

    -- | @TrFun fpr a b@ represents a function type @a -> b@. We use this for
    -- the sake of efficiency as functions are quite ubiquitous.
    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (a :: TYPE r1) (b :: TYPE r2).
               { -- See Note [TypeRep fingerprints]
                 TypeRep (a -> b) -> Fingerprint
trFunFingerprint :: {-# UNPACK #-} !Fingerprint

                 -- The TypeRep represents a function from trFunArg to
                 -- trFunRes.
               , TypeRep (a -> b) -> TypeRep a
trFunArg :: !(TypeRep a)
               , TypeRep (a -> b) -> TypeRep b
trFunRes :: !(TypeRep b) }
            -> TypeRep (a -> b)

{- Note [TypeRep fingerprints]
   ~~~~~~~~~~~~~~~~~~~~~~~~~~~
We store a Fingerprint of each TypeRep in its constructor. This allows
us to test whether two TypeReps are equal in constant time, rather than
having to walk their full structures.
-}

{- Note [Kind caching]
   ~~~~~~~~~~~~~~~~~~~

We cache the kind of the TypeRep in each TrTyCon and TrApp constructor.
This is necessary to ensure that typeRepKind (which is used, at least, in
deserialization and dynApply) is cheap. There are two reasons for this:

1. Calculating the kind of a nest of type applications, such as

  F X Y Z W   (App (App (App (App F X) Y) Z) W)

is linear in the depth, which is already a bit pricy. In deserialization,
we build up such a nest from the inside out, so without caching, that ends
up taking quadratic time, and calculating the KindRep of the constructor,
F, a linear number of times. See #14254.

2. Calculating the kind of a type constructor, in instantiateTypeRep,
requires building (allocating) a TypeRep for the kind "from scratch".
This can get pricy. When combined with point (1), we can end up with
a large amount of extra allocation deserializing very deep nests.
See #14337.

It is quite possible to speed up deserialization by structuring that process
very carefully. Unfortunately, that doesn't help dynApply or anything else
that may use typeRepKind. Since caching the kind isn't terribly expensive, it
seems better to just do that and solve all the potential problems at once.

There are two things we need to be careful about when caching kinds.

Wrinkle 1:

We want to do it eagerly. Suppose we have

  tf :: TypeRep (f :: j -> k)
  ta :: TypeRep (a :: j)

Then the cached kind of App tf ta should be eagerly evaluated to k, rather
than being stored as a thunk that will strip the (j ->) off of j -> k if
and when it is forced.

Wrinkle 2:

We need to be able to represent TypeRep Type. This is a bit tricky because
typeRepKind (typeRep @Type) = typeRep @Type, so if we actually cache the
typerep of the kind of Type, we will have a loop. One simple way to do this
is to make the cached kind fields lazy and allow TypeRep Type to be cyclical.

But we *do not* want TypeReps to have cyclical structure! Most importantly,
a cyclical structure cannot be stored in a compact region. Secondarily,
using :force in GHCi on a cyclical structure will lead to non-termination.

To avoid this trouble, we use a separate constructor for TypeRep Type.
mkTrApp is responsible for recognizing that TYPE is being applied to
'LiftedRep and produce trType; other functions must recognize that TrType
represents an application.
-}

-- Compare keys for equality

-- | @since 2.01
instance Eq (TypeRep a) where
  TypeRep a
_ == :: TypeRep a -> TypeRep a -> Bool
== TypeRep a
_  = Bool
True
  {-# INLINABLE (==) #-}

instance TestEquality TypeRep where
  TypeRep a
a testEquality :: TypeRep a -> TypeRep b -> Maybe (a :~: b)
`testEquality` TypeRep b
b
    | Just a :~~: b
HRefl <- TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
a TypeRep b
b
    = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
    | Bool
otherwise
    = Maybe (a :~: b)
forall a. Maybe a
Nothing
  {-# INLINEABLE testEquality #-}

-- | @since 4.4.0.0
instance Ord (TypeRep a) where
  compare :: TypeRep a -> TypeRep a -> Ordering
compare TypeRep a
_ TypeRep a
_ = Ordering
EQ
  {-# INLINABLE compare #-}

-- | A non-indexed type representation.
data SomeTypeRep where
    SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep

instance Eq SomeTypeRep where
  SomeTypeRep TypeRep a
a == :: SomeTypeRep -> SomeTypeRep -> Bool
== SomeTypeRep TypeRep a
b =
      case TypeRep a
a TypeRep a -> TypeRep a -> Maybe (a :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep a
b of
          Just a :~~: a
_  -> Bool
True
          Maybe (a :~~: a)
Nothing -> Bool
False

instance Ord SomeTypeRep where
  SomeTypeRep TypeRep a
a compare :: SomeTypeRep -> SomeTypeRep -> Ordering
`compare` SomeTypeRep TypeRep a
b =
    TypeRep a -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
a Fingerprint -> Fingerprint -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` TypeRep a -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
b

-- | The function type constructor.
--
-- For instance,
--
-- @
-- typeRep \@(Int -> Char) === Fun (typeRep \@Int) (typeRep \@Char)
-- @
--
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 $bFun :: TypeRep arg -> TypeRep res -> TypeRep fun
$mFun :: forall r k (fun :: k).
TypeRep fun
-> (forall arg res.
    (k ~ *, fun ~~ (arg -> res)) =>
    TypeRep arg -> TypeRep res -> r)
-> (Void# -> r)
-> r
Fun arg res <- TrFun {trFunArg = arg, trFunRes = res}
  where Fun TypeRep arg
arg TypeRep res
res = TypeRep arg -> TypeRep res -> TypeRep (arg -> res)
forall a b. TypeRep a -> TypeRep b -> TypeRep (a -> b)
mkTrFun TypeRep arg
arg TypeRep res
res

-- | Observe the 'Fingerprint' of a type representation
--
-- @since 4.8.0.0
typeRepFingerprint :: TypeRep a -> Fingerprint
typeRepFingerprint :: TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
TrType = Fingerprint
fpTYPELiftedRep
typeRepFingerprint (TrTyCon {trTyConFingerprint :: forall k (a :: k). TypeRep a -> Fingerprint
trTyConFingerprint = Fingerprint
fpr}) = Fingerprint
fpr
typeRepFingerprint (TrApp {trAppFingerprint :: forall k2 k1 (a :: k1 -> k2) (b :: k1).
TypeRep (a b) -> Fingerprint
trAppFingerprint = Fingerprint
fpr}) = Fingerprint
fpr
typeRepFingerprint (TrFun {trFunFingerprint :: forall a b. TypeRep (a -> b) -> Fingerprint
trFunFingerprint = Fingerprint
fpr}) = Fingerprint
fpr

-- For compiler use
mkTrType :: TypeRep Type
mkTrType :: TypeRep *
mkTrType = TypeRep *
TrType

-- | 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 :: TyCon -> [SomeTypeRep] -> TypeRep a
mkTrCon TyCon
tc [SomeTypeRep]
kind_vars = TrTyCon :: forall k (a :: k).
Fingerprint -> TyCon -> [SomeTypeRep] -> TypeRep k -> TypeRep a
TrTyCon
    { trTyConFingerprint :: Fingerprint
trTyConFingerprint = Fingerprint
fpr
    , trTyCon :: TyCon
trTyCon = TyCon
tc
    , trKindVars :: [SomeTypeRep]
trKindVars = [SomeTypeRep]
kind_vars
    , trTyConKind :: TypeRep k
trTyConKind = TypeRep k
kind }
  where
    fpr_tc :: Fingerprint
fpr_tc  = TyCon -> Fingerprint
tyConFingerprint TyCon
tc
    fpr_kvs :: [Fingerprint]
fpr_kvs = (SomeTypeRep -> Fingerprint) -> [SomeTypeRep] -> [Fingerprint]
forall a b. (a -> b) -> [a] -> [b]
map SomeTypeRep -> Fingerprint
someTypeRepFingerprint [SomeTypeRep]
kind_vars
    fpr :: Fingerprint
fpr     = [Fingerprint] -> Fingerprint
fingerprintFingerprints (Fingerprint
fpr_tcFingerprint -> [Fingerprint] -> [Fingerprint]
forall a. a -> [a] -> [a]
:[Fingerprint]
fpr_kvs)
    kind :: TypeRep k
kind    = SomeTypeRep -> TypeRep k
forall k (a :: k). SomeTypeRep -> TypeRep a
unsafeCoerceRep (SomeTypeRep -> TypeRep k) -> SomeTypeRep -> TypeRep k
forall a b. (a -> b) -> a -> b
$ TyCon -> [SomeTypeRep] -> SomeTypeRep
tyConKind TyCon
tc [SomeTypeRep]
kind_vars

-- The fingerprint of Type. We don't store this in the TrType
-- constructor, so we need to build it here.
fpTYPELiftedRep :: Fingerprint
fpTYPELiftedRep :: Fingerprint
fpTYPELiftedRep = [Fingerprint] -> Fingerprint
fingerprintFingerprints
      [TyCon -> Fingerprint
tyConFingerprint TyCon
tyConTYPE, TypeRep 'LiftedRep -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep 'LiftedRep
trLiftedRep]
-- There is absolutely nothing to gain and everything to lose
-- by inlining the worker. The wrapper should inline anyway.
{-# NOINLINE fpTYPELiftedRep #-}

trTYPE :: TypeRep TYPE
trTYPE :: TypeRep TYPE
trTYPE = TypeRep TYPE
forall k (a :: k). Typeable a => TypeRep a
typeRep

trLiftedRep :: TypeRep 'LiftedRep
trLiftedRep :: TypeRep 'LiftedRep
trLiftedRep = TypeRep 'LiftedRep
forall k (a :: k). Typeable a => TypeRep a
typeRep

-- | Construct a representation for a type application that is
-- NOT a saturated arrow type. This is not checked!

-- 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 :: TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrApp TypeRep a
a TypeRep b
b -- See Note [Kind caching], Wrinkle 2
  | Just a :~~: TYPE
HRefl <- TypeRep a
a TypeRep a -> TypeRep TYPE -> Maybe (a :~~: TYPE)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep TYPE
trTYPE
  , Just b :~~: 'LiftedRep
HRefl <- TypeRep b
b TypeRep b -> TypeRep 'LiftedRep -> Maybe (b :~~: 'LiftedRep)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep 'LiftedRep
trLiftedRep
  = TypeRep (a b)
TypeRep *
TrType

  | TrFun {trFunRes :: forall a b. TypeRep (a -> b) -> TypeRep b
trFunRes = TypeRep b
res_kind} <- TypeRep a -> TypeRep (k1 -> k2)
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep a
a
  = TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
Fingerprint
-> TypeRep a -> TypeRep b -> TypeRep k2 -> TypeRep (a b)
TrApp
    { trAppFingerprint :: Fingerprint
trAppFingerprint = Fingerprint
fpr
    , trAppFun :: TypeRep a
trAppFun = TypeRep a
a
    , trAppArg :: TypeRep b
trAppArg = TypeRep b
b
    , trAppKind :: TypeRep k2
trAppKind = TypeRep b
TypeRep k2
res_kind }

  | Bool
otherwise = String -> TypeRep (a b)
forall a. HasCallStack => String -> a
error (String
"Ill-kinded type application: "
                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep (k1 -> k2) -> String
forall a. Show a => a -> String
show (TypeRep a -> TypeRep (k1 -> k2)
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep a
a))
  where
    fpr_a :: Fingerprint
fpr_a = TypeRep a -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
a
    fpr_b :: Fingerprint
fpr_b = TypeRep b -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep b
b
    fpr :: Fingerprint
fpr   = [Fingerprint] -> Fingerprint
fingerprintFingerprints [Fingerprint
fpr_a, Fingerprint
fpr_b]

-- | Construct a representation for a type application that
-- may be a saturated arrow type. This is renamed to mkTrApp in
-- Type.Reflection.Unsafe
mkTrAppChecked :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
                  TypeRep (a :: k1 -> k2)
               -> TypeRep (b :: k1)
               -> TypeRep (a b)
mkTrAppChecked :: TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrAppChecked rep :: TypeRep a
rep@(TrApp {trAppFun :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep a
trAppFun = TypeRep a
p, trAppArg :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep b
trAppArg = TypeRep b
x :: TypeRep x})
               (TypeRep b
y :: TypeRep y)
  | TrTyCon {trTyCon :: forall k (a :: k). TypeRep a -> TyCon
trTyCon=TyCon
con} <- TypeRep a
p
  , TyCon
con TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
funTyCon  -- cheap check first
  , Just (IsTYPE (TypeRep r
rx :: TypeRep rx)) <- TypeRep k1 -> Maybe (IsTYPE k1)
forall a. TypeRep a -> Maybe (IsTYPE a)
isTYPE (TypeRep b -> TypeRep k1
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep b
x)
  , Just (IsTYPE (TypeRep r
ry :: TypeRep ry)) <- TypeRep k1 -> Maybe (IsTYPE k1)
forall a. TypeRep a -> Maybe (IsTYPE a)
isTYPE (TypeRep b -> TypeRep k1
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep b
y)
  , Just (->) b :~~: a b
HRefl <- TypeRep b
-> (Typeable b => Maybe ((->) b :~~: a b))
-> Maybe ((->) b :~~: a b)
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep b
x ((Typeable b => Maybe ((->) b :~~: a b))
 -> Maybe ((->) b :~~: a b))
-> (Typeable b => Maybe ((->) b :~~: a b))
-> Maybe ((->) b :~~: a b)
forall a b. (a -> b) -> a -> b
$ TypeRep r
-> (Typeable r => Maybe ((->) b :~~: a b))
-> Maybe ((->) b :~~: a b)
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep r
rx ((Typeable r => Maybe ((->) b :~~: a b))
 -> Maybe ((->) b :~~: a b))
-> (Typeable r => Maybe ((->) b :~~: a b))
-> Maybe ((->) b :~~: a b)
forall a b. (a -> b) -> a -> b
$ TypeRep r
-> (Typeable r => Maybe ((->) b :~~: a b))
-> Maybe ((->) b :~~: a b)
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep r
ry
                  ((Typeable r => Maybe ((->) b :~~: a b))
 -> Maybe ((->) b :~~: a b))
-> (Typeable r => Maybe ((->) b :~~: a b))
-> Maybe ((->) b :~~: a b)
forall a b. (a -> b) -> a -> b
$ Typeable ((->) b) => TypeRep ((->) b)
forall k (a :: k). Typeable a => TypeRep a
typeRep @((->) x :: TYPE ry -> Type) TypeRep ((->) b) -> TypeRep a -> Maybe ((->) b :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep a
rep
  = TypeRep b -> TypeRep b -> TypeRep (b -> b)
forall a b. TypeRep a -> TypeRep b -> TypeRep (a -> b)
mkTrFun TypeRep b
TypeRep b
x TypeRep b
TypeRep b
y
mkTrAppChecked TypeRep a
a TypeRep b
b = TypeRep a -> TypeRep b -> TypeRep (a b)
forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrApp TypeRep a
a TypeRep b
b

-- | A type application.
--
-- For instance,
--
-- @
-- typeRep \@(Maybe Int) === App (typeRep \@Maybe) (typeRep \@Int)
-- @
--
-- Note that this will also match a function type,
--
-- @
-- typeRep \@(Int# -> Char)
--   ===
-- App (App arrow (typeRep \@Int#)) (typeRep \@Char)
-- @
--
-- where @arrow :: TypeRep ((->) :: TYPE IntRep -> Type -> Type)@.
--
pattern App :: forall k2 (t :: k2). ()
            => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
            => TypeRep a -> TypeRep b -> TypeRep t
pattern $bApp :: TypeRep a -> TypeRep b -> TypeRep t
$mApp :: forall r k2 (t :: k2).
TypeRep t
-> (forall k1 (a :: k1 -> k2) (b :: k1).
    (t ~ a b) =>
    TypeRep a -> TypeRep b -> r)
-> (Void# -> r)
-> r
App f x <- (splitApp -> IsApp f x)
  where App TypeRep a
f TypeRep b
x = TypeRep a -> TypeRep b -> TypeRep (a b)
forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrAppChecked TypeRep a
f TypeRep b
x

data AppOrCon (a :: k) where
    IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
          => TypeRep f -> TypeRep x -> AppOrCon (f x)
    -- See Note [Con evidence]
    IsCon :: IsApplication a ~ "" => TyCon -> [SomeTypeRep] -> AppOrCon a

type family IsApplication (x :: k) :: Symbol where
  IsApplication (_ _) = "An error message about this unifying with \"\" "
     `AppendSymbol` "means that you tried to match a TypeRep with Con or "
     `AppendSymbol` "Con' when the represented type was known to be an "
     `AppendSymbol` "application."
  IsApplication _ = ""

splitApp :: forall k (a :: k). ()
         => TypeRep a
         -> AppOrCon a
splitApp :: TypeRep a -> AppOrCon a
splitApp TypeRep a
TrType = TypeRep TYPE -> TypeRep 'LiftedRep -> AppOrCon *
forall k k' (f :: k' -> k) (k :: k').
TypeRep f -> TypeRep k -> AppOrCon (f k)
IsApp TypeRep TYPE
trTYPE TypeRep 'LiftedRep
trLiftedRep
splitApp (TrApp {trAppFun :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep a
trAppFun = TypeRep a
f, trAppArg :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep b
trAppArg = TypeRep b
x}) = TypeRep a -> TypeRep b -> AppOrCon (a b)
forall k k' (f :: k' -> k) (k :: k').
TypeRep f -> TypeRep k -> AppOrCon (f k)
IsApp TypeRep a
f TypeRep b
x
splitApp rep :: TypeRep a
rep@(TrFun {trFunArg :: forall a b. TypeRep (a -> b) -> TypeRep a
trFunArg=TypeRep a
a, trFunRes :: forall a b. TypeRep (a -> b) -> TypeRep b
trFunRes=TypeRep b
b}) = TypeRep ((->) a) -> TypeRep b -> AppOrCon (a -> b)
forall k k' (f :: k' -> k) (k :: k').
TypeRep f -> TypeRep k -> AppOrCon (f k)
IsApp (TypeRep (->) -> TypeRep a -> TypeRep ((->) a)
forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrApp TypeRep (->)
arr TypeRep a
a) TypeRep b
b
  where arr :: TypeRep (->)
arr = TypeRep (a -> b) -> TypeRep (->)
forall a b. TypeRep (a -> b) -> TypeRep (->)
bareArrow TypeRep a
TypeRep (a -> b)
rep
splitApp (TrTyCon{trTyCon :: forall k (a :: k). TypeRep a -> TyCon
trTyCon = TyCon
con, trKindVars :: forall k (a :: k). TypeRep a -> [SomeTypeRep]
trKindVars = [SomeTypeRep]
kinds})
  = case (Any :~: Any) -> IsApplication a :~: ""
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: IsApplication a :~: "" of
      IsApplication a :~: ""
Refl -> TyCon -> [SomeTypeRep] -> AppOrCon a
forall k (a :: k).
(IsApplication a ~ "") =>
TyCon -> [SomeTypeRep] -> AppOrCon a
IsCon TyCon
con [SomeTypeRep]
kinds

-- | Use a 'TypeRep' as 'Typeable' evidence.
withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
             => TypeRep a -> (Typeable a => r) -> r
withTypeable :: TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep a
rep Typeable a => r
k = Gift a r -> TypeRep a -> r
forall a b. a -> b
unsafeCoerce Gift a r
k' TypeRep a
rep
  where k' :: Gift a r
        k' :: Gift a r
k' = (Typeable a => r) -> Gift a r
forall k (a :: k) r. (Typeable a => r) -> Gift a r
Gift Typeable a => r
k

-- | A helper to satisfy the type checker in 'withTypeable'.
newtype Gift a (r :: TYPE rep) = Gift (Typeable a => r)

-- | Pattern match on a type constructor
pattern Con :: forall k (a :: k). ()
            => IsApplication a ~ "" -- See Note [Con evidence]
            => TyCon -> TypeRep a
pattern $mCon :: forall r k (a :: k).
TypeRep a
-> ((IsApplication a ~ "") => TyCon -> r) -> (Void# -> r) -> r
Con con <- (splitApp -> IsCon con _)

-- | Pattern match on a type constructor including its instantiated kind
-- variables.
--
-- For instance,
--
-- @
-- App (Con' proxyTyCon ks) intRep = typeRep @(Proxy \@Int)
-- @
--
-- will bring into scope,
--
-- @
-- proxyTyCon :: TyCon
-- ks         == [someTypeRep @Type] :: [SomeTypeRep]
-- intRep     == typeRep @Int
-- @
--
pattern Con' :: forall k (a :: k). ()
             => IsApplication a ~ "" -- See Note [Con evidence]
             => TyCon -> [SomeTypeRep] -> TypeRep a
pattern $mCon' :: forall r k (a :: k).
TypeRep a
-> ((IsApplication a ~ "") => TyCon -> [SomeTypeRep] -> r)
-> (Void# -> r)
-> r
Con' con ks <- (splitApp -> IsCon con ks)

-- TODO: Remove Fun when #14253 is fixed
{-# COMPLETE Fun, App, Con  #-}
{-# COMPLETE Fun, App, Con' #-}

{- Note [Con evidence]
    ~~~~~~~~~~~~~~~~~~~

Matching TypeRep t on Con or Con' fakes up evidence that

  IsApplication t ~ "".

Why should anyone care about the value of strange internal type family?
Well, almost nobody cares about it, but the pattern checker does!
For example, suppose we have TypeRep (f x) and we want to get
TypeRep f and TypeRep x. There is no chance that the Con constructor
will match, because (f x) is not a constructor, but without the
IsApplication evidence, omitting it will lead to an incomplete pattern
warning. With the evidence, the pattern checker will see that
Con wouldn't typecheck, so everything works out as it should.

Why do we use Symbols? We would really like to use something like

  type family NotApplication (t :: k) :: Constraint where
    NotApplication (f a) = TypeError ...
    NotApplication _ = ()

Unfortunately, #11503 means that the pattern checker and type checker
will fail to actually reject the mistaken patterns. So we describe the
error in the result type. It's a horrible hack.
-}

----------------- Observation ---------------------

-- | Observe the type constructor of a quantified type representation.
someTypeRepTyCon :: SomeTypeRep -> TyCon
someTypeRepTyCon :: SomeTypeRep -> TyCon
someTypeRepTyCon (SomeTypeRep TypeRep a
t) = TypeRep a -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon TypeRep a
t

-- | Observe the type constructor of a type representation
typeRepTyCon :: TypeRep a -> TyCon
typeRepTyCon :: TypeRep a -> TyCon
typeRepTyCon TypeRep a
TrType = TyCon
tyConTYPE
typeRepTyCon (TrTyCon {trTyCon :: forall k (a :: k). TypeRep a -> TyCon
trTyCon = TyCon
tc}) = TyCon
tc
typeRepTyCon (TrApp {trAppFun :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep a
trAppFun = TypeRep a
a})   = TypeRep a -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon TypeRep a
a
typeRepTyCon (TrFun {})               = TypeRep (->) -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (TypeRep (->) -> TyCon) -> TypeRep (->) -> TyCon
forall a b. (a -> b) -> a -> b
$ Typeable (->) => TypeRep (->)
forall k (a :: k). Typeable a => TypeRep a
typeRep @(->)

-- | Type equality
--
-- @since 4.10
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
             TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
a TypeRep b
b
  | TypeRep a -> TypeRep b -> Bool
forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Bool
sameTypeRep TypeRep a
a TypeRep b
b = (a :~~: b) -> Maybe (a :~~: b)
forall a. a -> Maybe a
Just ((Any :~~: Any) -> a :~~: b
unsafeCoerce# Any :~~: Any
forall k2 (a :: k2). a :~~: a
HRefl)
  | Bool
otherwise       = Maybe (a :~~: b)
forall a. Maybe a
Nothing
-- We want GHC to inline eqTypeRep to get rid of the Maybe
-- in the usual case that it is scrutinized immediately. We
-- split eqTypeRep into a worker and wrapper because otherwise
-- it's much larger than anything we'd want to inline.
{-# INLINABLE eqTypeRep #-}

sameTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
               TypeRep a -> TypeRep b -> Bool
sameTypeRep :: TypeRep a -> TypeRep b -> Bool
sameTypeRep TypeRep a
a TypeRep b
b = TypeRep a -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
a Fingerprint -> Fingerprint -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep b -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep b
b

-------------------------------------------------------------
--
--      Computing kinds
--
-------------------------------------------------------------

-- | Observe the kind of a type.
typeRepKind :: TypeRep (a :: k) -> TypeRep k
typeRepKind :: TypeRep a -> TypeRep k
typeRepKind TypeRep a
TrType = TypeRep k
TypeRep *
TrType
typeRepKind (TrTyCon {trTyConKind :: forall k (a :: k). TypeRep a -> TypeRep k
trTyConKind = TypeRep k
kind}) = TypeRep k
kind
typeRepKind (TrApp {trAppKind :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep k2
trAppKind = TypeRep k
kind}) = TypeRep k
kind
typeRepKind (TrFun {}) = Typeable * => TypeRep *
forall k (a :: k). Typeable a => TypeRep a
typeRep @Type

tyConKind :: TyCon -> [SomeTypeRep] -> SomeTypeRep
tyConKind :: TyCon -> [SomeTypeRep] -> SomeTypeRep
tyConKind (TyCon Word#
_ Word#
_ Module
_ TrName
_ Int#
nKindVars# KindRep
kindRep) [SomeTypeRep]
kindVars =
    let kindVarsArr :: A.Array KindBndr SomeTypeRep
        kindVarsArr :: Array Int SomeTypeRep
kindVarsArr = (Int, Int) -> [SomeTypeRep] -> Array Int SomeTypeRep
forall i e. Ix i => (i, i) -> [e] -> Array i e
A.listArray (Int
0, Int# -> Int
I# (Int#
nKindVars# Int# -> Int# -> Int#
-# Int#
1#)) [SomeTypeRep]
kindVars
    in Array Int SomeTypeRep -> KindRep -> SomeTypeRep
instantiateKindRep Array Int SomeTypeRep
kindVarsArr KindRep
kindRep

instantiateKindRep :: A.Array KindBndr SomeTypeRep -> KindRep -> SomeTypeRep
instantiateKindRep :: Array Int SomeTypeRep -> KindRep -> SomeTypeRep
instantiateKindRep Array Int SomeTypeRep
vars = KindRep -> SomeTypeRep
go
  where
    go :: KindRep -> SomeTypeRep
    go :: KindRep -> SomeTypeRep
go (KindRepTyConApp TyCon
tc [KindRep]
args)
      = let n_kind_args :: Int
n_kind_args = TyCon -> Int
tyConKindArgs TyCon
tc
            ([KindRep]
kind_args, [KindRep]
ty_args) = Int -> [KindRep] -> ([KindRep], [KindRep])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n_kind_args [KindRep]
args
            -- First instantiate tycon kind arguments
            tycon_app :: SomeTypeRep
tycon_app = TypeRep Any -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep Any -> SomeTypeRep) -> TypeRep Any -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ TyCon -> [SomeTypeRep] -> TypeRep Any
forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
mkTrCon TyCon
tc ((KindRep -> SomeTypeRep) -> [KindRep] -> [SomeTypeRep]
forall a b. (a -> b) -> [a] -> [b]
map KindRep -> SomeTypeRep
go [KindRep]
kind_args)
            -- Then apply remaining type arguments
            applyTy :: SomeTypeRep -> KindRep -> SomeTypeRep
            applyTy :: SomeTypeRep -> KindRep -> SomeTypeRep
applyTy (SomeTypeRep TypeRep a
acc) KindRep
ty
              | SomeTypeRep TypeRep a
ty' <- KindRep -> SomeTypeRep
go KindRep
ty
              = TypeRep (Any a) -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep (Any a) -> SomeTypeRep) -> TypeRep (Any a) -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ TypeRep Any -> TypeRep a -> TypeRep (Any a)
forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrApp (TypeRep a -> TypeRep Any
forall a b. a -> b
unsafeCoerce TypeRep a
acc) TypeRep a
ty'
        in (SomeTypeRep -> KindRep -> SomeTypeRep)
-> SomeTypeRep -> [KindRep] -> SomeTypeRep
forall a b. (b -> a -> b) -> b -> [a] -> b
foldl' SomeTypeRep -> KindRep -> SomeTypeRep
applyTy SomeTypeRep
tycon_app [KindRep]
ty_args
    go (KindRepVar Int
var)
      = Array Int SomeTypeRep
vars Array Int SomeTypeRep -> Int -> SomeTypeRep
forall i e. Ix i => Array i e -> i -> e
A.! Int
var
    go (KindRepApp KindRep
f KindRep
a)
      = TypeRep (Any Any) -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep (Any Any) -> SomeTypeRep)
-> TypeRep (Any Any) -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ TypeRep Any -> TypeRep Any -> TypeRep (Any Any)
forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrApp (SomeTypeRep -> TypeRep Any
forall k (a :: k). SomeTypeRep -> TypeRep a
unsafeCoerceRep (SomeTypeRep -> TypeRep Any) -> SomeTypeRep -> TypeRep Any
forall a b. (a -> b) -> a -> b
$ KindRep -> SomeTypeRep
go KindRep
f) (SomeTypeRep -> TypeRep Any
forall k (a :: k). SomeTypeRep -> TypeRep a
unsafeCoerceRep (SomeTypeRep -> TypeRep Any) -> SomeTypeRep -> TypeRep Any
forall a b. (a -> b) -> a -> b
$ KindRep -> SomeTypeRep
go KindRep
a)
    go (KindRepFun KindRep
a KindRep
b)
      = TypeRep (Any -> Any) -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep (Any -> Any) -> SomeTypeRep)
-> TypeRep (Any -> Any) -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ TypeRep Any -> TypeRep Any -> TypeRep (Any -> Any)
forall a b. TypeRep a -> TypeRep b -> TypeRep (a -> b)
mkTrFun (SomeTypeRep -> TypeRep Any
forall k (a :: k). SomeTypeRep -> TypeRep a
unsafeCoerceRep (SomeTypeRep -> TypeRep Any) -> SomeTypeRep -> TypeRep Any
forall a b. (a -> b) -> a -> b
$ KindRep -> SomeTypeRep
go KindRep
a) (SomeTypeRep -> TypeRep Any
forall k (a :: k). SomeTypeRep -> TypeRep a
unsafeCoerceRep (SomeTypeRep -> TypeRep Any) -> SomeTypeRep -> TypeRep Any
forall a b. (a -> b) -> a -> b
$ KindRep -> SomeTypeRep
go KindRep
b)
    go (KindRepTYPE RuntimeRep
LiftedRep) = TypeRep * -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep *
TrType
    go (KindRepTYPE RuntimeRep
r) = SomeKindedTypeRep * -> SomeTypeRep
forall k. SomeKindedTypeRep k -> SomeTypeRep
unkindedTypeRep (SomeKindedTypeRep * -> SomeTypeRep)
-> SomeKindedTypeRep * -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ SomeKindedTypeRep (RuntimeRep -> *)
tYPE SomeKindedTypeRep (RuntimeRep -> *)
-> SomeKindedTypeRep RuntimeRep -> SomeKindedTypeRep *
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` RuntimeRep -> SomeKindedTypeRep RuntimeRep
runtimeRepTypeRep RuntimeRep
r
    go (KindRepTypeLitS TypeLitSort
sort Addr#
s)
      = TypeLitSort -> String -> SomeTypeRep
mkTypeLitFromString TypeLitSort
sort (Addr# -> String
unpackCStringUtf8# Addr#
s)
    go (KindRepTypeLitD TypeLitSort
sort String
s)
      = TypeLitSort -> String -> SomeTypeRep
mkTypeLitFromString TypeLitSort
sort String
s

    tYPE :: SomeKindedTypeRep (RuntimeRep -> *)
tYPE = Typeable TYPE => SomeKindedTypeRep (RuntimeRep -> *)
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @(RuntimeRep -> Type) @TYPE

unsafeCoerceRep :: SomeTypeRep -> TypeRep a
unsafeCoerceRep :: SomeTypeRep -> TypeRep a
unsafeCoerceRep (SomeTypeRep TypeRep a
r) = TypeRep a -> TypeRep a
forall a b. a -> b
unsafeCoerce TypeRep a
r

unkindedTypeRep :: SomeKindedTypeRep k -> SomeTypeRep
unkindedTypeRep :: SomeKindedTypeRep k -> SomeTypeRep
unkindedTypeRep (SomeKindedTypeRep TypeRep a
x) = TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep a
x

data SomeKindedTypeRep k where
    SomeKindedTypeRep :: forall k (a :: k). TypeRep a
                      -> SomeKindedTypeRep k

kApp :: SomeKindedTypeRep (k -> k')
     -> SomeKindedTypeRep k
     -> SomeKindedTypeRep k'
kApp :: SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
kApp (SomeKindedTypeRep TypeRep a
f) (SomeKindedTypeRep TypeRep a
a) =
    TypeRep (a a) -> SomeKindedTypeRep k'
forall k (a :: k). TypeRep a -> SomeKindedTypeRep k
SomeKindedTypeRep (TypeRep a -> TypeRep a -> TypeRep (a a)
forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep a -> TypeRep b -> TypeRep (a b)
mkTrApp TypeRep a
f TypeRep a
a)

kindedTypeRep :: forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep :: SomeKindedTypeRep k
kindedTypeRep = TypeRep a -> SomeKindedTypeRep k
forall k (a :: k). TypeRep a -> SomeKindedTypeRep k
SomeKindedTypeRep (Typeable a => TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep @a)

buildList :: forall k. Typeable k
          => [SomeKindedTypeRep k]
          -> SomeKindedTypeRep [k]
buildList :: [SomeKindedTypeRep k] -> SomeKindedTypeRep [k]
buildList = (SomeKindedTypeRep k
 -> SomeKindedTypeRep [k] -> SomeKindedTypeRep [k])
-> SomeKindedTypeRep [k]
-> [SomeKindedTypeRep k]
-> SomeKindedTypeRep [k]
forall a b. (a -> b -> b) -> b -> [a] -> b
foldr SomeKindedTypeRep k
-> SomeKindedTypeRep [k] -> SomeKindedTypeRep [k]
forall k.
Typeable k =>
SomeKindedTypeRep k
-> SomeKindedTypeRep [k] -> SomeKindedTypeRep [k]
cons SomeKindedTypeRep [k]
nil
  where
    nil :: SomeKindedTypeRep [k]
nil = Typeable '[] => SomeKindedTypeRep [k]
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @[k] @'[]
    cons :: SomeKindedTypeRep k
-> SomeKindedTypeRep [k] -> SomeKindedTypeRep [k]
cons SomeKindedTypeRep k
x SomeKindedTypeRep [k]
rest = TypeRep (':) -> SomeKindedTypeRep (k -> [k] -> [k])
forall k (a :: k). TypeRep a -> SomeKindedTypeRep k
SomeKindedTypeRep (Typeable (':) => TypeRep (':)
forall k (a :: k). Typeable a => TypeRep a
typeRep @'(:)) SomeKindedTypeRep (k -> [k] -> [k])
-> SomeKindedTypeRep k -> SomeKindedTypeRep ([k] -> [k])
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` SomeKindedTypeRep k
x SomeKindedTypeRep ([k] -> [k])
-> SomeKindedTypeRep [k] -> SomeKindedTypeRep [k]
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` SomeKindedTypeRep [k]
rest

runtimeRepTypeRep :: RuntimeRep -> SomeKindedTypeRep RuntimeRep
runtimeRepTypeRep :: RuntimeRep -> SomeKindedTypeRep RuntimeRep
runtimeRepTypeRep RuntimeRep
r =
    case RuntimeRep
r of
      RuntimeRep
LiftedRep   -> Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'LiftedRep
      RuntimeRep
UnliftedRep -> Typeable 'UnliftedRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'UnliftedRep
      VecRep VecCount
c VecElem
e  -> Typeable 'VecRep =>
SomeKindedTypeRep (VecCount -> VecElem -> RuntimeRep)
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @_ @'VecRep
                     SomeKindedTypeRep (VecCount -> VecElem -> RuntimeRep)
-> SomeKindedTypeRep VecCount
-> SomeKindedTypeRep (VecElem -> RuntimeRep)
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` VecCount -> SomeKindedTypeRep VecCount
vecCountTypeRep VecCount
c
                     SomeKindedTypeRep (VecElem -> RuntimeRep)
-> SomeKindedTypeRep VecElem -> SomeKindedTypeRep RuntimeRep
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` VecElem -> SomeKindedTypeRep VecElem
vecElemTypeRep VecElem
e
      TupleRep [RuntimeRep]
rs -> Typeable 'TupleRep =>
SomeKindedTypeRep ([RuntimeRep] -> RuntimeRep)
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @_ @'TupleRep
                     SomeKindedTypeRep ([RuntimeRep] -> RuntimeRep)
-> SomeKindedTypeRep [RuntimeRep] -> SomeKindedTypeRep RuntimeRep
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` [SomeKindedTypeRep RuntimeRep] -> SomeKindedTypeRep [RuntimeRep]
forall k.
Typeable k =>
[SomeKindedTypeRep k] -> SomeKindedTypeRep [k]
buildList ((RuntimeRep -> SomeKindedTypeRep RuntimeRep)
-> [RuntimeRep] -> [SomeKindedTypeRep RuntimeRep]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeRep -> SomeKindedTypeRep RuntimeRep
runtimeRepTypeRep [RuntimeRep]
rs)
      SumRep [RuntimeRep]
rs   -> Typeable 'SumRep => SomeKindedTypeRep ([RuntimeRep] -> RuntimeRep)
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @_ @'SumRep
                     SomeKindedTypeRep ([RuntimeRep] -> RuntimeRep)
-> SomeKindedTypeRep [RuntimeRep] -> SomeKindedTypeRep RuntimeRep
forall k k'.
SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k -> SomeKindedTypeRep k'
`kApp` [SomeKindedTypeRep RuntimeRep] -> SomeKindedTypeRep [RuntimeRep]
forall k.
Typeable k =>
[SomeKindedTypeRep k] -> SomeKindedTypeRep [k]
buildList ((RuntimeRep -> SomeKindedTypeRep RuntimeRep)
-> [RuntimeRep] -> [SomeKindedTypeRep RuntimeRep]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeRep -> SomeKindedTypeRep RuntimeRep
runtimeRepTypeRep [RuntimeRep]
rs)
      RuntimeRep
IntRep      -> Typeable 'IntRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'IntRep
      RuntimeRep
Int8Rep     -> Typeable 'Int8Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Int8Rep
      RuntimeRep
Int16Rep    -> Typeable 'Int16Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Int16Rep
      RuntimeRep
Int32Rep    -> Typeable 'Int32Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Int32Rep
      RuntimeRep
Int64Rep    -> Typeable 'Int64Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Int64Rep
      RuntimeRep
WordRep     -> Typeable 'WordRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'WordRep
      RuntimeRep
Word8Rep    -> Typeable 'Word8Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Word8Rep
      RuntimeRep
Word16Rep   -> Typeable 'Word16Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Word16Rep
      RuntimeRep
Word32Rep   -> Typeable 'Word32Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Word32Rep
      RuntimeRep
Word64Rep   -> Typeable 'Word64Rep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'Word64Rep
      RuntimeRep
AddrRep     -> Typeable 'AddrRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'AddrRep
      RuntimeRep
FloatRep    -> Typeable 'FloatRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'FloatRep
      RuntimeRep
DoubleRep   -> Typeable 'DoubleRep => SomeKindedTypeRep RuntimeRep
Typeable 'LiftedRep => SomeKindedTypeRep RuntimeRep
rep @'DoubleRep
  where
    rep :: forall (a :: RuntimeRep). Typeable a => SomeKindedTypeRep RuntimeRep
    rep :: SomeKindedTypeRep RuntimeRep
rep = Typeable a => SomeKindedTypeRep RuntimeRep
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @RuntimeRep @a

vecCountTypeRep :: VecCount -> SomeKindedTypeRep VecCount
vecCountTypeRep :: VecCount -> SomeKindedTypeRep VecCount
vecCountTypeRep VecCount
c =
    case VecCount
c of
      VecCount
Vec2  -> Typeable 'Vec2 => SomeKindedTypeRep VecCount
forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
rep @'Vec2
      VecCount
Vec4  -> Typeable 'Vec4 => SomeKindedTypeRep VecCount
forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
rep @'Vec4
      VecCount
Vec8  -> Typeable 'Vec8 => SomeKindedTypeRep VecCount
forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
rep @'Vec8
      VecCount
Vec16 -> Typeable 'Vec16 => SomeKindedTypeRep VecCount
forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
rep @'Vec16
      VecCount
Vec32 -> Typeable 'Vec32 => SomeKindedTypeRep VecCount
forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
rep @'Vec32
      VecCount
Vec64 -> Typeable 'Vec64 => SomeKindedTypeRep VecCount
forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
rep @'Vec64
  where
    rep :: forall (a :: VecCount). Typeable a => SomeKindedTypeRep VecCount
    rep :: SomeKindedTypeRep VecCount
rep = Typeable a => SomeKindedTypeRep VecCount
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @VecCount @a

vecElemTypeRep :: VecElem -> SomeKindedTypeRep VecElem
vecElemTypeRep :: VecElem -> SomeKindedTypeRep VecElem
vecElemTypeRep VecElem
e =
    case VecElem
e of
      VecElem
Int8ElemRep     -> Typeable 'Int8ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Int8ElemRep
      VecElem
Int16ElemRep    -> Typeable 'Int16ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Int16ElemRep
      VecElem
Int32ElemRep    -> Typeable 'Int32ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Int32ElemRep
      VecElem
Int64ElemRep    -> Typeable 'Int64ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Int64ElemRep
      VecElem
Word8ElemRep    -> Typeable 'Word8ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Word8ElemRep
      VecElem
Word16ElemRep   -> Typeable 'Word16ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Word16ElemRep
      VecElem
Word32ElemRep   -> Typeable 'Word32ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Word32ElemRep
      VecElem
Word64ElemRep   -> Typeable 'Word64ElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'Word64ElemRep
      VecElem
FloatElemRep    -> Typeable 'FloatElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'FloatElemRep
      VecElem
DoubleElemRep   -> Typeable 'DoubleElemRep => SomeKindedTypeRep VecElem
forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep @'DoubleElemRep
  where
    rep :: forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
    rep :: SomeKindedTypeRep VecElem
rep = Typeable a => SomeKindedTypeRep VecElem
forall k (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep @VecElem @a

bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                    (a :: TYPE r1) (b :: TYPE r2). ()
          => TypeRep (a -> b)
          -> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type)
bareArrow :: TypeRep (a -> b) -> TypeRep (->)
bareArrow (TrFun Fingerprint
_ TypeRep a
a TypeRep b
b) =
    TyCon -> [SomeTypeRep] -> TypeRep (->)
forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
mkTrCon TyCon
funTyCon [TypeRep r1 -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep r1
rep1, TypeRep r2 -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep r2
rep2]
  where
    rep1 :: TypeRep r1
rep1 = TypeRep (TYPE r1) -> TypeRep r1
TypeRep * -> TypeRep 'LiftedRep
getRuntimeRep (TypeRep (TYPE r1) -> TypeRep r1)
-> TypeRep (TYPE r1) -> TypeRep r1
forall a b. (a -> b) -> a -> b
$ TypeRep a -> TypeRep (TYPE r1)
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep a
a :: TypeRep r1
    rep2 :: TypeRep r2
rep2 = TypeRep (TYPE r2) -> TypeRep r2
TypeRep * -> TypeRep 'LiftedRep
getRuntimeRep (TypeRep (TYPE r2) -> TypeRep r2)
-> TypeRep (TYPE r2) -> TypeRep r2
forall a b. (a -> b) -> a -> b
$ TypeRep b -> TypeRep (TYPE r2)
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep b
b :: TypeRep r2
bareArrow TypeRep (a -> b)
_ = String -> TypeRep (->)
forall a. HasCallStack => String -> a
error String
"Data.Typeable.Internal.bareArrow: impossible"

data IsTYPE (a :: Type) where
    IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r)

-- | Is a type of the form @TYPE rep@?
isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a)
isTYPE :: TypeRep a -> Maybe (IsTYPE a)
isTYPE TypeRep a
TrType = IsTYPE * -> Maybe (IsTYPE *)
forall a. a -> Maybe a
Just (TypeRep 'LiftedRep -> IsTYPE *
TypeRep 'LiftedRep -> IsTYPE *
IsTYPE TypeRep 'LiftedRep
trLiftedRep)
isTYPE (TrApp {trAppFun :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep a
trAppFun=TypeRep a
f, trAppArg :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep b
trAppArg=TypeRep b
r})
  | Just a :~~: TYPE
HRefl <- TypeRep a
f TypeRep a -> TypeRep TYPE -> Maybe (a :~~: TYPE)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` Typeable TYPE => TypeRep TYPE
forall k (a :: k). Typeable a => TypeRep a
typeRep @TYPE
  = IsTYPE (TYPE b) -> Maybe (IsTYPE (TYPE b))
forall a. a -> Maybe a
Just (TypeRep b -> IsTYPE (TYPE b)
TypeRep 'LiftedRep -> IsTYPE *
IsTYPE TypeRep b
TypeRep b
r)
isTYPE TypeRep a
_ = Maybe (IsTYPE a)
forall a. Maybe a
Nothing

getRuntimeRep :: forall (r :: RuntimeRep). TypeRep (TYPE r) -> TypeRep r
getRuntimeRep :: TypeRep (TYPE r) -> TypeRep r
getRuntimeRep TypeRep (TYPE r)
TrType = TypeRep r
TypeRep 'LiftedRep
trLiftedRep
getRuntimeRep (TrApp {trAppArg :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep b
trAppArg=TypeRep b
r}) = TypeRep b
TypeRep r
r
getRuntimeRep TypeRep (TYPE r)
_ = String -> TypeRep r
forall a. HasCallStack => String -> a
error String
"Data.Typeable.Internal.getRuntimeRep: impossible"


-------------------------------------------------------------
--
--      The Typeable class and friends
--
-------------------------------------------------------------

-- | The class 'Typeable' allows a concrete representation of a type to
-- be calculated.
class Typeable (a :: k) where
  typeRep# :: TypeRep a

typeRep :: Typeable a => TypeRep a
typeRep :: TypeRep a
typeRep = TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep#

typeOf :: Typeable a => a -> TypeRep a
typeOf :: a -> TypeRep a
typeOf a
_ = TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep

-- | Takes a value of type @a@ and returns a concrete representation
-- of that type.
--
-- @since 4.7.0.0
someTypeRep :: forall proxy a. Typeable a => proxy a -> SomeTypeRep
someTypeRep :: proxy a -> SomeTypeRep
someTypeRep proxy a
_ = TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep a
forall k (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep a)
{-# INLINE typeRep #-}

someTypeRepFingerprint :: SomeTypeRep -> Fingerprint
someTypeRepFingerprint :: SomeTypeRep -> Fingerprint
someTypeRepFingerprint (SomeTypeRep TypeRep a
t) = TypeRep a -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
t

----------------- Showing TypeReps --------------------

-- This follows roughly the precedence structure described in Note [Precedence
-- in types].
instance Show (TypeRep (a :: k)) where
    showsPrec :: Int -> TypeRep a -> String -> String
showsPrec = Int -> TypeRep a -> String -> String
forall k (a :: k). Int -> TypeRep a -> String -> String
showTypeable


showTypeable :: Int -> TypeRep (a :: k) -> ShowS
showTypeable :: Int -> TypeRep a -> String -> String
showTypeable Int
_ TypeRep a
TrType = Char -> String -> String
showChar Char
'*'
showTypeable Int
_ TypeRep a
rep
  | TyCon -> Bool
isListTyCon TyCon
tc, [SomeTypeRep
ty] <- [SomeTypeRep]
tys =
    Char -> String -> String
showChar Char
'[' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTypeRep -> String -> String
forall a. Show a => a -> String -> String
shows SomeTypeRep
ty (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
']'

    -- Take care only to render saturated tuple tycon applications
    -- with tuple notation (#14341).
  | TyCon -> Bool
isTupleTyCon TyCon
tc,
    Just * :~~: k
_ <- TypeRep *
TrType TypeRep * -> TypeRep k -> Maybe (* :~~: k)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep a -> TypeRep k
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep a
rep =
    Char -> String -> String
showChar Char
'(' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [SomeTypeRep] -> String -> String
forall a. Show a => (String -> String) -> [a] -> String -> String
showArgs (Char -> String -> String
showChar Char
',') [SomeTypeRep]
tys (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
')'
  where (TyCon
tc, [SomeTypeRep]
tys) = TypeRep a -> (TyCon, [SomeTypeRep])
forall k (a :: k). TypeRep a -> (TyCon, [SomeTypeRep])
splitApps TypeRep a
rep
showTypeable Int
_ (TrTyCon {trTyCon :: forall k (a :: k). TypeRep a -> TyCon
trTyCon = TyCon
tycon, trKindVars :: forall k (a :: k). TypeRep a -> [SomeTypeRep]
trKindVars = []})
  = TyCon -> String -> String
showTyCon TyCon
tycon
showTypeable Int
p (TrTyCon {trTyCon :: forall k (a :: k). TypeRep a -> TyCon
trTyCon = TyCon
tycon, trKindVars :: forall k (a :: k). TypeRep a -> [SomeTypeRep]
trKindVars = [SomeTypeRep]
args})
  = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    TyCon -> String -> String
showTyCon TyCon
tycon (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Char -> String -> String
showChar Char
' ' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (String -> String) -> [SomeTypeRep] -> String -> String
forall a. Show a => (String -> String) -> [a] -> String -> String
showArgs (Char -> String -> String
showChar Char
' ') [SomeTypeRep]
args
showTypeable Int
p (TrFun {trFunArg :: forall a b. TypeRep (a -> b) -> TypeRep a
trFunArg = TypeRep a
x, trFunRes :: forall a b. TypeRep (a -> b) -> TypeRep b
trFunRes = TypeRep b
r})
  = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    Int -> TypeRep a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
9 TypeRep a
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
" -> " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TypeRep b -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
8 TypeRep b
r
showTypeable Int
p (TrApp {trAppFun :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep a
trAppFun = TypeRep a
f, trAppArg :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep b
trAppArg = TypeRep b
x})
  = Bool -> (String -> String) -> String -> String
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
    Int -> TypeRep a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
8 TypeRep a
f (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Char -> String -> String
showChar Char
' ' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Int -> TypeRep b -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 TypeRep b
x

-- | @since 4.10.0.0
instance Show SomeTypeRep where
  showsPrec :: Int -> SomeTypeRep -> String -> String
showsPrec Int
p (SomeTypeRep TypeRep a
ty) = Int -> TypeRep a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
p TypeRep a
ty

splitApps :: TypeRep a -> (TyCon, [SomeTypeRep])
splitApps :: TypeRep a -> (TyCon, [SomeTypeRep])
splitApps = [SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
forall k (a :: k).
[SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
go []
  where
    go :: [SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
    go :: [SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
go [SomeTypeRep]
xs (TrTyCon {trTyCon :: forall k (a :: k). TypeRep a -> TyCon
trTyCon = TyCon
tc})
      = (TyCon
tc, [SomeTypeRep]
xs)
    go [SomeTypeRep]
xs (TrApp {trAppFun :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep a
trAppFun = TypeRep a
f, trAppArg :: forall k2 k1 (a :: k1 -> k2) (b :: k1). TypeRep (a b) -> TypeRep b
trAppArg = TypeRep b
x})
      = [SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
forall k (a :: k).
[SomeTypeRep] -> TypeRep a -> (TyCon, [SomeTypeRep])
go (TypeRep b -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep b
x SomeTypeRep -> [SomeTypeRep] -> [SomeTypeRep]
forall a. a -> [a] -> [a]
: [SomeTypeRep]
xs) TypeRep a
f
    go [] (TrFun {trFunArg :: forall a b. TypeRep (a -> b) -> TypeRep a
trFunArg = TypeRep a
a, trFunRes :: forall a b. TypeRep (a -> b) -> TypeRep b
trFunRes = TypeRep b
b})
      = (TyCon
funTyCon, [TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep a
a, TypeRep b -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep b
b])
    go [SomeTypeRep]
_  (TrFun {})
      = String -> (TyCon, [SomeTypeRep])
forall a. String -> a
errorWithoutStackTrace String
"Data.Typeable.Internal.splitApps: Impossible 1"
    go [] TypeRep a
TrType = (TyCon
tyConTYPE, [TypeRep 'LiftedRep -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep TypeRep 'LiftedRep
trLiftedRep])
    go [SomeTypeRep]
_ TypeRep a
TrType
      = String -> (TyCon, [SomeTypeRep])
forall a. String -> a
errorWithoutStackTrace String
"Data.Typeable.Internal.splitApps: Impossible 2"

-- This is incredibly shady! We don't really want to do this here; we
-- should really have the compiler reveal the TYPE TyCon directly
-- somehow. We need to construct this by hand because otherwise
-- we end up with horrible and somewhat mysterious loops trying to calculate
-- typeRep @TYPE. For the moment, we use the fact that we can get the proper
-- name of the ghc-prim package from the TyCon of LiftedRep (which we can
-- produce a TypeRep for without difficulty), and then just substitute in the
-- appropriate module and constructor names.
--
-- The ticket to find a better way to deal with this is
-- #14480.
tyConTYPE :: TyCon
tyConTYPE :: TyCon
tyConTYPE = String -> String -> String -> Int -> KindRep -> TyCon
mkTyCon (TyCon -> String
tyConPackage TyCon
liftedRepTyCon) String
"GHC.Prim" String
"TYPE" Int
0
       (KindRep -> KindRep -> KindRep
KindRepFun (TyCon -> [KindRep] -> KindRep
KindRepTyConApp TyCon
liftedRepTyCon []) (RuntimeRep -> KindRep
KindRepTYPE RuntimeRep
LiftedRep))
  where
    liftedRepTyCon :: TyCon
liftedRepTyCon = TypeRep RuntimeRep -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (Typeable RuntimeRep => TypeRep RuntimeRep
forall k (a :: k). Typeable a => TypeRep a
typeRep @RuntimeRep)

funTyCon :: TyCon
funTyCon :: TyCon
funTyCon = TypeRep (->) -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (Typeable (->) => TypeRep (->)
forall k (a :: k). Typeable a => TypeRep a
typeRep @(->))

isListTyCon :: TyCon -> Bool
isListTyCon :: TyCon -> Bool
isListTyCon TyCon
tc = TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep [] -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (TypeRep []
forall k (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep [])

isTupleTyCon :: TyCon -> Bool
isTupleTyCon :: TyCon -> Bool
isTupleTyCon TyCon
tc
  | (Char
'(':Char
',':String
_) <- TyCon -> String
tyConName TyCon
tc = Bool
True
  | Bool
otherwise                   = Bool
False

-- This is only an approximation. We don't have the general
-- character-classification machinery here, so we just do our best.
-- This should work for promoted Haskell 98 data constructors and
-- for TypeOperators type constructors that begin with ASCII
-- characters, but it will miss Unicode operators.
--
-- If we wanted to catch Unicode as well, we ought to consider moving
-- GHC.Lexeme from ghc-boot-th to base. Then we could just say:
--
--   startsVarSym symb || startsConSym symb
--
-- But this is a fair deal of work just for one corner case, so I think I'll
-- leave it like this unless someone shouts.
isOperatorTyCon :: TyCon -> Bool
isOperatorTyCon :: TyCon -> Bool
isOperatorTyCon TyCon
tc
  | Char
symb : String
_ <- TyCon -> String
tyConName TyCon
tc
  , Char
symb Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
`elem` String
"!#$%&*+./<=>?@\\^|-~:" = Bool
True
  | Bool
otherwise                           = Bool
False

showTyCon :: TyCon -> ShowS
showTyCon :: TyCon -> String -> String
showTyCon TyCon
tycon = Bool -> (String -> String) -> String -> String
showParen (TyCon -> Bool
isOperatorTyCon TyCon
tycon) (TyCon -> String -> String
forall a. Show a => a -> String -> String
shows TyCon
tycon)

showArgs :: Show a => ShowS -> [a] -> ShowS
showArgs :: (String -> String) -> [a] -> String -> String
showArgs String -> String
_   []     = String -> String
forall a. a -> a
id
showArgs String -> String
_   [a
a]    = Int -> a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 a
a
showArgs String -> String
sep (a
a:[a]
as) = Int -> a -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec Int
10 a
a (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
sep (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [a] -> String -> String
forall a. Show a => (String -> String) -> [a] -> String -> String
showArgs String -> String
sep [a]
as

-- | Helper to fully evaluate 'TypeRep' for use as @NFData(rnf)@ implementation
--
-- @since 4.8.0.0
rnfTypeRep :: TypeRep a -> ()
-- The TypeRep structure is almost entirely strict by definition. The
-- fingerprinting and strict kind caching ensure that everything
-- else is forced anyway. So we don't need to do anything special
-- to reduce to normal form.
rnfTypeRep :: TypeRep a -> ()
rnfTypeRep !TypeRep a
_ = ()

-- | Helper to fully evaluate 'SomeTypeRep' for use as @NFData(rnf)@
-- implementation
--
-- @since 4.10.0.0
rnfSomeTypeRep :: SomeTypeRep -> ()
rnfSomeTypeRep :: SomeTypeRep -> ()
rnfSomeTypeRep (SomeTypeRep TypeRep a
r) = TypeRep a -> ()
forall k (a :: k). TypeRep a -> ()
rnfTypeRep TypeRep a
r

{- *********************************************************
*                                                          *
*       TyCon/TypeRep definitions for type literals        *
*              (Symbol and Nat)                            *
*                                                          *
********************************************************* -}

pattern KindRepTypeLit :: TypeLitSort -> String -> KindRep
pattern $bKindRepTypeLit :: TypeLitSort -> String -> KindRep
$mKindRepTypeLit :: forall r.
KindRep -> (TypeLitSort -> String -> r) -> (Void# -> r) -> r
KindRepTypeLit sort t <- (getKindRepTypeLit -> Just (sort, t))
  where
    KindRepTypeLit TypeLitSort
sort String
t = TypeLitSort -> String -> KindRep
KindRepTypeLitD TypeLitSort
sort String
t

{-# COMPLETE KindRepTyConApp, KindRepVar, KindRepApp, KindRepFun,
             KindRepTYPE, KindRepTypeLit #-}

getKindRepTypeLit :: KindRep -> Maybe (TypeLitSort, String)
getKindRepTypeLit :: KindRep -> Maybe (TypeLitSort, String)
getKindRepTypeLit (KindRepTypeLitS TypeLitSort
sort Addr#
t) = (TypeLitSort, String) -> Maybe (TypeLitSort, String)
forall a. a -> Maybe a
Just (TypeLitSort
sort, Addr# -> String
unpackCStringUtf8# Addr#
t)
getKindRepTypeLit (KindRepTypeLitD TypeLitSort
sort String
t) = (TypeLitSort, String) -> Maybe (TypeLitSort, String)
forall a. a -> Maybe a
Just (TypeLitSort
sort, String
t)
getKindRepTypeLit KindRep
_                        = Maybe (TypeLitSort, String)
forall a. Maybe a
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# :: Addr# -> Addr# -> Addr# -> Int# -> KindRep -> TyCon
mkTyCon# Addr#
pkg Addr#
modl Addr#
name Int#
n_kinds KindRep
kind_rep
  | Fingerprint (W64# Word#
hi) (W64# Word#
lo) <- Fingerprint
fingerprint
  = Word# -> Word# -> Module -> TrName -> Int# -> KindRep -> TyCon
TyCon Word#
hi Word#
lo Module
mod (Addr# -> TrName
TrNameS Addr#
name) Int#
n_kinds KindRep
kind_rep
  where
    mod :: Module
mod = TrName -> TrName -> Module
Module (Addr# -> TrName
TrNameS Addr#
pkg) (Addr# -> TrName
TrNameS Addr#
modl)
    fingerprint :: Fingerprint
    fingerprint :: Fingerprint
fingerprint = String -> String -> String -> Fingerprint
mkTyConFingerprint (Addr# -> String
unpackCStringUtf8# Addr#
pkg)
                                     (Addr# -> String
unpackCStringUtf8# Addr#
modl)
                                     (Addr# -> String
unpackCStringUtf8# Addr#
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 :: String -> String -> String -> Int -> KindRep -> TyCon
mkTyCon String
pkg String
modl String
name (I# Int#
n_kinds) KindRep
kind_rep
  | Fingerprint (W64# Word#
hi) (W64# Word#
lo) <- Fingerprint
fingerprint
  = Word# -> Word# -> Module -> TrName -> Int# -> KindRep -> TyCon
TyCon Word#
hi Word#
lo Module
mod (String -> TrName
TrNameD String
name) Int#
n_kinds KindRep
kind_rep
  where
    mod :: Module
mod = TrName -> TrName -> Module
Module (String -> TrName
TrNameD String
pkg) (String -> TrName
TrNameD String
modl)
    fingerprint :: Fingerprint
    fingerprint :: Fingerprint
fingerprint = String -> String -> String -> Fingerprint
mkTyConFingerprint String
pkg String
modl String
name

-- This must match the computation done in TcTypeable.mkTyConRepTyConRHS.
mkTyConFingerprint :: String -- ^ package name
                   -> String -- ^ module name
                   -> String -- ^ tycon name
                   -> Fingerprint
mkTyConFingerprint :: String -> String -> String -> Fingerprint
mkTyConFingerprint String
pkg_name String
mod_name String
tycon_name =
        [Fingerprint] -> Fingerprint
fingerprintFingerprints
        [ String -> Fingerprint
fingerprintString String
pkg_name
        , String -> Fingerprint
fingerprintString String
mod_name
        , String -> Fingerprint
fingerprintString String
tycon_name
        ]

mkTypeLitTyCon :: String -> TyCon -> TyCon
mkTypeLitTyCon :: String -> TyCon -> TyCon
mkTypeLitTyCon String
name TyCon
kind_tycon
  = String -> String -> String -> Int -> KindRep -> TyCon
mkTyCon String
"base" String
"GHC.TypeLits" String
name Int
0 KindRep
kind
  where kind :: KindRep
kind = TyCon -> [KindRep] -> KindRep
KindRepTyConApp TyCon
kind_tycon []

-- | Used to make `'Typeable' instance for things of kind Nat
typeNatTypeRep :: KnownNat a => Proxy# a -> TypeRep a
typeNatTypeRep :: Proxy# a -> TypeRep a
typeNatTypeRep Proxy# a
p = String -> TyCon -> TypeRep a
forall k (a :: k). Typeable k => String -> TyCon -> TypeRep a
typeLitTypeRep (Natural -> String
forall a. Show a => a -> String
show (Proxy# a -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' Proxy# a
p)) TyCon
tcNat

-- | Used to make `'Typeable' instance for things of kind Symbol
typeSymbolTypeRep :: KnownSymbol a => Proxy# a -> TypeRep a
typeSymbolTypeRep :: Proxy# a -> TypeRep a
typeSymbolTypeRep Proxy# a
p = String -> TyCon -> TypeRep a
forall k (a :: k). Typeable k => String -> TyCon -> TypeRep a
typeLitTypeRep (String -> String
forall a. Show a => a -> String
show (Proxy# a -> String
forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' Proxy# a
p)) TyCon
tcSymbol

mkTypeLitFromString :: TypeLitSort -> String -> SomeTypeRep
mkTypeLitFromString :: TypeLitSort -> String -> SomeTypeRep
mkTypeLitFromString TypeLitSort
TypeLitSymbol String
s =
    TypeRep Symbol -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep Symbol -> SomeTypeRep) -> TypeRep Symbol -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ (String -> TyCon -> TypeRep Symbol
forall k (a :: k). Typeable k => String -> TyCon -> TypeRep a
typeLitTypeRep String
s TyCon
tcSymbol :: TypeRep Symbol)
mkTypeLitFromString TypeLitSort
TypeLitNat String
s =
    TypeRep Nat -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep (TypeRep Nat -> SomeTypeRep) -> TypeRep Nat -> SomeTypeRep
forall a b. (a -> b) -> a -> b
$ (String -> TyCon -> TypeRep Nat
forall k (a :: k). Typeable k => String -> TyCon -> TypeRep a
typeLitTypeRep String
s TyCon
tcSymbol :: TypeRep Nat)

tcSymbol :: TyCon
tcSymbol :: TyCon
tcSymbol = TypeRep Symbol -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (Typeable Symbol => TypeRep Symbol
forall k (a :: k). Typeable a => TypeRep a
typeRep @Symbol)

tcNat :: TyCon
tcNat :: TyCon
tcNat = TypeRep Nat -> TyCon
forall k (a :: k). TypeRep a -> TyCon
typeRepTyCon (Typeable Nat => TypeRep Nat
forall k (a :: k). Typeable a => TypeRep a
typeRep @Nat)

-- | An internal function, to make representations for type literals.
typeLitTypeRep :: forall k (a :: k). (Typeable k) =>
                  String -> TyCon -> TypeRep a
typeLitTypeRep :: String -> TyCon -> TypeRep a
typeLitTypeRep String
nm TyCon
kind_tycon = TyCon -> [SomeTypeRep] -> TypeRep a
forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
mkTrCon (String -> TyCon -> TyCon
mkTypeLitTyCon String
nm TyCon
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 :: TypeRep a -> TypeRep b -> TypeRep (a -> b)
mkTrFun TypeRep a
arg TypeRep b
res = TrFun :: forall a b.
Fingerprint -> TypeRep a -> TypeRep b -> TypeRep (a -> b)
TrFun
    { trFunFingerprint :: Fingerprint
trFunFingerprint = Fingerprint
fpr
    , trFunArg :: TypeRep a
trFunArg = TypeRep a
arg
    , trFunRes :: TypeRep b
trFunRes = TypeRep b
res }
  where fpr :: Fingerprint
fpr = [Fingerprint] -> Fingerprint
fingerprintFingerprints [ TypeRep a -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
arg
                                      , TypeRep b -> Fingerprint
forall k (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep b
res]

{- $kind_instantiation

Consider a type like 'Data.Proxy.Proxy',

@
data Proxy :: forall k. k -> Type
@

One might think that one could decompose an instantiation of this type like
@Proxy Int@ into two applications,

@
'App' (App a b) c === typeRep @(Proxy Int)
@

where,

@
a = typeRep @Proxy
b = typeRep @Type
c = typeRep @Int
@

However, this isn't the case. Instead we can only decompose into an application
and a constructor,

@
'App' ('Con' proxyTyCon) (typeRep @Int) === typeRep @(Proxy Int)
@

The reason for this is that 'Typeable' can only represent /kind-monomorphic/
types. That is, we must saturate enough of @Proxy@\'s arguments to
fully determine its kind. In the particular case of @Proxy@ this means we must
instantiate the kind variable @k@ such that no @forall@-quantified variables
remain.

While it is not possible to decompose the 'Con' above into an application, it is
possible to observe the kind variable instantiations of the constructor with the
'Con\'' pattern,

@
'App' (Con' proxyTyCon kinds) _ === typeRep @(Proxy Int)
@

Here @kinds@ will be @[typeRep \@Type]@.

-}