base-compat-0.13.1: A compatibility layer for base
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Type.Equality.Compat

Documentation

class a ~# b => (a :: k0) ~~ (b :: k1) #

class a ~# b => (a :: k) ~ (b :: k) #

type family (a :: k) == (b :: k) :: Bool where ... #

Equations

(f a :: k2) == (g b :: k2) = (f == g) && (a == b) 
(a :: k) == (a :: k) = 'True 
(_1 :: k) == (_2 :: k) = 'False 

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 #

data (a :: k) :~: (b :: k) where #

Constructors

Refl :: forall {k} (a :: k). 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) #

(a ~ b, Data a) => 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 #

class TestEquality (f :: k -> Type) where #

Methods

testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #

Instances

Instances details
TestEquality SNat 
Instance details

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #

TestEquality SChar 
Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) #

TestEquality SSymbol 
Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) #

TestEquality (TypeRep :: k -> Type) 
Instance details

Defined in Data.Typeable.Internal

Methods

testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: 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) #

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

TestEquality f => TestEquality (Compose f g :: k2 -> Type) 
Instance details

Defined in Data.Functor.Compose

Methods

testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) #

sym :: forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a #

trans :: forall {k} (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c #

apply :: forall {k1} {k2} (f :: k1 -> k2) (g :: k1 -> k2) (a :: k1) (b :: k1). (f :~: g) -> (a :~: b) -> f a :~: g b #

castWith :: (a :~: b) -> a -> b #

gcastWith :: forall {k} (a :: k) (b :: k) r. (a :~: b) -> (a ~ b => r) -> r #

inner :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> a :~: b #

outer :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> f :~: g #