Manual derivation of the type for `f1 x xs = (filter . (<)) x xs`

Question

I want to manually derive the type of:

f1 x xs = (filter . (<)) x xs

First time we see x, so:

x :: t1

Then (<) has this type:

(<) :: Ord a1 => a1 -> a1 -> Bool

We can only say (< x) if the following types can be unified:

t1  ~  a1

Then

x :: a1

So

(<x) :: Ord a1 => a1 -> Bool

Filter has this type

filter :: (a2 -> Bool) -> [a2] -> [a2]

First time to see xs, so:

xs :: t2

We can only say (filter . (<)) x xs if the following types can be unified:

a1 -> Bool ~ a2 -> Bool
t2  ~ [a2]

So I get that f1 :: (a2 -> Bool) -> [a2] -> [a2], the same type as filter, when the correct type is Ord a => a -> [a] -> [a] (asking GHCi).

Any help?

Answer 1

The constraint

a1 -> Bool ~ a2 -> Bool

can be broken down to

a1 ~ a2

and the obviously true

Bool ~ Bool

So you have a1 ~ a2. You already know that x is a1, xs is [a2] and, thanks to filter, the result type is [a2]. Therefore, you end up with:

f1 :: Ord a2 => a2 -> [a2] -> [a2]

(Don't forget the class constraint a1 got from (<).)