Safe Haskell	Trustworthy
Language	Haskell2010

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

Category ((:~~:) :: k -> k -> Type)
Instance details Defined in Control.Category Methods id :: forall (a :: k). a :~~: a (.) :: forall (b :: k) (c :: k) (a :: k). (b :~~: c) -> (a :~~: b) -> a :~~: c
TestCoercion ((:~~:) a :: k -> Type)
Instance details Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b)
TestEquality ((:~~:) a :: k -> Type)
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b)
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b)
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) toConstr :: (a :~~: b) -> Constr dataTypeOf :: (a :~~: b) -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: 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