[GHC] #14362: Allow: Coercing (a:~:b) to (b:~:a)

[GHC]

#14362: Allow: Coercing (a:~:b) to (b:~:a)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  roles
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Replying to [comment:9 simonpj]:
 > * Is `(a :~: b) ~R# (b :~: a)` sound?

 You have described in your comment a new specification for
 representational equality: that two types are representationally equal
 when they are isomorphic and have identical runtime representations. It's
 too bad we never said that in the paper, because I agree with that
 specification. The paper then describes an incomplete "implementation" of
 that specification in its rules for representational equality. This is not
 the only source of incompleteness. See Appendix A.1 of
 [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1013&context=compsci_pubs
 the extended version of the original ICFP paper].

 So, to your question: Is such a thing sound? It would appear to be so,
 yes. But until we have a full theory that allows such a coercion without
 breaking something else, I can't be sure.

 > * And if so, what would be its evidence?

 We don't have any representation. And you're right that even if we had
 newtype-GADTs (which would give a new challenge to the Constraint-vs-Type
 debate, because they're somewhat the converse of newtype-classes), we
 couldn't pull this off. (I was wrong on this point, above.) The question
 is whether `(a ~# b) ~# (b ~# a)`. Right now, the answer is "no" because
 we can decompose `(~#)`. However, Stephanie's new theory ''can'' handle
 such things, because it was designed not to be able to decompose `(~#)`.
 I'm not intimately familiar with that end of her work, though. (In
 particular, I know it's forward-compatible with these ideas, but I don't
 know whether this end of the theory has been worked out in detail.)

 My bottom line: GHC's notion of representational equality is useful, but
 still quite limited. There are lots of ways of expanding it. This is one
 of them.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14362#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler