[GHC] #12418: Make `MonadCont (ContT r m)` polykinded (r::k), (m::k -> Type)

21 Jul 2016


      #12418: Make `MonadCont (ContT r m)` polykinded (r::k), (m::k -> Type)
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Core           |           Version:  8.0.1
  Libraries                          |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 == 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:

 {{{#!hs
 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
 }}}
--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12418
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler