type-eq-0.5: Type equality evidence you can carry around

Safe HaskellTrustworthy
LanguageHaskell98

Type.Eq.Poly

Contents

Description

Kind-polymorphic functions for manipulating type equality evidence.

This module is available only if PolyKinds are available (GHC 7.6+).

Synopsis

Documentation

module Type.Eq

(|.|) :: (b :~: c) -> (a :~: b) -> a :~: c Source

Synonym for composeEq. Kind-polymorphic, unlike (.).

applyEq :: (f :~: g) -> (a :~: b) -> f a :~: g b Source

Congruence?

(|$|) :: (f :~: g) -> (a :~: b) -> f a :~: g b Source

Congruence?

constructorEq :: (f a :~: g b) -> f :~: g Source

Type constructors are generative

dynamicEq1 :: (Typeable1 f, Typeable1 g) => Maybe (f :~: g) Source

Runtime type equality evidence from Typeable1

dynamicEq2 :: (Typeable2 n, Typeable2 m) => Maybe (n :~: m) Source

Runtime type equality evidence from Typeable2

dynamicEq3 :: (Typeable3 x, Typeable3 y) => Maybe (x :~: y) Source

Runtime type equality evidence from Typeable3

dynamicEq4 :: (Typeable4 x, Typeable4 y) => Maybe (x :~: y) Source

Runtime type equality evidence from Typeable4

dynamicEq5 :: (Typeable5 x, Typeable5 y) => Maybe (x :~: y) Source

Runtime type equality evidence from Typeable5

dynamicEq6 :: (Typeable6 x, Typeable6 y) => Maybe (x :~: y) Source

Runtime type equality evidence from Typeable6

dynamicEq7 :: (Typeable7 x, Typeable7 y) => Maybe (x :~: y) Source

Runtime type equality evidence from Typeable7

sameOuterEq :: OuterEq f a -> OuterEq g a -> f :~: g Source

Compatibility with Type.Eq.Higher

fromEq1 :: (f ::~:: g) -> f :~: g Source

toEq1 :: (f :~: g) -> f ::~:: g Source

fromEq2 :: (n :::~::: m) -> n :~: m Source

toEq2 :: (n :~: m) -> n :::~::: m Source