Data.Type.Equality.Hetero

This module shims kind heterogeneous propositional equality.

Note: some instances: Read, Enum, Bounded and Data would be available only since GHC-8.0 as we need ~~ constraint. Also GH-7.10.3 is nitpicky data constructor ‘HRefl’ cannot be GADT-like in its *kind* arguments, thus this module is available only with GHC >= 8.0

Documentation

data (a :: k1) :~~: (b :: k2) :: forall k1 k2. k1 -> k2 -> Type 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 k2 (a :: k1) (b :: k2). a :~~: a

Instances

TestEquality ((:~~:) a :: k -> Type)

Since: base-4.10.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b)

a ~~ b => Bounded (a :~~: b)

Since: base-4.10.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~~: b

maxBound :: a :~~: b

a ~~ b => Enum (a :~~: b)

Since: base-4.10.0.0

Defined in 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]

Eq (a :~~: b)

Since: base-4.10.0.0

Defined in Data.Type.Equality

Methods

(==) :: (a :~~: b) -> (a :~~: b) -> Bool

(/=) :: (a :~~: b) -> (a :~~: b) -> Bool

Ord (a :~~: b)

Since: base-4.10.0.0

Defined in 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 => Read (a :~~: b)

Since: base-4.10.0.0

Defined in 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

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~~: b) -> ShowS

show :: (a :~~: b) -> String

showList :: [a :~~: b] -> ShowS