Why does adding an as-pattern to a working function cause compilation errors?

Question

Here's the standard Functor instance for Either a:

instance Functor (Either a) where
        fmap _ (Left x) = Left x
        fmap f (Right y) = Right (f y)

adding in an as-pattern causes compilation errors when loading into GHCi:

instance Functor (Either a) where
        fmap _ z@(Left x) = z          -- <-- here's the as-pattern
        fmap f (Right y) = Right (f y)

Couldn't match expected type `b' against inferred type `a1'
  `b' is a rigid type variable bound by
      the type signature for `fmap' at <no location info>
  `a1' is a rigid type variable bound by
       the type signature for `fmap' at <no location info>
  Expected type: Either a b
  Inferred type: Either a a1
In the expression: z
In the definition of `fmap': fmap _ (z@(Left x)) = z

Why doesn't this work?

Answer 1

If you specialize the signature of fmap to Either l, you get:

fmap :: (a -> b) -> Either l a -> Either l b

This means that the Left r that you are pattern-matching on the left-hand side of your case statement must have type Either l a. However, you can't return it as is, because you have to return an Either l b. This requires re-wrapping the left-hand value in a new Left so that the compiler can infer that it is returning a newly minted Either that might have a different type for the Right value.

Answer 2

For the Either a instance, fmap has the following type:

(i -> j) -> Either a i -> Either a j

In this equation:

fmap _ (Left x) = Left x

the second argument is known to be of type Either a i and to have matched the pattern Left x. We take the x out, and apply Left to it to get the result of fmap.

The trick is that the Left on the left side of the equation is not the same thing as the Left on the right side! On the LHS Left is this constructor:

Left :: a -> Either a i

Whereas on the RHS the Left is this constructor:

Left :: a -> Either a j

The RHS Left used in the pattern wouldn't have matched the type of fmap's second argument Either a i, and the LHS Left doesn't construct values of the type needed as fmap's result Either a j.

So there's no way to use the same Left for both things, semantically speaking; you have to construct a new Left x :: Either a j containing the x found in the Left x :: Either a i. Operationally, the Haskell implementation may or may not represent those two terms identically, and may or may not be able to share a single in-memory representation of two values with different types, and may or may not be clever enough to optimise away the construction of a new value that would be represented identically to another value it already has on hand. But those implementation issues are distinct from what the program means, and the type-checker's role is purely concerned with meaning.

Answer 3

fmap has signature (a -> b) -> f a -> f b, i.e. it has to allow for a and b to be different. In your implementation, a and b can only be the same, because it returns the same thing that was passed as an argument. So GHC complains.

Answer 4

My best guess is that this fails because z represents different types on each side of the equation:

• the overall type is fmap :: (a -> b) -> Either t a -> Either t b

• on the left side, z :: Either t a

• on the right side, z :: Either t b

It seems that Left x is allowed to have multiple different types in the same equation, but z is not.

This implementation also fails, apparently for the same reason:

instance Functor (Either a) where
        fmap f (Right y) = Right (f y)
        fmap _ z = z          

Couldn't match expected type `b' against inferred type `a1'
  `b' is a rigid type variable bound by
      the type signature for `fmap' at <no location info>
  `a1' is a rigid type variable bound by
       the type signature for `fmap' at <no location info>
  Expected type: Either a b
  Inferred type: Either a a1
In the expression: z
In the definition of `fmap': fmap _ z = z