Potential type error in Error law

[maralorn]

Following our discussion on irc I am still trying to wrap my head around the catch handling in eff.

While looking at the law for catch I wondered if the pure is correct there.

According to this type signature:

catch :: Error e :< effs => Eff (Error e ': effs) a -> (e -> Eff effs a) -> Eff effs a 

I deduce the types catch (throw x) f :: Eff effs a and f x :: Eff effs a, so pure (f x) :: Applicative a1 => a1 (Eff effs a)?

So I think instead of catch (throw x) f ≡ pure (f x) it should just be catch (throw x) f ≡ f x.