Tricky type signature for pairs of reversed pairs

Question

Lets say I have the following data type:

data D a b = D (a,b) (b,a)

And I want to define the following function on it:

apply f (D x y) = D (f x) (f y)

What is the type signature of apply?

Here are some examples of f which are okay:

f :: a -> a -- OK
f :: (a, b) -> (b, a) -- OK
f :: (a, b) -> ((a, c), (b, c)) -- OK

In all of the above cases, we end up with a valid type D.

But this is not okay:

f :: (a, b) -> (a, a)

Because when we send such a function through apply we end up having to attempt to construct D (a,a) (b,b) which is not valid unless a = b.

I can't seem to work out a type signature to express all this? Also, in general, is there a way to get GHC to tell me what these signatures should be?

Typed Holes Edit:

In an attempt to find the type using typed holes, I tried the following:

x = apply _ (D (1::Int,'a') ('b',2::Int))

And got:

Found hole ‘_’ with type: (Int, Int) -> (b, b)
Where: ‘b’ is a rigid type variable bound by
           the inferred type of x :: D b b

Which seems to me to be nonsense as f :: (Int, Int) -> (b, b) is clearly not going to work here.

Answer 1

Multiple types fit apply, but the inferred ((t, t) -> (b, b)) -> D t t -> D b b is the most sensible and usable one. The alternatives are going to be higher-rank, so let's enable that language extension:

{-# LANGUAGE RankNTypes #-}

First, we can make apply id work:

apply :: (forall a. a -> a) -> D a b -> D a b
apply f (D x y) = D (f x) (f y)

However, now id is the only function with which apply works (all total functions of type forall a. a -> a are equal to id).

Here's another type:

apply :: (forall a. a -> (c, c)) -> D a b -> D c c
apply f (D x y) = D (f x) (f y)

But this too comes at a price. Now the f-s can only be constant functions that ignore the previous fields of D. So apply (const (0, 0)) works, but we have no way to inspect the argument of f.

In contrast, the inferred type is pretty useful. We can express transformations with it that look at the actual data contained in D.

At this point, we might ask: why does GHC infer what it infers? After all, some functions work with the alternative types, but don't work with the default type. Could it be better to sometimes infer higher-ranked types? Well, such types are often extremely useful, but inferring them is unfeasible.

Type inference for rank-2 types is rather complicated, and not very practical either, because it's not possible to infer most general types. With rank-1 inference, we can infer a type that is more general than all other valid types for the same expression. There's no such guarantee with rank-2 types. And inference for rank-3 and above types is just undecidable.

For these reasons, GHC sticks to rank-1 inference, so it never infers types with forall-s inside function arguments.