[GHC] #14362: Allow: Coercing (a:~:b) to (b:~:a)
GHC
ghc-devs at haskell.org
Tue Oct 17 22:43:48 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 Iceland_jack):
But what is the most general type of `convert Refl = Refl`?
We cannot write
{{{#!hs
-- Could not deduce: a' ~ b'
-- from the context: a ~ b
convert :: (a :~: b) -> (a' :~: b')
convert Refl = Refl
}}}
note how type checking this depends on the ‘underlying constraint’ of
`(:~:)`: `(~)`.
We have to be deduce `a' ~ b'` from the given context `a ~ b`, which is
this?
{{{#!hs
convert :: ((a~b) => (a'~b')) => (a :~: b) -> (a' :~: b')
convert Refl = Refl
}}}
so I would expect `coerce` to have that type.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14362#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list