[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):

 I'm not really sure what this ticket is about. The relation `~R#` defines
 representational equality. The rules for this are written in the Coercible
 paper. There are several other tickets floating about talking about things
 that are provably `~R#`, but that GHC's solver can't figure it out. This
 ticket is different, though: it seems to propose new rules for `~R#`.

 (Note: `Coercible` is defined as

 {{{#!hs
 class a ~R# b => Coercible a b
 instance a ~R# b => Coercible a b
 }}}

 )

 According to the rules for `~R#`, we don't have `(a :~: b) ~R# (b :~: a)`:
 the parameters to `:~:` both have a nominal role. (Note that role
 inference looks at constraints as well as other data members, so the `a ~
 b` constraint in the type of `Refl` is what induces the nominal roles.)

 It's conceivable that we could have newtype-GADTs, like

 {{{#!hs
 newtype a :~: b where
   Refl :: a ~ b => a :~: b
 }}}

 With a newtype-GADT, we could imagine forming `(a :~: b) ~R# (b :~: a)` by
 unwrapping, using `sym` and then wrapping using the newtype constructor.
 (I'm unsure how the solver would work here... but at least it's possible
 in Core.) Of course, we don't have newtype-GADTs.

 And I'm afraid I don't understand what's going on in comment:3 and
 comment:4. How do these ideas relate to the definition of `~R#`?

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