#9123: Need for higher kinded roles -------------------------------------+------------------------------------ Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): The question, as I see it, is this: If we know `(Rep m, Coercible a b)` can we derive `Coercible (s -> m (a, s)) (s -> m (b, s))`? We assume that the ''only'' way we can use `Rep` is in the following rule: `(Rep m, Coercible x y)` implies `Coercible (m x) (m y)`. Call that rule (*). Yes: 1. Decompose the `(->)` to get that we need to show `Coercible (m (a, s)) (m (b, s))`. 2. Use (*) to get that we need to show `Coercible (a, s) (b, s)`. 3. By the roles of `(,)`, this reduces to `Coercible a b`. 4. We are done by assumption. What have I missed? Where did the asymmetry come into play? I'm not saying that the current solver does this, but it seems possible. You may also want to see the original post in #9117 which may be of interest. (Much of the ensuing commentary is not as relevant.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler