Re: Heterogeneous equality into base?

I also agree that we should keep HRefl a distinct name, and moreover, we should keep :~: and :~~: as distinct datatypes. I'm also on-board with the idea that we should introduce a separate Data.Type.Equality.Hetero module that reexports :~~: and defines heterogeneous counterparts for sym, trans, etc. from Data.Type.Equality. I don't have a strong opinion on how they should be named (e.g., sym vs. hsym). Ryan S.