[GHC] #14362: Allow: Coercing (a:~:b) to (b:~:a)
GHC
ghc-devs at haskell.org
Tue Oct 17 23:10:03 UTC 2017
#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
More information about the ghc-tickets
mailing list