[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