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

GHC ghc-devs at haskell.org
Thu Jul 21 18:21:03 UTC 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


More information about the ghc-tickets mailing list