#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Roles, | QuantifiedContexts 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 RyanGlScott): It turns out that my earlier comment: Replying to [comment:2 RyanGlScott]:
But to my knowledge, there's no reasoning principle which states that `f a ~R g a` implies `f ~R g`.
So far, we have only seen `Coercible` applied to types of kind `*`, but
Is a bit misleading. I've re-read the [http://www.seas.upenn.edu/~sweirich/papers/coercible-JFP.pdf Safe Zero- cost Coercions for Haskell] paper recently, and it turns out that Section 2.8 (Supporting higher-order polymorphism) pertains to this very topic: that is not sufficient to support all coercions that we might want. For example, consider a monad transformer such as
{{{#!hs data MaybeT m a = MaybeT (m (Maybe a)) }}}
and a newtype that wraps another monad, e.g.
{{{#!hs newtype MyIO a = MyIO (IO a) }}}
It is reasonable to expect that `Coercible (MaybeT MyIO a) (MaybeT IO
a)` can be derived. Using the lifting rule for `MaybeT`, this requires `Coercible MyIO IO` to hold. Therefore, for a `newtype` declaration as the one above, GHC will //η//-reduce the unwrapping rule to say `Coercible IO MyIO` instead of `Coercible (IO a) (MyIO a)`. Using symmetry, this allows us to solve `Coercible (MaybeT MyIO a) (MaybeT IO a)`. Alas, that is the //only// discussion of eta-reducing unwrapping rules that I can find in the entire paper, as it doesn't appear to be brought up again at any point. But this would definitely explain why you can construct a `Coercion (EITHER USD) (Either Int)` with relative ease. Now it is clear to me why you still can't derive `Coercible Identity (Compose Identity Identity)` from `Coercible (Identity a) (Compose Identity Identity a)`. The reason is because you'd have to be able to //η//-reduce this unwrapping rule: {{{#!hs Coercible (Compose f g a) (f (g a)) }}} But there is no way to //η//-reduce the `a` from `f (g a)`, so GHC evidently does not attempt this. So I'm inclined to label this as not-a-bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler