Document how equality-bearing constructors are promoted in Core
In D4728, Simon was utterly baffled as to how one could promote the
MkT constructor in:
data T a where MkT :: (a ~ Int) => T a
Richard knows the inner machinations of how this works (including what coercions are used in the Core that
'MkT desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.