Algebraic Data Types and Equality

Question

Given the following data type from TypeClassopedia:

data Cons a = Cons a (Cons a) | Empty deriving (Show, Eq)

I implemented its evil Functor implementation:

instance Functor Cons where
    fmap _ Empty       = Empty
    fmap f (Cons x xs) = Cons (f x) (Cons (f x) (fmap f xs) )

Then, I attempted to write a function (quickcheck property) that takes a Cons a and returns a Bool:

prop_id_functor_law :: Cons a -> Bool
prop_id_functor_law x = fmap id x == id x

However, I get a compile-time error:

Prelude> :l EvilFunctor
[1 of 1] Compiling EvilFunctor      ( EvilFunctor.hs, interpreted )

EvilFunctor.hs:18:23:
    No instance for (Eq a) arising from a use of `=='
    Possible fix:
      add (Eq a) to the context of
        the type signature for prop_id :: Cons a -> Bool
    In the expression: fmap id x == id x
    In an equation for `prop_id': prop_id x = fmap id x == id x
Failed, modules loaded: none.

My rough intuition is that this compile-time error makes sense. How could two a's be compared unless they implemented the Eq typeclass?

However, what did the deriving ... Eq even do when I defined data Cons a?

Answer 1

It says you need to add the constraint to prop_id_functor_law, so it'd be prop_id_functor_law :: Eq a => Cons a -> Bool. The deriving part just means it derives the instance

instance Eq a => Eq (Cons a) where
    Empty == Empty = True
    Cons a1 x1 == Cons a2 x2 = a1 == a2 && x1 == x2
    _ == _ = False

You still have that the type parameter is constrained in order for the Eq instance to be satisfied. If you were to check :info Cons in GHCi, you'd see that instance.

Answer 2

what did the deriving ... Eq even do when I defined data Cons a?

When you derive an instance, GHC always mechanically generates an instance that implements the logic required by the type class for the structure of the type. For example:

data Foo = Foo Int Int
  deriving Eq

Will give you something like:

instance Eq Foo
  where Foo a b == Foo a' b'
          = a == a' && b == b'

But if you had instead:

data Foo a b = Foo a b
  deriving Eq

Then it can tell it needs to follow the same structure (Foos are equal if both contained fields are equal) but it is forced to delegate to equality for the types a and b for part of the comparison. These aren't always types that have equality, so the derived instance has to declare that they do as constraints:

instance (Eq a, Eq b) => Eq (Foo a b)
  where Foo a b == Foo a' b'
          = a == a' && b == b'

The same thing happens for your Cons. So two Cons a values are comparable for equality when a values are comparable for equality. A function like prop_id_functor_law :: Cons a -> Bool is declared to work for all Cons a values, whether or not Eq a holds, so the type checker will not allow you to call == on Cons a within the implementation; it might not support equality, and guaranteeing that you never call unsupported operations is the point of type checking. But if you instead had prop_id_functor_law :: Eq a => Cons a -> Bool, then you could use == (and the responsibility moves to the callers of prop_id_functor_law to ensure they call it for types that support equality).