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.