#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): Reminder {{{ data Coercion a b where Coercion :: Coercible a b => Coercion a b data a :~: b where Refl :: a :~: a }}} So you want to be able to prove {{{ [W] (a :~: b) ~R# (b :~: a) [W] Coercible a b ~R# Coercible b a }}} Once could imagine special cases in the compiler, these are really perfectly ordinary data type declarations. What makes these representational type equalities true? Well, representationally speaking * `Refl :: (a ~# b) => a :~: b` has no represented value arguments. I suppose that for such types it's true that `(a :~: b) ~R# (c :~: d)` for any `a, b, c, d`. Is that right? Let's think about that first; I expect that once we figure this one out, `Coercible` will follow. Richard? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler