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

The key to this is in the type signature of bimap:

bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d

In this particular case, if we specialise p to SemiDrei a and rename the type variables to avoid confusion with that a, we get:

bimap :: (b -> c) -> (d -> e) -> SemiDrei a b d -> SemiDrei a c e

So when you attempt to implement this:

bimap f g = ...

The functions f and g are completely arbitrary, not just in their implementation, but in their input and return types as well. f has type b -> c where b and c could be absolutely anything - similarly for g. The definition you give has to work for absolutely any types and functions that the caller provides - this is what being (parametrically) polymorphic means.

If we now look at your three definitions in these terms, we can solve the apparent mystery:

First:

bimap f g (SemiDrei a) = SemiDrei a

this is completely fine, as you saw. SemiDrei a has type SemiDrei a b c, where only a is specified. That means it can take on any type such as SemiDrei a Int String, or SemiDrei [Bool] (Char, [Double]), or whatever. SemiDrei a is itself polymorphic, it can be of any compatible type. This means that in particular it can act as both the SemiDrei a b c and the SemiDrei a c e in the above signature of bimap.

Contrast with your other attempts:

bimap f g = id

The problem here is that id, although polymorphic, is not polymorphic enough for this purpose. Its type is a -> a (for any a), which in particular can be specialised to SemiDrei a b c -> SemiDrei a b c. But it can't possibly be specialised to a type SemiDrei a b d -> SemiDrei a c e as required, because b, c, d and e will in general be completely different types. Recall that the caller of bimap gets to choose what the types are - they can easily choose functions f and g where b and c are different types, for example, and then there is no way id can take a SemiDrei a b d to SemiDrei a c e, because they're different types.

At this stage you may object that the value SemiDrei a can be a value of all such types. That's perfectly true, but it's not relevant for type inference - the compiler only cares about the types, not what values may inhabit them. It has to consider that different types have completely different, non-intersecting, values. And, say, SemiDrei a Int String and SemiDrei a Bool Char are in fact different types. Again, the compiler doesn't know that the Int etc aren't actually used by any of the values of the type. That's indeed exactly why such "phantom types" (types which appear in a type definition but not in any of their data constructors) are used in practice - to allow the compiler to be able to differentiate them by type, even though the run-time representation might be completely equivalent.

As for your third attempt, bimap f g x = x, that's exactly the same as the previous one - it constrains bimap f g to have its output type the same as its input. (It's in fact totally equivalent to bimap f g = id.)

So the important takeaway is that, at the type-checking phase, the compiler only cares about types - and two types with different names are (and have to be) considered totally distinct, even though it may be that equivalent values can be embedded in both.

Answer 3

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.