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

Maintainer | libraries@haskell.org |

Stability | experimental |

Portability | not portable |

Safe Haskell | None |

Language | Haskell2010 |

Definition of propositional equality `(:~:)`

. Pattern-matching on a variable
of type `(a :~: b)`

produces a proof that `a ~ b`

.

*Since: 4.7.0.0*

- data a :~: b where
- sym :: (a :~: b) -> b :~: a
- trans :: (a :~: b) -> (b :~: c) -> a :~: c
- castWith :: (a :~: b) -> a -> b
- gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
- apply :: (f :~: g) -> (a :~: b) -> f a :~: g b
- inner :: (f a :~: g b) -> a :~: b
- outer :: (f a :~: g b) -> f :~: g
- class TestEquality f where
- testEquality :: f a -> f b -> Maybe (a :~: b)

- type family a == b :: Bool

# The equality type

data a :~: b 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: 4.7.0.0*

Category k ((:~:) k) | |

TestEquality k ((:~:) k a) | |

TestCoercion k ((:~:) k a) | |

Typeable (k -> k -> *) ((:~:) k) | |

(~) k a b => Bounded ((:~:) k a b) | |

(~) k a b => Enum ((:~:) k a b) | |

Eq ((:~:) k a b) | |

((~) * a b, Data a) => Data ((:~:) * a b) | |

Ord ((:~:) k a b) | |

(~) k a b => Read ((:~:) k a b) | |

Show ((:~:) k a b) |

# Working with equality

gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r Source

Generalized form of type-safe cast using propositional equality

inner :: (f a :~: g b) -> a :~: b Source

Extract equality of the arguments from an equality of a applied types

outer :: (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 where Source

This class contains types where you can learn the equality of two types
from information contained in *terms*. Typically, only singleton types should
inhabit this class.

testEquality :: f a -> f b -> Maybe (a :~: b) Source

Conditionally prove the equality of `a`

and `b`

.

TestEquality k ((:~:) k a) |

# Boolean type-level equality

type family a == b :: Bool infix 4 Source

A type family to compute Boolean equality. Instances are provided
only for *open* kinds, such as `*`

and function kinds. Instances are
also provided for datatypes exported from base. A poly-kinded instance
is *not* provided, as a recursive definition for algebraic kinds is
generally more useful.

type (==) Bool a b | |

type (==) Ordering a b | |

type (==) * a b | |

type (==) Nat a b | |

type (==) Symbol a b | |

type (==) () a b | |

type (==) [k] a b | |

type (==) (Maybe k) a b | |

type (==) (k -> k1) a b | |

type (==) (Either k k1) a b | |

type (==) ((,) k k1) a b | |

type (==) ((,,) k k1 k2) a b | |

type (==) ((,,,) k k1 k2 k3) a b | |

type (==) ((,,,,) k k1 k2 k3 k4) a b | |

type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b | |

type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b | |

type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b | |

type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b | |

type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b | |

type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b | |

type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b | |

type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b | |

type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b | |

type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b |