Data.Type.Coercion

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.

Type-safe cast, using representational equality

Generalized form of type-safe cast using representational equality

Symmetry of representational equality

Transitivity of representational equality

Convert propositional (nominal) equality to representational equality

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.