base-compat-batteries-0.11.1: base-compat with extra batteries

Safe Haskell | Trustworthy
Language | Haskell98

Data.Type.Equality.Compat

Contents

- The equality types
- Working with equality
- Inferring equality from other types
- Boolean type-level equality

Synopsis

- data (a :: k) :~: (b :: k) where
  - Refl :: forall k (a :: k). a :~: a
- class a ~# b => (a :: k0) ~~ (b :: k1)
- data (a :: k1) :~~: (b :: k2) where
  - HRefl :: forall k1 (a :: k1). a :~~: a
- 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
  - testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- 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) #

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