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