License | BSD-style (see the LICENSE file in the distribution) |
---|---|

Maintainer | libraries@haskell.org |

Stability | stable |

Portability | not portable |

Safe Haskell | Trustworthy |

Language | Haskell2010 |

## Synopsis

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

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

# The equality types

class a ~# b => (a :: k) ~ (b :: k) infix 4 Source #

Lifted, homogeneous equality. By lifted, we mean that it
can be bogus (deferred type error). By homogeneous, the two
types `a`

and `b`

must have the same kinds.

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

Lifted, heterogeneous equality. By lifted, we mean that it
can be bogus (deferred type error). By heterogeneous, the two
types `a`

and `b`

might have different kinds. Because `~~`

can
appear unexpectedly in error messages to users who do not care
about the difference between heterogeneous equality `~~`

and
homogeneous equality `~`

, this is printed as `~`

unless
`-fprint-equality-relations`

is set.

In `0.7.0`

, the fixity was set to `infix 4`

to match the fixity of `:~~:`

.

data (a :: k) :~: (b :: k) where infix 4 Source #

Propositional equality. If `a :~: b`

is inhabited by some terminating
value, then the type `a`

is the same as the type `b`

. To use this equality
in practice, pattern-match on the `a :~: b`

to get out the `Refl`

constructor;
in the body of the pattern-match, the compiler knows that `a ~ b`

.

@since base-4.7.0.0

#### Instances

Category ((:~:) :: k -> k -> Type) Source # | @since base-4.7.0.0 |

TestCoercion ((:~:) a :: k -> Type) Source # | @since base-4.7.0.0 |

Defined in GHC.Internal.Data.Type.Coercion | |

TestEquality ((:~:) a :: k -> Type) Source # | @since base-4.7.0.0 |

Defined in GHC.Internal.Data.Type.Equality | |

(a ~ b, Data a) => Data (a :~: b) Source # | @since base-4.7.0.0 |

Defined in GHC.Internal.Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source # toConstr :: (a :~: b) -> Constr Source # dataTypeOf :: (a :~: b) -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # | |

a ~ b => Bounded (a :~: b) Source # | @since base-4.7.0.0 |

a ~ b => Enum (a :~: b) Source # | @since base-4.7.0.0 |

Defined in GHC.Internal.Data.Type.Equality succ :: (a :~: b) -> a :~: b Source # pred :: (a :~: b) -> a :~: b Source # toEnum :: Int -> a :~: b Source # fromEnum :: (a :~: b) -> Int Source # enumFrom :: (a :~: b) -> [a :~: b] Source # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source # | |

a ~ b => Read (a :~: b) Source # | @since base-4.7.0.0 |

Show (a :~: b) Source # | @since base-4.7.0.0 |

Eq (a :~: b) Source # | @since base-4.7.0.0 |

Ord (a :~: b) Source # | @since base-4.7.0.0 |

Defined in GHC.Internal.Data.Type.Equality |

data (a :: k1) :~~: (b :: k2) where infix 4 Source #

Kind heterogeneous propositional equality. Like `:~:`

, `a :~~: b`

is
inhabited by a terminating value if and only if `a`

is the same type as `b`

.

@since base-4.10.0.0

#### Instances

Category ((:~~:) :: k -> k -> Type) Source # | @since base-4.10.0.0 |

TestCoercion ((:~~:) a :: k -> Type) Source # | @since base-4.10.0.0 |

Defined in GHC.Internal.Data.Type.Coercion | |

TestEquality ((:~~:) a :: k -> Type) Source # | @since base-4.10.0.0 |

Defined in GHC.Internal.Data.Type.Equality | |

(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) Source # | @since base-4.10.0.0 |

Defined in GHC.Internal.Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) Source # toConstr :: (a :~~: b) -> Constr Source # dataTypeOf :: (a :~~: b) -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source # gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source # | |

a ~~ b => Bounded (a :~~: b) Source # | @since base-4.10.0.0 |

a ~~ b => Enum (a :~~: b) Source # | @since base-4.10.0.0 |

Defined in GHC.Internal.Data.Type.Equality succ :: (a :~~: b) -> a :~~: b Source # pred :: (a :~~: b) -> a :~~: b Source # toEnum :: Int -> a :~~: b Source # fromEnum :: (a :~~: b) -> Int Source # enumFrom :: (a :~~: b) -> [a :~~: b] Source # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # | |

a ~~ b => Read (a :~~: b) Source # | @since base-4.10.0.0 |

Show (a :~~: b) Source # | @since base-4.10.0.0 |

Eq (a :~~: b) Source # | @since base-4.10.0.0 |

Ord (a :~~: b) Source # | @since base-4.10.0.0 |

Defined in GHC.Internal.Data.Type.Equality compare :: (a :~~: b) -> (a :~~: b) -> Ordering Source # (<) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (<=) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (>) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (>=) :: (a :~~: b) -> (a :~~: b) -> Bool Source # |

# Working with equality

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

Transitivity of equality

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

Generalized form of type-safe cast using propositional equality

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

Apply one equality to another, respectively

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

Extract equality of the arguments from an equality of applied types

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

Extract equality of type constructors from an equality of applied types

# Inferring equality from other types

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

This class contains types where you can learn the equality of two types
from information contained in *terms*.

The result should be `Just Refl`

if and only if the types applied to `f`

are
equal:

testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b

Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:

testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y

isJust (testEquality x y) = x == y

Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.

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

Conditionally prove the equality of `a`

and `b`

.

#### Instances

TestEquality SNat Source # | @since base-4.18.0.0 |

Defined in GHC.Internal.TypeNats | |

TestEquality SChar Source # | @since base-4.18.0.0 |

Defined in GHC.Internal.TypeLits | |

TestEquality SSymbol Source # | @since base-4.18.0.0 |

Defined in GHC.Internal.TypeLits | |

TestEquality (TypeRep :: k -> Type) Source # | |

Defined in GHC.Internal.Data.Typeable.Internal | |

TestEquality ((:~:) a :: k -> Type) Source # | @since base-4.7.0.0 |

Defined in GHC.Internal.Data.Type.Equality | |

TestEquality ((:~~:) a :: k -> Type) Source # | @since base-4.10.0.0 |

Defined in GHC.Internal.Data.Type.Equality |