Data.Singletons.Decide

Members of the SDecide "kind" class support decidable equality. Instances of this class are generated alongside singleton definitions for datatypes that derive an Eq instance.

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.

Uninhabited data type

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

A suitable default implementation for testEquality that leverages SDecide.

A suitable default implementation for testCoercion that leverages SDecide.