{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  GHC.Internal.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   :  stable
-- Portability :  portable
--
-- The 'Typeable' class reifies types to some extent by associating type
-- representations to types. These type representations can be compared,
-- and one can in turn define a type-safe cast operation. To this end,
-- an unsafe cast is guarded by a test for type (representation)
-- equivalence. The module "Data.Dynamic" uses Typeable for an
-- implementation of dynamics. The module "Data.Data" uses Typeable
-- and type-safe cast (but not dynamics) to support the \"Scrap your
-- boilerplate\" style of generic programming.
--
-- == 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 "Type.Reflection".
--
-- Since GHC 7.10, all types automatically have 'Typeable' instances derived.
-- This is in contrast to previous releases where 'Typeable' had to be
-- explicitly derived using the @DeriveDataTypeable@ language extension.
--
-- 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
-- <https://gitlab.haskell.org/ghc/ghc/wikis/ghc-kinds/poly-typeable PolyTypeable wiki page>
--
-----------------------------------------------------------------------------

module GHC.Internal.Data.Typeable
    ( -- * The Typeable class
      Typeable
    , typeOf
    , typeRep

      -- * Propositional equality
    , (:~:)(Refl)
    , (:~~:)(HRefl)

      -- * Type-safe cast
    , cast
    , eqT
    , heqT
    , decT
    , hdecT
    , 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
    , rnfTypeRep
    , showsTypeRep
    , mkFunTy

      -- * Observing type representations
    , funResultTy
    , splitTyConApp
    , typeRepArgs
    , typeRepTyCon
    , 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
    , I.tyConFingerprint

      -- * For backwards compatibility
    , typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7
      -- Jank
    , I.trLiftedRep
    ) where

import qualified GHC.Internal.Data.Typeable.Internal as I
import GHC.Internal.Data.Typeable.Internal (Typeable)
import GHC.Internal.Data.Type.Equality

import GHC.Internal.Data.Either
import GHC.Internal.Data.Maybe
import GHC.Internal.Data.Proxy
import GHC.Internal.Fingerprint.Type
import GHC.Internal.Show
import GHC.Internal.Base

-- | 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 :: forall a. Typeable a => a -> TypeRep
typeOf a
_ = Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a)

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

-- | Show a type representation
showsTypeRep :: TypeRep -> ShowS
showsTypeRep :: TypeRep -> ShowS
showsTypeRep = TypeRep -> ShowS
forall a. Show a => a -> ShowS
shows

-- | The type-safe cast operation
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x
  | Just a :~~: b
HRefl <- TypeRep a
ta TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`I.eqTypeRep` TypeRep b
tb = b -> Maybe b
forall a. a -> Maybe a
Just a
b
x
  | Bool
otherwise                         = Maybe b
forall a. Maybe a
Nothing
  where
    ta :: TypeRep a
ta = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep a
    tb :: TypeRep b
tb = TypeRep b
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep b

-- | Extract a witness of equality of two types
--
-- @since base-4.7.0.0
eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT :: forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  | Just a :~~: b
HRefl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~~: b)
forall {k1} {k2} (a :: k1) (b :: k2).
(Typeable a, Typeable b) =>
Maybe (a :~~: b)
heqT @a @b = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  | Bool
otherwise                = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | Decide an equality of two types
--
-- @since base-4.19.0.0
decT :: forall a b. (Typeable a, Typeable b) => Either (a :~: b -> Void) (a :~: b)
decT :: forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Either ((a :~: b) -> Void) (a :~: b)
decT = case forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Either ((a :~~: b) -> Void) (a :~~: b)
forall {k1} {k2} (a :: k1) (b :: k2).
(Typeable a, Typeable b) =>
Either ((a :~~: b) -> Void) (a :~~: b)
hdecT @a @b of
  Right a :~~: b
HRefl -> (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  Left (a :~~: b) -> Void
p      -> ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left (\a :~: b
Refl -> (a :~~: b) -> Void
p a :~~: a
a :~~: b
forall {k1} (a :: k1). a :~~: a
HRefl)

-- | Extract a witness of heterogeneous equality of two types
--
-- @since base-4.18.0.0
heqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~~: b)
heqT :: forall {k1} {k2} (a :: k1) (b :: k2).
(Typeable a, Typeable b) =>
Maybe (a :~~: b)
heqT = TypeRep a
ta TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`I.eqTypeRep` TypeRep b
tb
  where
    ta :: TypeRep a
ta = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep a
    tb :: TypeRep b
tb = TypeRep b
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep b

-- | Decide heterogeneous equality of two types.
--
-- @since base-4.19.0.0
hdecT :: forall a b. (Typeable a, Typeable b) => Either (a :~~: b -> Void) (a :~~: b)
hdecT :: forall {k1} {k2} (a :: k1) (b :: k2).
(Typeable a, Typeable b) =>
Either ((a :~~: b) -> Void) (a :~~: b)
hdecT = TypeRep a
ta TypeRep a -> TypeRep b -> Either ((a :~~: b) -> Void) (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Either ((a :~~: b) -> Void) (a :~~: b)
`I.decTypeRep` TypeRep b
tb
  where
    ta :: TypeRep a
ta = TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep a
    tb :: TypeRep b
tb = TypeRep b
forall {k} (a :: k). Typeable a => TypeRep a
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)
gcast :: forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast c a
x = ((a :~: b) -> c b) -> Maybe (a :~: b) -> Maybe (c b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :~: b
Refl -> c a
c b
x) (Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
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))
gcast1 :: forall {k} {k} (c :: k -> *) (t :: k -> k) (t' :: k -> k) (a :: k).
(Typeable t, Typeable t') =>
c (t a) -> Maybe (c (t' a))
gcast1 c (t a)
x = ((t :~: t') -> c (t' a)) -> Maybe (t :~: t') -> Maybe (c (t' a))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\t :~: t'
Refl -> c (t a)
c (t' a)
x) (Maybe (t :~: t')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
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))
gcast2 :: forall {k} {k} {k} (c :: k -> *) (t :: k -> k -> k)
       (t' :: k -> k -> k) (a :: k) (b :: k).
(Typeable t, Typeable t') =>
c (t a b) -> Maybe (c (t' a b))
gcast2 c (t a b)
x = ((t :~: t') -> c (t' a b))
-> Maybe (t :~: t') -> Maybe (c (t' a b))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\t :~: t'
Refl -> c (t a b)
c (t' a b)
x) (Maybe (t :~: t')
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT :: Maybe (t :~: t'))

-- | 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 :: TypeRep -> TypeRep -> Maybe TypeRep
funResultTy (I.SomeTypeRep TypeRep a
f) (I.SomeTypeRep TypeRep a
x)
  | Just * :~~: k
HRefl <- (TypeRep (*)
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep Type) TypeRep (*) -> TypeRep k -> Maybe (* :~~: k)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`I.eqTypeRep` TypeRep a -> TypeRep k
forall k (a :: k). TypeRep a -> TypeRep k
I.typeRepKind TypeRep a
f
  , I.Fun TypeRep arg
arg TypeRep res
res <- TypeRep a
f
  , Just arg :~~: a
HRefl <- TypeRep arg
arg TypeRep arg -> TypeRep a -> Maybe (arg :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`I.eqTypeRep` TypeRep a
x
  = TypeRep -> Maybe TypeRep
forall a. a -> Maybe a
Just (TypeRep res -> TypeRep
forall k (a :: k). TypeRep a -> TypeRep
I.SomeTypeRep TypeRep res
res)
  | Bool
otherwise = Maybe TypeRep
forall a. Maybe a
Nothing

-- | Build a function type.
mkFunTy :: TypeRep -> TypeRep -> TypeRep
mkFunTy :: TypeRep -> TypeRep -> TypeRep
mkFunTy (I.SomeTypeRep TypeRep a
arg) (I.SomeTypeRep TypeRep a
res)
  | Just k :~~: *
HRefl <- TypeRep a -> TypeRep k
forall k (a :: k). TypeRep a -> TypeRep k
I.typeRepKind TypeRep a
arg TypeRep k -> TypeRep (*) -> Maybe (k :~~: *)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`I.eqTypeRep` TypeRep (*)
liftedTy
  , Just k :~~: *
HRefl <- TypeRep a -> TypeRep k
forall k (a :: k). TypeRep a -> TypeRep k
I.typeRepKind TypeRep a
res TypeRep k -> TypeRep (*) -> Maybe (k :~~: *)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`I.eqTypeRep` TypeRep (*)
liftedTy
  = TypeRep (a -> a) -> TypeRep
forall k (a :: k). TypeRep a -> TypeRep
I.SomeTypeRep (TypeRep a -> TypeRep a -> TypeRep (a -> a)
forall k (fun :: k) arg res.
(k ~ *, fun ~~ (arg -> res)) =>
TypeRep arg -> TypeRep res -> TypeRep fun
I.Fun TypeRep a
TypeRep a
arg TypeRep a
TypeRep a
res)
  | Bool
otherwise
  = [Char] -> TypeRep
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeRep) -> [Char] -> TypeRep
forall a b. (a -> b) -> a -> b
$ [Char]
"mkFunTy: Attempted to construct function type from non-lifted "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
            [Char]
"type: arg="[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
arg[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
", res="[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
res
  where liftedTy :: TypeRep (*)
liftedTy = TypeRep (*)
forall {k} (a :: k). Typeable a => TypeRep a
I.typeRep :: I.TypeRep Type

-- | Splits a type constructor application. Note that if the type constructor is
-- polymorphic, this will not return the kinds that were used.
splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
splitTyConApp (I.SomeTypeRep TypeRep a
x) = TypeRep a -> (TyCon, [TypeRep])
forall {k} (a :: k). TypeRep a -> (TyCon, [TypeRep])
I.splitApps TypeRep a
x

-- | Observe the argument types of a type representation
typeRepArgs :: TypeRep -> [TypeRep]
typeRepArgs :: TypeRep -> [TypeRep]
typeRepArgs TypeRep
ty = case TypeRep -> (TyCon, [TypeRep])
splitTyConApp TypeRep
ty of (TyCon
_, [TypeRep]
args) -> [TypeRep]
args

-- | Observe the type constructor of a quantified type representation.
typeRepTyCon :: TypeRep -> TyCon
typeRepTyCon :: TypeRep -> TyCon
typeRepTyCon = TypeRep -> TyCon
I.someTypeRepTyCon

-- | Takes a value of type @a@ and returns a concrete representation
-- of that type.
--
-- @since base-4.7.0.0
typeRepFingerprint :: TypeRep -> Fingerprint
typeRepFingerprint :: TypeRep -> Fingerprint
typeRepFingerprint = TypeRep -> Fingerprint
I.someTypeRepFingerprint

-- | Force a 'TypeRep' to normal form.
rnfTypeRep :: TypeRep -> ()
rnfTypeRep :: TypeRep -> ()
rnfTypeRep = TypeRep -> ()
I.rnfSomeTypeRep


-- Keeping backwards-compatibility
typeOf1 :: forall t (a :: Type). Typeable t => t a -> TypeRep
typeOf1 :: forall (t :: * -> *) a. Typeable t => t a -> TypeRep
typeOf1 t a
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)

typeOf2 :: forall t (a :: Type) (b :: Type). Typeable t => t a b -> TypeRep
typeOf2 :: forall (t :: * -> * -> *) a b. Typeable t => t a b -> TypeRep
typeOf2 t a b
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)

typeOf3 :: forall t (a :: Type) (b :: Type) (c :: Type).
           Typeable t => t a b c -> TypeRep
typeOf3 :: forall (t :: * -> * -> * -> *) a b c.
Typeable t =>
t a b c -> TypeRep
typeOf3 t a b c
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)

typeOf4 :: forall t (a :: Type) (b :: Type) (c :: Type) (d :: Type).
           Typeable t => t a b c d -> TypeRep
typeOf4 :: forall (t :: * -> * -> * -> * -> *) a b c d.
Typeable t =>
t a b c d -> TypeRep
typeOf4 t a b c d
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)

typeOf5 :: forall t (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type).
           Typeable t => t a b c d e -> TypeRep
typeOf5 :: forall (t :: * -> * -> * -> * -> * -> *) a b c d e.
Typeable t =>
t a b c d e -> TypeRep
typeOf5 t a b c d e
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)

typeOf6 :: forall t (a :: Type) (b :: Type) (c :: Type)
                    (d :: Type) (e :: Type) (f :: Type).
           Typeable t => t a b c d e f -> TypeRep
typeOf6 :: forall (t :: * -> * -> * -> * -> * -> * -> *) a b c d e f.
Typeable t =>
t a b c d e f -> TypeRep
typeOf6 t a b c d e f
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)

typeOf7 :: forall t (a :: Type) (b :: Type) (c :: Type)
                    (d :: Type) (e :: Type) (f :: Type) (g :: Type).
           Typeable t => t a b c d e f g -> TypeRep
typeOf7 :: forall (t :: * -> * -> * -> * -> * -> * -> * -> *) a b c d e f g.
Typeable t =>
t a b c d e f g -> TypeRep
typeOf7 t a b c d e f g
_ = Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
I.someTypeRep (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)