Why the difference in type-inference over the as-pattern in two similar function definitions?

Question

I have the following two similar function definitions:

left f (Left x) = Left (f x) left _ (Right x) = Right x  left' f (Left x) = Left (f x) left' _ r@(Right _) = r 

When I check the type signatures of the two functions, I am confused by the following types:

ghci> :t left left :: (t -> a) -> Either t b -> Either a b ghci> :t left' left' :: (a -> a) -> Either a b -> Either a b 

I suppose left and left' should be of the same type signature, but the haskell's type inference gives me a suprise.

I can't figure out why the type signatures of left and left' are different. Can anybody give me some information? Thanks!

Answer 1

In the second line of left':

left' _ r@(Right _) = r --      ^^^^^^^^^^^   ^ 

Since you use an as-pattern, you require the input type to be equal to the return type, since clearly they're the exact same value. left''s type is then restricted to something of the form a -> b -> b.

This restriction then propogates backwards to in turn restrict the function's type – hopefully you can see how; it's not too difficult.

However, in the second line of left, you construct a new value

left _ (Right x) = Right x --                 ^^^^^^^ 

The type of this new value has not been restricted, and thus the same problem doesn't occur; it can be something of the form a -> b -> c, which is what you want.

For this reason, the type of left' is more restricted than the type of left, which is what causes their types to be unequal.

---

To illustrate this concept more concretely, I will describe to you more precisely how this restriction propogates backwards.

We know that left''s signature is of the form (a -> b) -> Either a q -> Either b q. However, line 2 dictates that Either a q = Either b q, which means that a = b, so the type now becomes (a -> a) -> Either a q -> Either a q.