coerce package:equational-reasoning

coerce :: (a :=: b) -> f a -> f b
equational-reasoning Proof.Equational
Deprecated: Use coerceInner instead
coerce' :: (a :=: b) -> a -> b
equational-reasoning Proof.Equational
Coercion for identity types.
coerceInner :: (a :=: b) -> f a -> f b
equational-reasoning Proof.Equational
Type coercion. coerce is using unsafeCoerce a. So, please, please do not provide the undefined as the proof. Using this function instead of pattern-matching on equality proof, you can reduce the overhead introduced by run-time proof.