#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 Iceland_jack): In the syntax of #12045 (which I hope to continue working on soon), a fully explicit instance might look like: {{{#!hs instance forall k (r::k) (m::k -> Type). MonadCont (ContT @k r m) where callCC :: ((a -> ContT @k r m b) -> ContT @k r m a) -> ContT @k r m a callCC = callCC' }}} and if we wanted the current version for some reason as defined in [https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control-Monad- Cont-Class.html Control.Monad.Cont.Class] (which doesn't seem to have `PolyKinds` enabled) {{{#!hs instance forall (r::Type) (m::Type -> Type). MonadCont (ContT @Type r m) where callCC :: ((a -> ContT @Type r m b) -> ContT @Type r m a) -> ContT @Type r m a callCC = callCC' }}} This could be displayed in `:info`, possibly given some flag or hiding given some smart heuristic. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12418#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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): {{{#!hs instance MonadState s m => MonadState s (ContT @Type r m) }}} suffers the same sort of problem as the MonadCont instance, if you define it pointwise at @Type. If m and r are left underspecified kind wise and you go to invoke a `MonadState s ` operation, it has no reason to pick that instance, unless it can figure out `k = Type`, hence `m :: Type -> Type`, it won't discharge the head and go looking for `MonadState s m` from the body and use this instance. It'll just whine about a missing instance at an unknown kind. So if `m` is polykinded like `Proxy`, which has kind k -> *, but at * -> * is a perfectly legitimate monad (it is the unique-up-to-isomorphism terminal monad), then this no longer monomorphizes m to kind * -> * to go look for this possible instance. The compiler doesn't know if you doesn't know someone won't make up some completely different instance like: {{{#!hs instance MonadState () (ContT @Whatever r m) where get = return () put () = return () }}} pointwise at another kind. This 'can't do the same sort of lifting as the typical MonadState, so it really doesn't have any place being defined on this data type and any such instance will necessarily be an orphan. As you note Functor, Applicative, Monad all work fine, because really if you look at ContT the fact that m and r exist as separate entities doesn't matter to those instances at all, those are just the basic `Cont r'` instances instantiated at `r' = m r`. They never use 'm' to do any work, and just teeat `m r` as an opaque blob. Once you start lifting monad transformer instances for things like MonadState, MonadWriter, etc. over `ContT r` then we need to know `m :: Type -> Type`, because we finally start interacting with the extra structure we've given our CPS'd result type. You get a slightly more general callCC at the expense of screwing up inference for every monad transformer instance, that can only be taken advantage of to make instances that act at different kinds inconsistently with the instances that are already in place. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12418#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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):

So perhaps CLC should do as you implicitly suggest?

I very deliberately didn't suggest that. I actually pointed it out as a sign of quite how bad it would be to do this. It would affect every single user defined monad transformer type that happens to lift over `ContT` as well. Not just code in `transformers`. This would fix the inference for the handful of instances `transformers` defines, but not for every other package out there that builds on top. For the record, I'm pretty strongly against this proposal from the standpoint of what it does in practice to what is currently a very stable part of our ecosystem. A single combinator gets a slightly more general signature, but the result is that the `ContT` type becomes worse at its original stated job as serving as a monad transformer. Given that it comes from `Control.Monad.Trans.Cont`, it seems it is well placed for the current design. The replacement doesn't actually offer any new uses. If you use it at the new kind almost none of the existing instances are useful and they in fact actively get in the way of anything more generic you might want by overlapping these hypothetical instances for hypothetical classes we don't have. This is a situation where a different type offered by a different library is in order. The compromise of adding a ton of constraints is worse than the compromise of simply not PolyKinding the data type in the first place, as it impacts both the existing users badly _and_ whatever potential users the more general form woudl have, as if you wanted to use the power to do something more interesting the instance of these blanket instances would likely prevent you from doing it anyways. If you want the power of this proposal you can get it by just using `Cont (IdentityT m r) a` out of the box today. It has every single one of the admissible instances that would be let through by this proposal. `IdentityT` is already PolyKinded, but doesn't cause these sorts of problems. I'm inclined to close this out until the unlikely day when there is a library out there that shows the change, and people out there who see a need to use it. @Iceland_jack, I'm sorry, but would you object terribly strongly to that resolution? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12418#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12418: Make `MonadCont (ContT r m)` polykinded (r::k), (m::k -> Type) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: invalid | 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: | -------------------------------------+------------------------------------- Changes (by ekmett): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12418#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler