#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 Iceland_jack): My goal was to specialize `id1F`, `id2F` to {{{#!hs id1F :: F (Compose Identity Identity) a a id2F :: F Identity a a }}} such that `F f` can be made a `Category` (less useful than I originally thought). This works with Adam's code (on 8.0.1) {{{#!hs data F' f a b where MkF' :: Coercible (f b) (f' b) => (a -> f' b) -> F' f a b id1F :: Coercible (f a) a => F' f a a id1F = MkF' Identity a :: F' Identity a a a = id1F b :: F' (Compose Identity Identity) a a b = id1F }}} which cannot be made into a `Category` because the representation of `a` leaks into the signature. Replying to [comment:2 RyanGlScott]:
I think you might be inclined to believe that because `Identity a` is representationally equal to `(Compose Identity Identity) a`, that GHC can conclude that `Identity` is representationally equal to `Compose Identity Identity`.
Yes that's right
But to my knowledge, there's no reasoning principle which states that `f a ~R g a` implies `f ~R g`.
Can there not be some kind of pseudo rule? {{{#!hs instance (forall xx. f xx `Coercible` g xx) => Coercible f g }}} I don't understand the purpose + rules for polykinded `Coercible` {{{#!hs newtype MAYBE a = M (Maybe a) newtype EITHER a b = E (Either a b) newtype PAIR a b = P ((,) a b) works :: Coercion Maybe MAYBE works = Coercion works2 :: Coercion PAIR (,) works2 = Coercion -- ! fails :: Coercion Either EITHER fails = Coercion }}} `coerce` and `coerceWith` only work with `Type`s.. maybe it is used to assist the constraint solver in ways I don't get -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14317#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler