There's another version of heterogeneous equality that takes its arguments in the other order. I'm not sure if this is generally useful enough to want to include. -- (:~~:) :: forall j k. j -> k -> * data OtherEquality :: forall j. j -> forall k. k -> Type where OtherRefl :: OtherEquality a a On Mon, Jul 10, 2017 at 11:24 AM, Ryan Scott <ryan.gl.scott@gmail.com> wrote:
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.
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries