Type.Reflection.Compat

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.

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

A non-indexed type representation.

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

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 -}

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

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

Observe the type constructor of a type representation

The function type constructor.

For instance,

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

Type equality decision

Type equality

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

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

Observe the type constructor of a quantified type representation.

Observe the kind of a type.

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 match on a type constructor

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

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

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 -}