Make `MonadCont (ContT r m)` polykinded (r::k), (m::k -> Type)

Issue ==

The current MonadCont (ContT r m) instance seems to have r::Type and m::Type -> Type.

While this is accepted

>>> :t callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a
callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a
  :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a

this gets rejected

>>> :set -XPolyKinds 
>>> :t callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a

<interactive>:1:1: error:
    • No instance for (MonadCont (ContT r1 m1))
        arising from a use of ‘callCC’
    • In the expression:
          callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a

and this doesn't reduce

>>> :t callCC @(ContT _ _)
callCC @(ContT _ _)
  :: MonadCont (ContT t t1) =>
     ((a -> ContT t t1 b) -> ContT t t1 a) -> ContT t t1 a

the kinds must be specified

>>> :t callCC @(ContT (_::Type) _)
callCC @(ContT (_::Type) _)
  :: ((a -> ContT t t1 b) -> ContT t t1 a) -> ContT t t1 a

Solution

This is unfortunate since since callCC can be kind polymorphic:

newtype ContT' r m a = ContT' { runContT' :: (a -> m r) -> m r }

callCC' :: forall k a (r :: k) (m :: k -> Type) b. 
           ((a -> ContT' r m b) -> ContT' r m a) 
        -> ContT' r m a
callCC' f = ContT' $ \ c -> runContT' (f (\ x -> ContT' $ \ _ -> c x)) c

instance forall k (r::k) (m::k -> Type). MonadCont (ContT' r m) where
  callCC = callCC'

this works now

>>> :t callCC @(ContT' _ _)
callCC @(ContT' _ _)
  :: forall k (t :: k) (t1 :: k -> *) a b.
     ((a -> ContT' t t1 b) -> ContT' t t1 a) -> ContT' t t1 a 

>>> :t callCC :: ((a -> ContT' r m b) -> ContT' r m a) -> ContT' r m a
callCC :: ((a -> ContT' r m b) -> ContT' r m a) -> ContT' r m a
  :: forall k a (r :: k) (m :: k -> *) b.
     ((a -> ContT' r m b) -> ContT' r m a) -> ContT' r m a

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Core Libraries
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	ekmett
Operating system
Architecture