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 representational equality (`Coercion`

).

*Since: 4.7.0.0*

# Documentation

data Coercion a b where Source

Representational equality. If `Coercion a b`

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

has the same underlying representation as the type `b`

.

To use this equality in practice, pattern-match on the `Coercion a b`

to get out
the `Coercible a b`

instance, and then use `coerce`

to apply it.

*Since: 4.7.0.0*

Category k (Coercion k) Source | |

TestCoercion k (Coercion k a) Source | |

Coercible k a b => Bounded (Coercion k a b) Source | |

Coercible k a b => Enum (Coercion k a b) Source | |

Eq (Coercion k a b) Source | |

(Coercible * a b, Data a, Data b) => Data (Coercion * a b) Source | |

Ord (Coercion k a b) Source | |

Coercible k a b => Read (Coercion k a b) Source | |

Show (Coercion k a b) Source |

coerceWith :: Coercion a b -> a -> b Source

Type-safe cast, using representational equality

trans :: Coercion a b -> Coercion b c -> Coercion a c Source

Transitivity of representational equality

repr :: (a :~: b) -> Coercion a b Source

Convert propositional (nominal) equality to representational equality

class TestCoercion 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.

testCoercion :: f a -> f b -> Maybe (Coercion a b) Source

Conditionally prove the representational equality of `a`

and `b`

.

TestCoercion k (Coercion k a) Source | |

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