Typecheck fails for apparently equal instance definition

Question

Given the following type definition

newtype Constant a b = Constant { getConstant :: a }
  deriving (Eq, Show)

this Functor instance definition is valid

instance Functor (Constant a) where
  fmap _ (Constant x) = Constant x

whereas the apparently equivalent instance definition

instance Functor (Constant a) where
  fmap _ x = x

fails with the typecheck error (excerpt)

Expected type: Constant a b
  Actual type: Constant a a1

using GHC version 8.0.2.

The question is, why these two (apparently equivalent) instance definitions behave differently in terms of typechecking.

Answer 1

It might become clearer if we give the constructor a different name, so as to distinguish type-level and value-level:

newtype Constant a b = ConstVal { getConstVal :: a }
  deriving (Eq, Show)

instance Functor (Constant a) where
  fmap _ (ConstVal x) = ConstVal x

Now, why can you not write fmap _ x = x?

ConstVal is a polymorphic constructor:

ConstVal :: a -> Constant a b

...i.e.

ConstVal :: ∀ a b . a -> Constant a b

Though that universal quantifier is optional in Haskell, it is actually important. ConstVal has basically two additional, type-level arguments. In other words, this is not just one constructor but a whole family of constructors, like

ConstValBoolBool :: Bool -> Constant Bool Bool
ConstValBoolInt  :: Bool -> Constant Bool Int
ConstValBoolChar :: Bool -> Constant Bool Char
...
ConstValCharBool :: Char -> Constant Char Bool
ConstValCharInt  :: Char -> Constant Char Int
ConstValCharChar :: Char -> Constant Char Char
...
...

All of these actually share the same value-level name ConstVal, but to the type system they are all distinct. Explicitly written out, you'd have for instance

fmapBoolStringInt :: (String -> Int) -> Constant Bool String -> Constant Bool Int
fmapBoolStringInt _ (ConstValBoolString x) = ConstValBoolInt x

Here it's clear that the values on both sides are not actually the same, and hence can not be reduced to fmapBoolStringInt _ x = x.