[Haskell-cafe] Generalizing "unlift" functions with monad-control

[Erik Hesselink]

Hi Michael,

The problem seems to be that the constraint you want isn't (b ~ StT t
b) for some specific b, you want (forall b. b ~ StT t b). It's not
possible to say this directly, but after some trying I got something
ugly that works. Perhaps it can be the inspiration for something
nicer?

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.Trans.Control
import Control.Monad.Trans.Reader

newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }

newtype ForallStId t = ForallStId (forall a. StTEq t a)

data StTEq (t :: (* -> *) -> * -> *) a where
  StTEq :: a ~ StT t a => StTEq t a

askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))
askRun = liftWith (return . Unlift)

askRunG :: forall t m.
           ( MonadTransControl t
           , Monad m
           )
        => ForallStId t -> t m (Unlift t)
askRunG x = liftWith $ \runT ->
  return $ Unlift ( (case x of ForallStId (StTEq :: StTEq t b) ->
runT) :: forall b n. Monad n => t n b -> n b )

askRun' :: Monad m => ReaderT r m (Unlift (ReaderT r))
askRun' = askRunG (ForallStId StTEq)

The constraints package allows you to define Forall constraints, but
that needs something of kind (* -> Constraint) and I can't figure out
how to get something like (b ~ StT t b) in that form: we don't have
'data constraints'.

Hope this helps you along, and please let me know if you find a nicer
way to do this.

Regards,

Erik

On Mon, Mar 30, 2015 at 7:33 AM, Michael Snoyman <michael at snoyman.com> wrote:
> I'm trying to extract an "unlift" function from monad-control, which would
> allow stripping off a layer of a transformer stack in some cases. It's easy
> to see that this works well for ReaderT, e.g.:
>
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE TypeFamilies #-}
> import Control.Monad.Trans.Control
> import Control.Monad.Trans.Reader
>
> newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }
>
> askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))
> askRun = liftWith (return . Unlift)
>
> The reason this works is that the `StT` associated type for `ReaderT` just
> returns the original type, i.e. `type instance StT (ReaderT r) m a = a`. In
> theory, we should be able to generalize `askRun` to any transformer for
> which that applies. However, I can't figure out any way to express that
> generalized type signature in a way that GHC accepts it. It seems like the
> following should do the trick:
>
> askRunG :: ( MonadTransControl t
>            , Monad m
>            , b ~ StT t b
>            )
>         => t m (Unlift t)
> askRunG = liftWith (return . Unlift)
>
> However, I get the following error message when trying this:
>
> foo.hs:11:12:
>     Occurs check: cannot construct the infinite type: b0 ~ StT t b0
>     The type variable ‘b0’ is ambiguous
>     In the ambiguity check for the type signature for ‘askRunG’:
>       askRunG :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) b.
>                  (MonadTransControl t, Monad m, b ~ StT t b) =>
>                  t m (Unlift t)
>     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
>     In the type signature for ‘askRunG’:
>       askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =>
>                  t m (Unlift t)
>
> Adding AllowAmbiguousTypes to the mix provides:
>
> foo.hs:17:30:
>     Could not deduce (b1 ~ StT t b1)
>     from the context (MonadTransControl t, Monad m, b ~ StT t b)
>       bound by the type signature for
>                  askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =>
>                             t m (Unlift t)
>       at foo.hs:(12,12)-(16,25)
>       ‘b1’ is a rigid type variable bound by
>            the type forall (n1 :: * -> *) b2.
>                     Monad n1 =>
>                     t n1 b2 -> n1 (StT t b2)
>            at foo.hs:1:1
>     Expected type: Run t -> Unlift t
>       Actual type: (forall (n :: * -> *) b. Monad n => t n b -> n b)
>                    -> Unlift t
>     Relevant bindings include
>       askRunG :: t m (Unlift t) (bound at foo.hs:17:1)
>     In the second argument of ‘(.)’, namely ‘Unlift’
>     In the first argument of ‘liftWith’, namely ‘(return . Unlift)’
>
> I've tested with both GHC 7.8.4 and 7.10.1. Any suggestions?
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>