[Haskell-cafe] Problem with lifted-async

Lana Black lanablack at amok.cc
Sat Sep 5 18:51:48 UTC 2015

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.

More information about the Haskell-Cafe mailing list