#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): But I don't want the most general type of `convert`! The general principle of `Coercible` is that it simply automates what you could do by hand. E.g {{{ newtype Age = MkAge Int convert :: [Int] -> [Age] convert xs = map MkAge xs }}} And back. So we can reasonably claim `Coercible [Age] [Int]`. It's the same with `Coercible (a :~: b) (b :~: a)`, which is what you asked for. I can do it by hand (with `convert`); using `coerce` just automates it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14362#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler