#9123: Need for higher kinded roles -------------------------------------+------------------------------------- Reporter: simonpj | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Project (more Type of failure: | than a week) None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:30 simonpj]:
You want to ''infer'' a rather complicated context. I don't know how to do that.
Sure you do! Currently, the code in !TcDeriv instructs the solver to try to reduce certain constraints. This reduction results in an unsolved implication constraint -- exactly the one we need to quantify over. The !TcDeriv code, at this point, extracts out the flat (er... now called ''simple'') constraints, checks to see if they're exotic, and then reports an error if there are any exotic simple constraints or if there are any leftover implication constraints. Currently, there's a leftover implication, and so we report an error. If, instead, we quantified over the leftover implication, we'd be done, with an inferred implication constraint. A separate question is whether or not this is desirable from a user's standpoint. `deriving` quite rightly restricts what it will quantify over. And implication constraints seem quite exotic. We could, though, say that implication constraints aren't exotic. Or, we could bake in the particular implication constraint `(forall a b. Coercible a b => Coercible (m a) (m b))`, recognize that, rewrite it to use Simon's type synonym `RepArg1 m`, and then it doesn't seem so exotic after all. That's terribly hacky, but it just might be useful enough to do. Or, we could punt and require users to write the constraint when they want it -- the error message will give them guidance. I don't have a strong opinion in any direction here. It is worth noting that, if `join :: m (m a) -> m a` is in `Monad`, most GNDs of `Monad` would work today. The ones that trip up are when the newtype wraps a monad transformer. That's a common-enough case that we don't want to make it impossible, but a rare enough case that I'm OK with making it annoying, if we can't do better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9123#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler