#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 simonpj):
I'm not really sure what this ticket is about.
It's about the following questions: * Is `(a :~: b) ~R# (b :~: a)` sound? * And if so, what would be its evidence? Remember we are talking only of when a value of type `(a :~: b)` can be coerced to one of type `(b :~: a)`, ust as we speak of coercing a value of type `[Int]` to one of type `[Age]`. Curiuosly, the paper doesn't actually articulate the circumstances under which such a coercion is OK -- instead it describes role inference. My sanity check (again not articulated explicitly in the paper) is this: it's sound to coerce a value of type `t1` into a value of type `t2`, and vice versa, if * I could write code of type `t1 -> t2` and `t2 -> t1` * The runtime representations of the two are identical Both properties hold for `(a :~: b)` and `(b :~: a)`, regardless of `a` and `b`, don't they? So I claim that `(a :~: b) ~R# (b :~: a)` is sound. But `(a :~: a) ~R# (a :~: b)` obviously must ''not'' hold, else I could write {{{ good :: forall a. a :~: a good = Refl bad :: forall a b. a -> b bad x = case (coerce (good @ a)) :: a :~: b of Refl -> x }}} (And, returning to the sanity check, I could not write a function of type `(a :~: a) -> (a :~: b)`.) So how ''could'' we prove `(a :~: b) ~R# (b :~: a)`? We have two ways to prove `Coercible`: * Decomposition on `(T ts1) ~R# (T ts2)`, using the roles of T. That isn't going to work here because it loses the crucial connection bettween `ts1` and `ts2`. * Newtype-unwrapping on `(N ts1) ~R# t2`. And (you are way ahead of me as usual), we could do that here if only `:~:` was a newtype. But, even leaving aside that we don't have newtype GADTs (I think we could maybe fix that), after decomposing both sides we'd have `(a ~ b) ~R# (b ~ a)`. And now we are back to the original problem: what would be the evidence for such an equality? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler