The type signature of a combinator does not match the type signature of its equivalent Lambda function

Question

Consider this combinator:

S (S K)

Apply it to the arguments X Y:

S (S K) X Y

It contracts to:

X Y

I converted S (S K) to the corresponding Lambda terms and got this result:

(\x y -> x y)

I used the Haskell WinGHCi tool to get the type signature of (\x y -> x y) and it returned:

(t1 -> t) -> t1 -> t

That makes sense to me.

Next, I used WinGHCi to get the type signature of s (s k) and it returned:

((t -> t1) -> t) -> (t -> t1) -> t

That doesn't make sense to me. Why are the type signatures different?

Note: I defined s, k, and i as:

s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)

Answer 1

We start with the types of k and s

k :: t1 -> t2 -> t1
k = (\a x -> a)

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5
s = (\f g x -> f x (g x))

So passing k as the first argument of s, we unify k's type with the type of s's first argument, and use s at the type

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1

hence we obtain

s k :: (t1 -> t2) -> t1 -> t1
s k = (\g x -> k x (g x)) = (\g x -> x)

Then in s (s k), the outer s is used at the type (t3 = t1 -> t2, t4 = t5 = t1)

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

applying that to s k drops the type of the first argument and leaves us with

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

As a summary: In Haskell, the type of s (s k) is derived from the types of its constituent subexpressions, not from its effect on its argument(s). Therefore it has a less general type than the lambda expression that denotes the effect of s (s k).