#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): Here, we need more assumptions. We have to assume an instance `Rep p` and an instance `Rep (p a)`. (We need it only for the `a` in question, though there would almost certainly be an axiom asserting `forall a. Rep (p a)`.) So, we assume `(Rep p, Rep (p a), Rep f, Coercible a b)` and wish to prove `Coercible (p a (f (F p f a))) (p b (f (F p f b)))`. We would be doing this in the context of an instance declaration for `Rep (F p f)`, so we can assume that, too. 1. Use transitivity to break our goal down to two sub-goals: `Coercible (p a (f (F p f a))) (p a (f (F p f b)))` and `Coercible (p a (f (F p f b))) (p b (f (F p f b)))`. 2. First sub-goal `Coercible (p a (f (F p f a))) (p a (f (F p f b)))`: a. Use rule (*) to break the goal down to `Rep (p a)` and `Coercible (f (F p f a)) (f (F p f b))`. The first of these is solved by assumption. b. Use rule (*) to get `Rep f` and `Coercible (F p f a) (F p f b)`. The first of these is solved by assumption. c. Use rule (*) to get `Rep (F p f)` and `Coercible a b`. Both are solved by assumption. 3. Second sub-goal `Coercible (p a (f (F p f b))) (p b (f (F p f b)))`: a. Use the #9117 eta rule to reduce the goal to `Coercible (p a) (p b)`. b. Use rule (*) to reduce the goal to `(Rep p, Coercible a b)`. c. Done by assumption. I'm not necessarily saying that the constraint solver is up to this task without help (that is, user annotations or other assistance), but `Rep` with rule (*) seems to be able to support the derivation once found. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler