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

Safe HaskellTrustworthy

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 :~: cSource

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

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

Congruence?

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

Congruence?

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

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 :~: gSource

Compatibility with Type.Eq.Higher

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

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

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

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