Type Signature Mismatch on Bifunctor instance definition

Question

I'm learning about Haskell by working through the book Haskell Programming from First Principles, Allen & Moronuki.

In the exercises for the chapter on Monad Transformers, Functor & Applicative composition, it asks the reader to write Bifunctor instance for the following type

data SemiDrei a b c = SemiDrei a

My first attempt (which compiles) was

instance Bifunctor (SemiDrei a) where
    bimap f g (SemiDrei a) = SemiDrei a

But, looking at it, It seemed to me that I ought to be able to write bimap f g = id because the last argument is yielded unchanged or write bimap f g x = x. Both gave me compile errors, and I'm hoping someone can explain to me why I can't express the bimap with these shorter alternatives, i.e. why do I have to specify (SemiDrei a).

I ran this on Haskell 8.6.5 (in case that is relevant)

attempt: id

instance Bifunctor (SemiDrei a) where
    bimap f g = id

-- compile error message:
• Couldn't match type ‘a1’ with ‘b’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  ‘b’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  Expected type: SemiDrei a a1 c -> SemiDrei a b d
    Actual type: SemiDrei a b d -> SemiDrei a b d
• In the expression: id
  In an equation for ‘bimap’: bimap f g = id
  In the instance declaration for ‘Bifunctor (SemiDrei a)’
• Relevant bindings include
    f :: a1 -> b (bound at src/Main.hs:69:11)
    bimap :: (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
      (bound at src/Main.hs:69:5)
   |
69 |     bimap f g = id
   |                 ^^

attempt: f g x = x

instance Bifunctor (SemiDrei a) where
    bimap f g x = x

-- compile error message:
• Couldn't match type ‘a1’ with ‘b’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  ‘b’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  Expected type: SemiDrei a b d
    Actual type: SemiDrei a a1 c
• In the expression: x
  In an equation for ‘bimap’: bimap f g x = x
  In the instance declaration for ‘Bifunctor (SemiDrei a)’
• Relevant bindings include
    x :: SemiDrei a a1 c (bound at src/Main.hs:69:15)
    f :: a1 -> b (bound at src/Main.hs:69:11)
    bimap :: (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
      (bound at src/Main.hs:69:5)
   |
69 |     bimap f g x = x
   |                   ^

Answer 1

There last argument is not, in fact, yielded unchanged: its type changes. The input is SemiDrei a x y and the output is SemiDrei a p q, where f :: x -> p and g :: y -> q.

This means that you have to deconstruct the value of the original type and reconstruct a value of the new type, which is what you're doing in the original implementation.

But your intuition is correct: the two values do have the same in-memory representation. And GHC can deduce this fact, and when it does, it will automatically solve a Coercible constraint for you, which means that you can use the coerce function to convert one to the other:

 bimap _ _ = coerce

Answer 2

This shows the same issue in a simpler case:

data T a = K

foo :: T a -> T b
foo K = K  -- type checks

bar :: T a -> T b
bar x = x  -- type error

-- bar = id would also be a type error, for the same reason

The issue here is that the two K in foo values hide their type parameters. A more precise definition would be

-- pseudo code
foo (K @a) = K @b

Here you can see that the implicit type argument changes. GHC automatically infers those type arguments for us when we write K in the definition of foo. Since they are implicit, they look as if they are the same Ks, but they are not to the type checker.

Instead, when we use x in the definition of bar, there are no implicit type arguments to infer. We have that x :: T a and that's all. We can not use x and claim that has a different type T b.

Finally, note that using "safe coercions" we can perform the intuitively correct kind-of-id which turns one K (in one type) into the other K of the other type:

import Data.Coerce

baz :: T a -> T b
baz = coerce

Whether this is better is arguable. For simple cases, pattern matching can be easier to understand than coerce, since the latter can perform a vast array of (safe) coercions, possibly leaving the reader to guess about what's actually happening at the type level.