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 ;) 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. Ryan S. ----- [1] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a... [2] http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5f718d18fcaa66a...