Data.Constraint.Deferrable

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.

Kind heterogeneous propositional equality. Like :~:, a :~~: b is inhabited by a terminating value if and only if a is the same type as b.