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

Question

Here is a standard Functor instance for Either a :

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

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

 instance Functor (Either a) where fmap _ z@ (Left x) = z -- <-- here the as-pattern fmap f (Right y) = Right (fy) 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 ab Inferred type: Either a a1 In the expression: z In the definition of `fmap': fmap _ ( z@ (Left x)) = z 

Why is this not working?

Answer 1

fmap has a signature (a -> b) -> fa -> fb , i.e. it must have values a and b . In your implementation, a and b can only be the same, since it returns the same thing that was passed as an argument. Therefore, the GHC complains.

Answer 2

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

• generic type fmap :: (a -> b) -> Either ta -> Either tb

• left side, z :: Either ta

• on the right side, z :: Either tb

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

This implementation also does not work, apparently for the same reason:

 instance Functor (Either a) where fmap f (Right y) = Right (fy) 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 ab Inferred type: Either a a1 In the expression: z In the definition of `fmap': fmap _ z = z 

Answer 3

If you specialize fmap signature before Either l , you get:

 fmap :: (a -> b) -> Either la -> Either lb 

This means that Left r , that you are matching patterns on the left side of your case statement, must be of type Either la . However, you cannot return it as is, because you need to return Either lb This requires re-packing the left value into a new Left , so that the compiler can assume that it returns a new minted Either , which may have a different type for the Right value.

Answer 4

For an instance, Either a fmap is of the following type:

 (i -> j) -> Either ai -> Either aj 

In this equation:

 fmap _ (Left x) = Left x 

it is known that the second argument is of type Either ai and matches the Left x pattern. Take x out and apply Left to it to get the result of fmap .

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

 Left :: a -> Either ai 

Whereas on RHS Left is a constructor:

 Left :: a -> Either aj 

The RHS Left used in the template would not match the fmap type of the second argument Either ai , and LHS Left would not produce the type value needed as the fmap result Either aj .

Thus, it is not possible to use the same Left for both things, semantically; you need to build a new Left x :: Either aj containing x found in Left x :: Either ai . Haskell’s implementation may or may not represent the two terms in the same way and may or may not share the same representation in memory of two values ​​with different types and may or may not be smart enough to optimize the construction of a new value that will be presented identically to another value, which it already has at hand. But these implementation problems are different from what the program means, and the role of type checking makes pure sense.