<div dir="ltr">Those are some impressive type gymnastics :) Unfortunately, I still don't think I'm able to write the generic function the way I wanted to, so I'll be stuck with a typeclass. However, I may be able to provide your helper types/functions to make it easier for people to declare their own instances.<br></div><br><div class="gmail_quote">On Mon, Mar 30, 2015 at 10:42 PM Erik Hesselink <<a href="mailto:hesselink@gmail.com">hesselink@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Michael,<br>
<br>
The problem seems to be that the constraint you want isn't (b ~ StT t<br>
b) for some specific b, you want (forall b. b ~ StT t b). It's not<br>
possible to say this directly, but after some trying I got something<br>
ugly that works. Perhaps it can be the inspiration for something<br>
nicer?<br>
<br>
{-# LANGUAGE RankNTypes #-}<br>
{-# LANGUAGE KindSignatures #-}<br>
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
<br>
import Control.Monad.Trans.Control<br>
import Control.Monad.Trans.Reader<br>
<br>
newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }<br>
<br>
newtype ForallStId t = ForallStId (forall a. StTEq t a)<br>
<br>
data StTEq (t :: (* -> *) -> * -> *) a where<br>
  StTEq :: a ~ StT t a => StTEq t a<br>
<br>
askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))<br>
askRun = liftWith (return . Unlift)<br>
<br>
askRunG :: forall t m.<br>
           ( MonadTransControl t<br>
           , Monad m<br>
           )<br>
        => ForallStId t -> t m (Unlift t)<br>
askRunG x = liftWith $ \runT -><br>
  return $ Unlift ( (case x of ForallStId (StTEq :: StTEq t b) -><br>
runT) :: forall b n. Monad n => t n b -> n b )<br>
<br>
askRun' :: Monad m => ReaderT r m (Unlift (ReaderT r))<br>
askRun' = askRunG (ForallStId StTEq)<br>
<br>
The constraints package allows you to define Forall constraints, but<br>
that needs something of kind (* -> Constraint) and I can't figure out<br>
how to get something like (b ~ StT t b) in that form: we don't have<br>
'data constraints'.<br>
<br>
Hope this helps you along, and please let me know if you find a nicer<br>
way to do this.<br>
<br>
Regards,<br>
<br>
Erik<br>
<br>
On Mon, Mar 30, 2015 at 7:33 AM, Michael Snoyman <<a href="mailto:michael@snoyman.com" target="_blank">michael@snoyman.com</a>> wrote:<br>
> I'm trying to extract an "unlift" function from monad-control, which would<br>
> allow stripping off a layer of a transformer stack in some cases. It's easy<br>
> to see that this works well for ReaderT, e.g.:<br>
><br>
> {-# LANGUAGE RankNTypes #-}<br>
> {-# LANGUAGE TypeFamilies #-}<br>
> import Control.Monad.Trans.Control<br>
> import Control.Monad.Trans.Reader<br>
><br>
> newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }<br>
><br>
> askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))<br>
> askRun = liftWith (return . Unlift)<br>
><br>
> The reason this works is that the `StT` associated type for `ReaderT` just<br>
> returns the original type, i.e. `type instance StT (ReaderT r) m a = a`. In<br>
> theory, we should be able to generalize `askRun` to any transformer for<br>
> which that applies. However, I can't figure out any way to express that<br>
> generalized type signature in a way that GHC accepts it. It seems like the<br>
> following should do the trick:<br>
><br>
> askRunG :: ( MonadTransControl t<br>
>            , Monad m<br>
>            , b ~ StT t b<br>
>            )<br>
>         => t m (Unlift t)<br>
> askRunG = liftWith (return . Unlift)<br>
><br>
> However, I get the following error message when trying this:<br>
><br>
> foo.hs:11:12:<br>
>     Occurs check: cannot construct the infinite type: b0 ~ StT t b0<br>
>     The type variable ‘b0’ is ambiguous<br>
>     In the ambiguity check for the type signature for ‘askRunG’:<br>
>       askRunG :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) b.<br>
>                  (MonadTransControl t, Monad m, b ~ StT t b) =><br>
>                  t m (Unlift t)<br>
>     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes<br>
>     In the type signature for ‘askRunG’:<br>
>       askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =><br>
>                  t m (Unlift t)<br>
><br>
> Adding AllowAmbiguousTypes to the mix provides:<br>
><br>
> foo.hs:17:30:<br>
>     Could not deduce (b1 ~ StT t b1)<br>
>     from the context (MonadTransControl t, Monad m, b ~ StT t b)<br>
>       bound by the type signature for<br>
>                  askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =><br>
>                             t m (Unlift t)<br>
>       at foo.hs:(12,12)-(16,25)<br>
>       ‘b1’ is a rigid type variable bound by<br>
>            the type forall (n1 :: * -> *) b2.<br>
>                     Monad n1 =><br>
>                     t n1 b2 -> n1 (StT t b2)<br>
>            at foo.hs:1:1<br>
>     Expected type: Run t -> Unlift t<br>
>       Actual type: (forall (n :: * -> *) b. Monad n => t n b -> n b)<br>
>                    -> Unlift t<br>
>     Relevant bindings include<br>
>       askRunG :: t m (Unlift t) (bound at foo.hs:17:1)<br>
>     In the second argument of ‘(.)’, namely ‘Unlift’<br>
>     In the first argument of ‘liftWith’, namely ‘(return . Unlift)’<br>
><br>
> I've tested with both GHC 7.8.4 and 7.10.1. Any suggestions?<br>
><br>
> ______________________________<u></u>_________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-<u></u>bin/mailman/listinfo/haskell-<u></u>cafe</a><br>
><br>
</blockquote></div>