GEq package:prim-uniq

A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.

Produce a witness of type-equality, if one exists. A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:

extract :: GEq tag => tag a -> DSum tag -> Maybe a
extract t1 (t2 :=> x) = do
Refl <- geq t1 t2
return x

Or in a list comprehension:

extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]

(Making use of the DSum type from Data.Dependent.Sum in both examples)