base-compat-batteries-0.11.1: base-compat with extra batteries
Safe HaskellTrustworthy
LanguageHaskell98

Data.Type.Equality.Compat

Synopsis
  • data (a :: k) :~: (b :: k) where
  • class a ~# b => (a :: k0) ~~ (b :: k1)
  • data (a :: k1) :~~: (b :: k2) where
  • 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
  • castWith :: (a :~: b) -> a -> b
  • gcastWith :: forall k (a :: k) (b :: k) r. (a :~: b) -> (a ~ b => r) -> r
  • apply :: forall k1 k2 (f :: k1 -> k2) (g :: k1 -> k2) (a :: k1) (b :: k1). (f :~: g) -> (a :~: b) -> f a :~: g b
  • 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
  • class TestEquality (f :: k -> Type) where
  • type family (a :: k) == (b :: k) :: Bool where ...

The equality types

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

Constructors

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

TestCoercion ((:~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion 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]

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

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

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

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

TestCoercion ((:~~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion 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]

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

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

Working with equality

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 #

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

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

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

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 #

Inferring equality from other types

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

Methods

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

Instances

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

Defined in Data.Typeable.Internal

Methods

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

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

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

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

Defined in Data.Functor.Compose

Methods

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

Boolean type-level equality

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