<div dir="ltr">Sorry for only just discovering this thread now. A lot of this discussion is in fact moot, since (:~~:) already is in base! Specifically, it's landing in Data.Type.Equality [1] in the next version of base (bundled with GHC 8.2). Moreover, it's constructor is named HRefl, so your wish has been granted ;)<div><br></div><div>As for why it's being introduced in base, it ended up being useful for the new Type-indexed Typeable that's also landing in GHC 8.2. In particular, the eqTypeRep function [2] must return heterogeneous equality (:~~:), not homogeneous equality (:~:), since it's possible that you'll compare two TypeReps with different kinds.<br><div><div><br></div><div>Ryan S.</div><div>-----</div><div>[1] <a href="http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37">http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37</a></div></div></div><div>[2] <a href="http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311">http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311</a></div></div>