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.