[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