Problem with lifted-async
Hello, I'm writing a thread supervisor that allows implicitly passing some monadic context (e.g. ReaderT) using MonadBaseControl from monad-control. The problem is that I don't know how to tackle this error. GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( ex.hs, interpreted ) ex.hs:20:20: Couldn't match type ‘StM t a0’ with ‘StM t a’ NB: ‘StM’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: Async (StM t a0) Actual type: Async (StM t a) Relevant bindings include as :: Async (StM t a) (bound at ex.hs:19:30) t :: Task t a (bound at ex.hs:19:28) td :: TaskDescriptor t (bound at ex.hs:19:10) pollTask :: TaskDescriptor t -> TaskDescriptor t -> t (TaskDescriptor t) (bound at ex.hs:19:1) In the first argument of ‘poll’, namely ‘as’ In a stmt of a 'do' block: st <- poll as Failed, modules loaded: none. This minimal code snippet would be {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} import Control.Concurrent.Async.Lifted (Async,async,asyncBound,poll,cancel) import Control.Monad.Trans.Control (MonadBaseControl,StM) data Task m a = Task { taskVal :: m a } data TaskDescriptor m = forall a. TaskDescriptor { task :: Task m a, asyncThread :: Async (StM m a) } runTask :: forall a m. (MonadBaseControl IO m) => Task m a -> m (TaskDescriptor m) runTask = undefined pollTask td(TaskDescriptor t as) = do st <- poll as case st of Nothing -> pure td Just r -> runTask t main = undefined StM is a type from MonadBaseControl typeclass, the definition is class MonadBase b m => MonadBaseControl b m | m -> b where type StM m a :: * liftBaseWith :: (RunInBase m b -> b a) -> m a restoreM :: StM m a -> m a type RunInBase m b = forall a. m a -> b (StM m a) I stripped the comments, the full version is here https://hackage.haskell.org/package/monad-control-1.0.0.4/docs/src/Control-M...
ex.hs:20:20: Couldn't match type ‘StM t a0’ with ‘StM t a’ NB: ‘StM’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: Async (StM t a0) Actual type: Async (StM t a) Relevant bindings include as :: Async (StM t a) (bound at ex.hs:19:30) t :: Task t a (bound at ex.hs:19:28) td :: TaskDescriptor t (bound at ex.hs:19:10) pollTask :: TaskDescriptor t -> TaskDescriptor t -> t (TaskDescriptor t) (bound at ex.hs:19:1) In the first argument of ‘poll’, namely ‘as’ In a stmt of a 'do' block: st <- poll as Failed, modules loaded: none.
A working version can be found at the bottom of this message: essentially you need to explain to GHC that the 'a' and 'a0' from the above error message are in fact the same. The problem is indeed, as GHC suggests, that the StM type family might not be injective. The signature of 'poll' is poll :: forall m a0. MonadBaseControl IO m => Async (StM m a0) -> m (Maybe (Either SomeException a0)) Now, 'poll' is fed the argument 'as', which has type Async (StM m a), where 'a' is from opening the existential TaskDescriptor type. GHC combines this with the type of 'poll', and concludes that Async (StM m a) ~ Async (StM m a0). Now, we would like to conclude from this that a ~ a0, but this is not a valid conclusion, exactly because of this possible non-injectivity of StM. Because the return value of 'poll' is not used quite that fully, there is no way for the compiler to infer what the type variable 'a0' should be instantiated with. Another way to fix this is to use the return value of 'poll' in such a way that 'a0' must equal 'a', for example by replacing the line Just r -> runTask t by Just r -> runTask (case r of Left _ -> t; Right a -> Task (return a)) That way, you don't need the below scoped type variables workaround. (BTW: perhaps the LHS of 'pollTask' should be pollTask td@(TaskDescriptor t as) , with the @ ? Doesn't really matter for the problem at hand, though.) Regards, Arie ==== ✂ ==== {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} import Control.Concurrent.Async.Lifted (Async,async,asyncBound,poll,cancel) import Control.Monad.Trans.Control (MonadBaseControl,StM) import Control.Exception.Base (SomeException) data Task m a = Task { taskVal :: m a } data TaskDescriptor m = forall a. TaskDescriptor { task :: Task m a, asyncThread :: Async (StM m a) } runTask :: forall a m. (MonadBaseControl IO m) => Task m a -> m (TaskDescriptor m) runTask = undefined pollTask td(TaskDescriptor (t :: Task m a) as) = do st :: Maybe (Either SomeException a) <- poll as case st of Nothing -> return td Just r -> runTask t main = undefined ==== ✂ ====
On 16:38 Sat 05 Sep , Arie Peterson wrote:
A working version can be found at the bottom of this message: essentially you need to explain to GHC that the 'a' and 'a0' from the above error message are in fact the same.
The problem is indeed, as GHC suggests, that the StM type family might not be injective. The signature of 'poll' is
poll :: forall m a0. MonadBaseControl IO m => Async (StM m a0) -> m (Maybe (Either SomeException a0))
Now, 'poll' is fed the argument 'as', which has type Async (StM m a), where 'a' is from opening the existential TaskDescriptor type. GHC combines this with the type of 'poll', and concludes that Async (StM m a) ~ Async (StM m a0). Now, we would like to conclude from this that a ~ a0, but this is not a valid conclusion, exactly because of this possible non-injectivity of StM. Because the return value of 'poll' is not used quite that fully, there is no way for the compiler to infer what the type variable 'a0' should be instantiated with.
Another way to fix this is to use the return value of 'poll' in such a way that 'a0' must equal 'a', for example by replacing the line
Just r -> runTask t
by
Just r -> runTask (case r of Left _ -> t; Right a -> Task (return a))
That way, you don't need the below scoped type variables workaround.
Great! That solved it. Thank you.
(BTW: perhaps the LHS of 'pollTask' should be
pollTask td@(TaskDescriptor t as)
, with the @ ? Doesn't really matter for the problem at hand, though.)
That was just a minimal example showing the problem. The actual code is a bit longer.
participants (2)
-
Arie Peterson -
Lana Black