[Haskell-cafe] Problem with lifted-async

[Arie Peterson]

> 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
==== ✂ ====