#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