Type equality in GADT/TypeFamily context

A follow-up on my prior comment.

Data.Type.Equality.==

The reason for its weird implementation is discussed in this comment.

Rather than simplifying it, the better course of action should be to use/provide:

equal :: a :~: b -> (a == b) :~: True
equal Refl = unsafeCoerce (Refl @True)

apart

I didn’t do enough testing. There’s no issue with this primitive in principle, but in practice the GHC.TypeLits.decide* functions don’t actually provide legitimate inequalities. apart refuses to be fooled and explodes.

This can be fixed, so I’ve made an issue of it.