type-equality-1: Data.Type.Equality compat package
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Type.Equality.Hetero

Description

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) where #

Constructors

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

Instances

Instances details
TestEquality ((:~~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b)

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

Defined in Data.Type.Equality

Methods

minBound :: a :~~: b

maxBound :: a :~~: b

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

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]

a ~~ b => Read (a :~~: b) 
Instance details

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) 
Instance details

Defined in Data.Type.Equality

Methods

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

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

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

Eq (a :~~: b) 
Instance details

Defined in Data.Type.Equality

Methods

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

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

Ord (a :~~: b) 
Instance details

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