#12418: Make `MonadCont (ContT r m)` polykinded (r::k), (m::k -> Type) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: 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 ekmett): I have some rather large concerns about the fact that now selecting the sensible existing monad transformer instances becomes quite brittle. {{{#!hs instance [safe] forall r (m :: Type -> Type). MonadCont (ContT @Type r m) }}} requires `k :: Type` to be figured out before it'll be selected. So you get the ability to define your own `callCC` and other operations where `(r :: MyKind)` and `(m :: MyKind -> *)` by making other instances pointwise at particular kinds, but now if you are polymorphic enough, you'll get "No instance" warnings that are completely opaque to the average user. The FlexibleInstance-style shape of the instance head here is a sign that inference will go to hell. If the instance was based on something like {{{#!hs instance k ~ Type => MonadCont (ContT @k r m) }}} then type inference for that particular instance could never blow up, at the expense of losing ability to co-opt callCC for some unrelated monad- transformer-like pipeline that worked on an entirely different kind that could never be made compatible with the way the rest of the MonadFoo classes lift over `m`, anyways. Attempting to use `callCC` with that sort of tweak would then force k = Type, and inference could proceed as usual. Of course even if we did do that, we just stuck one finger in the dyke. There are other leaks. e.g. What makes this instance any different than the behavior of `MonadState s` or `MonadReader e`? They all need `m :: Type -> Type`, so they'll _all_ have these inference woes, `Cont r m :: * -> *`, so they could be instances of `MonadState s` at any choice of kind k, but the lifting of `MonadState s` requires `m :: Type -> Type`, etc. So now attempting to call `get`, `ask`, etc. in a sufficiently polymorphic situation would run afoul of the same thing! It seems every one of those instances would need to adopt the same pattern. The fact that our behavior for any of the instances we use `ContT r m` at that exploit information about `m` is tied to m having kind `* -> *` makes this a mess, and that all the transformer instances become significantly harder to use makes me very nervous. User code that defines instances that lift over ContT won't exhibit the same care. The fact that the only thing we gain here seems to be the ability to define instances that relies on working pointwise completely differently at different kinds, and really tricky type errors for the kinds of users most ill equipped to handle them makes me think this probably isn't a good idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12418#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler