Refl package:gdp

A binary relation R is reflexive if, for all x, R(x, x) is true. The Reflexive r typeclass provides a single method, refl :: Proof (r x x), proving R(x, x) for an arbitrary x. Within the module where the relation R is defined, you can declare R to be reflexive with an empty instance:

-- Define a reflexive binary relation
data SameColor p q
instance Reflexive SameColor

Reflect an equality between x and y into a propositional equality between the types x and y.

newtype Bob = Bob Defn

bob :: Int ~~ Bob
bob = defn 42

needsBob :: (Int ~~ Bob) -> Int
needsBob x = the x + the x

isBob :: (Int ~~ name) -> Maybe (Proof (name == Bob))
isBob = same x bob

f :: (Int ~~ name) -> Int
f x = case reflectEq <$> isBob x of
Nothing   -> 17
Just Refl -> needsBob x x

A binary relation R is irreflexive if, for all x, R(x, x) is false. The Irreflexive r typeclass provides a single method, irrefl :: Proof (Not (r x x)), proving the negation of R(x, x) for an arbitrary x. Within the module where the relation R is defined, you can declare R to be irreflexive with an empty instance:

-- Define an irreflexive binary relation
newtype DifferentColor p q = DifferentColor Defn
type role DifferentColor nominal nominal
instance Irreflexive DifferentColor