Copyright	(c) The University of Glasgow CWI 2001--2017
License	BSD-style (see the file libraries/base/LICENSE)
Maintainer	libraries@haskell.org
Stability	stable
Portability	non-portable (requires GADTs and compiler support)
Safe Haskell	Safe-Inferred
Language	Haskell2010

GHC.Internal.Type.Reflection

Contents

The Typeable class
Propositional equality
Type representations
- Type-Indexed
- Quantified
Type constructors
Module names

Description

This provides a type-indexed type representation mechanism, similar to that described by,

Simon Peyton-Jones, Stephanie Weirich, Richard Eisenberg, Dimitrios Vytiniotis. "A reflection on types". Proc. Philip Wadler's 60th birthday Festschrift, Edinburgh (April 2016).

The interface provides TypeRep, a type representation which can be safely decomposed and composed. See Data.Dynamic for an example of this.

Since: base-4.10.0.0

Synopsis

class Typeable (a :: k)
typeRep :: forall {k} (a :: k). Typeable a => TypeRep a
withTypeable :: forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
data (a :: k) :~: (b :: k) where
- Refl :: forall {k} (a :: k). a :~: a
data (a :: k1) :~~: (b :: k2) where
- HRefl :: forall {k1} (a :: k1). a :~~: a
data TypeRep (a :: k)
pattern TypeRep :: () => Typeable a => TypeRep a
typeOf :: Typeable a => a -> TypeRep a
pattern App :: forall k2 t k1 a b. () => t ~ a b => TypeRep a -> TypeRep b -> TypeRep t
pattern Con :: () => NotApplication a => TyCon -> TypeRep a
pattern Con' :: () => NotApplication a => TyCon -> [SomeTypeRep] -> TypeRep a
pattern Fun :: forall k fun (r1 :: RuntimeRep) (r2 :: RuntimeRep) arg res. () => (k ~ Type, fun ~~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun
typeRepTyCon :: forall {k} (a :: k). TypeRep a -> TyCon
rnfTypeRep :: forall {k} (a :: k). TypeRep a -> ()
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
decTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Either ((a :~~: b) -> Void) (a :~~: b)
typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
splitApps :: forall {k} (a :: k). TypeRep a -> (TyCon, [SomeTypeRep])
data SomeTypeRep where
- SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep
someTypeRep :: forall {k} proxy (a :: k). Typeable a => proxy a -> SomeTypeRep
someTypeRepTyCon :: SomeTypeRep -> TyCon
rnfSomeTypeRep :: SomeTypeRep -> ()
data TyCon
tyConPackage :: TyCon -> String
tyConModule :: TyCon -> String
tyConName :: TyCon -> String
rnfTyCon :: TyCon -> ()
data Module
moduleName :: Module -> String
modulePackage :: Module -> String
rnfModule :: Module -> ()

The Typeable class

class Typeable (a :: k) #

The class Typeable allows a concrete representation of a type to be calculated.

Minimal complete definition

typeRep#

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

withTypeable :: forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r #

Use a TypeRep as Typeable evidence.

The TypeRep pattern synonym brings a Typeable constraint into scope and can be used in place of withTypeable.

f :: TypeRep a -> ..
f rep = withTypeable {- Typeable a in scope -}

f :: TypeRep a -> ..
f TypeRep = {- Typeable a in scope -}

Propositional equality

data (a :: k) :~: (b :: k) where infix 4 #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a

Instances

Instances details

Category ((:~:) :: k -> k -> Type) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~: a # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c #
TestCoercion ((:~:) a :: k -> Type) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) #
TestEquality ((:~:) a :: k -> Type) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
Eq (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering # (<) :: (a :~: b) -> (a :~: b) -> Bool # (<=) :: (a :~: b) -> (a :~: b) -> Bool # (>) :: (a :~: b) -> (a :~: b) -> Bool # (>=) :: (a :~: b) -> (a :~: b) -> Bool # max :: (a :~: b) -> (a :~: b) -> a :~: b # min :: (a :~: b) -> (a :~: b) -> a :~: b #
(a ~ b, Data a) => Data (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #
a ~ b => Bounded (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> a :~: b # toEnum :: Int -> a :~: b # fromEnum :: (a :~: b) -> Int # enumFrom :: (a :~: b) -> [a :~: b] # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] #
a ~ b => Read (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) # readList :: ReadS [a :~: b] # readPrec :: ReadPrec (a :~: b) # readListPrec :: ReadPrec [a :~: b] #
Show (a :~: b) #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #

data (a :: k1) :~~: (b :: k2) where infix 4 #

Kind heterogeneous propositional equality. Like :~:, a :~~: b is inhabited by a terminating value if and only if a is the same type as b.

Since: base-4.10.0.0

Constructors

HRefl :: forall {k1} (a :: k1). a :~~: a

Instances

Instances details

Category ((:~~:) :: k -> k -> Type) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~~: a # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~~: c) -> (a :~~: b) -> a :~~: c #
TestCoercion ((:~~:) a :: k -> Type) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) #
TestEquality ((:~~:) a :: k -> Type) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
Eq (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~~: b) -> (a :~~: b) -> Bool # (/=) :: (a :~~: b) -> (a :~~: b) -> Bool #
Ord (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods compare :: (a :~~: b) -> (a :~~: b) -> Ordering # (<) :: (a :~~: b) -> (a :~~: b) -> Bool # (<=) :: (a :~~: b) -> (a :~~: b) -> Bool # (>) :: (a :~~: b) -> (a :~~: b) -> Bool # (>=) :: (a :~~: b) -> (a :~~: b) -> Bool # max :: (a :~~: b) -> (a :~~: b) -> a :~~: b # min :: (a :~~: b) -> (a :~~: b) -> a :~~: b #
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) # toConstr :: (a :~~: b) -> Constr # dataTypeOf :: (a :~~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) #
a ~~ b => Bounded (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~~: b # maxBound :: a :~~: b #
a ~~ b => Enum (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods succ :: (a :~~: b) -> a :~~: b # pred :: (a :~~: b) -> a :~~: b # toEnum :: Int -> a :~~: b # fromEnum :: (a :~~: b) -> Int # enumFrom :: (a :~~: b) -> [a :~~: b] # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] #
a ~~ b => Read (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~~: b) # readList :: ReadS [a :~~: b] # readPrec :: ReadPrec (a :~~: b) # readListPrec :: ReadPrec [a :~~: b] #
Show (a :~~: b) #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~~: b) -> ShowS # show :: (a :~~: b) -> String # showList :: [a :~~: b] -> ShowS #

Type representations

Type-Indexed

data TypeRep (a :: k) #

TypeRep is a concrete representation of a (monomorphic) type. TypeRep supports reasonably efficient equality. See Note [Grand plan for Typeable] in GHC.Tc.Instance.Typeable

Instances

Instances details

TestEquality (TypeRep :: k -> Type) #
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) #
Eq (TypeRep a) #	Since: base-2.1
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods (==) :: TypeRep a -> TypeRep a -> Bool # (/=) :: TypeRep a -> TypeRep a -> Bool #
Ord (TypeRep a) #	Since: base-4.4.0.0
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods compare :: TypeRep a -> TypeRep a -> Ordering # (<) :: TypeRep a -> TypeRep a -> Bool # (<=) :: TypeRep a -> TypeRep a -> Bool # (>) :: TypeRep a -> TypeRep a -> Bool # (>=) :: TypeRep a -> TypeRep a -> Bool # max :: TypeRep a -> TypeRep a -> TypeRep a # min :: TypeRep a -> TypeRep a -> TypeRep a #
Show (TypeRep a) #
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods showsPrec :: Int -> TypeRep a -> ShowS # show :: TypeRep a -> String # showList :: [TypeRep a] -> ShowS #

pattern TypeRep :: () => Typeable a => TypeRep a #

A explicitly bidirectional pattern synonym to construct a concrete representation of a type.

As an expression: Constructs a singleton TypeRep a given a implicit 'Typeable a' constraint:

TypeRep @a :: Typeable a => TypeRep a

As a pattern: Matches on an explicit TypeRep a witness bringing an implicit Typeable a constraint into scope.

f :: TypeRep a -> ..
f TypeRep = {- Typeable a in scope -}

Since: base-4.17.0.0

typeOf :: Typeable a => a -> TypeRep a #

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

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 Con :: () => NotApplication a => TyCon -> TypeRep a #

Pattern match on a type constructor

pattern Con' :: () => NotApplication a => TyCon -> [SomeTypeRep] -> TypeRep a #

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 Fun :: forall k fun (r1 :: RuntimeRep) (r2 :: RuntimeRep) arg res. () => (k ~ Type, fun ~~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun #

The function type constructor.

For instance,

typeRep @(Int -> Char) === Fun (typeRep @Int) (typeRep @Char)

typeRepTyCon :: forall {k} (a :: k). TypeRep a -> TyCon #

Observe the type constructor of a type representation

rnfTypeRep :: forall {k} (a :: k). TypeRep a -> () #

Helper to fully evaluate TypeRep for use as NFData(rnf) implementation

Since: base-4.8.0.0

eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) #

Type equality

Since: base-4.10

decTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Either ((a :~~: b) -> Void) (a :~~: b) #

Type equality decision

Since: base-4.19.0.0

typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k #

Observe the kind of a type.

splitApps :: forall {k} (a :: k). TypeRep a -> (TyCon, [SomeTypeRep]) #

Quantified

data SomeTypeRep where #

A non-indexed type representation.

Constructors

SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep

Instances

Instances details

Eq SomeTypeRep #
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods (==) :: SomeTypeRep -> SomeTypeRep -> Bool # (/=) :: SomeTypeRep -> SomeTypeRep -> Bool #
Ord SomeTypeRep #
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods compare :: SomeTypeRep -> SomeTypeRep -> Ordering # (<) :: SomeTypeRep -> SomeTypeRep -> Bool # (<=) :: SomeTypeRep -> SomeTypeRep -> Bool # (>) :: SomeTypeRep -> SomeTypeRep -> Bool # (>=) :: SomeTypeRep -> SomeTypeRep -> Bool # max :: SomeTypeRep -> SomeTypeRep -> SomeTypeRep # min :: SomeTypeRep -> SomeTypeRep -> SomeTypeRep #
Show SomeTypeRep #	Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods showsPrec :: Int -> SomeTypeRep -> ShowS # show :: SomeTypeRep -> String # showList :: [SomeTypeRep] -> ShowS #

someTypeRep :: forall {k} proxy (a :: k). Typeable a => proxy a -> SomeTypeRep #

Takes a value of type a and returns a concrete representation of that type.

Since: base-4.7.0.0

someTypeRepTyCon :: SomeTypeRep -> TyCon #

Observe the type constructor of a quantified type representation.

rnfSomeTypeRep :: SomeTypeRep -> () #

Helper to fully evaluate SomeTypeRep for use as NFData(rnf) implementation

Since: base-4.10.0.0

Type constructors

data TyCon #

Instances

Instances details

Eq TyCon #
Instance details Defined in GHC.Internal.Classes Methods (==) :: TyCon -> TyCon -> Bool # (/=) :: TyCon -> TyCon -> Bool #
Ord TyCon #
Instance details Defined in GHC.Internal.Classes Methods compare :: TyCon -> TyCon -> Ordering # (<) :: TyCon -> TyCon -> Bool # (<=) :: TyCon -> TyCon -> Bool # (>) :: TyCon -> TyCon -> Bool # (>=) :: TyCon -> TyCon -> Bool # max :: TyCon -> TyCon -> TyCon # min :: TyCon -> TyCon -> TyCon #
Show TyCon #	Since: base-2.1
Instance details Defined in GHC.Internal.Show Methods showsPrec :: Int -> TyCon -> ShowS # show :: TyCon -> String # showList :: [TyCon] -> ShowS #

tyConPackage :: TyCon -> String #

tyConModule :: TyCon -> String #

tyConName :: TyCon -> String #

rnfTyCon :: TyCon -> () #

Module names

data Module #

Instances

Instances details

Eq Module #
Instance details Defined in GHC.Internal.Classes Methods (==) :: Module -> Module -> Bool # (/=) :: Module -> Module -> Bool #
Show Module #	Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Show Methods showsPrec :: Int -> Module -> ShowS # show :: Module -> String # showList :: [Module] -> ShowS #

moduleName :: Module -> String #

modulePackage :: Module -> String #

rnfModule :: Module -> () #

Helper to fully evaluate TyCon for use as NFData(rnf) implementation

Since: base-4.8.0.0