How to type the simply typed lambda calculus term (S K K)

Question

I am attempting to implement a simply typed lambda calculus type checker. When running sanity tests I tried typing (S K K) and my type checker throws this error:

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

The offending term is clearly the (S K K)

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

I think the problem arises from a lack of polymorphism because when I type check this haskell code it works fine:

k x y = x
s x y z = x z (y z)
test = s k k -- type checks

but if I specialize the type:

k :: () -> () -> ()
k x y = x
s :: (() -> () -> ()) -> (() -> ()) -> () -> ()
s x y z = x z (y z)
test = s k k -- doesn't type check 

Just for reference my type system is a simple as it gets:

data Type = T | TArr Type Type

full source

Answer 1

I will steal the ideas from a previous answer of mine to show how to ask ghci your question. But first I am going to reformulate your question slightly.

In Haskell, we have

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: a -> b -> a

and the question we want to ask is "What do these types look like after type-checking s k k?". More to the point, if we rewrite them with distinct unification variables,

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: d -> e -> d
k :: f -> g -> f
s k k :: h

then the question becomes a unification one: we are trying to unify the type of s with the type it's being used at -- namely (d -> e -> d) -> (f -> g -> f) -> h. Now that we have a unification question in hand, we can ask in the format showed in my other answer:

> :{
| :t undefined
| ::   ((a -> b -> c) -> (a -> b) -> (a -> c))
|    ~ ((d -> e -> d) -> (f -> g -> f) -> h)
| => (a, b, c, d, e, f, g, h)
| :}
undefined
::   ((a -> b -> c) -> (a -> b) -> (a -> c))
   ~ ((d -> e -> d) -> (f -> g -> f) -> h)
=> (a, b, c, d, e, f, g, h)
  :: (f, g -> f, f, f, g -> f, f, g, f -> f)

And now we can see why your version doesn't work: in your version, you've instantiated all polymorphic variables to the base type T; but since b ~ g -> f, e ~ g -> f, and h ~ f -> f are manifestly arrow types, that certainly isn't going to work! However, any choices for f and g will work if we respect the substitution above; in particular if we choose f ~ T and g ~ T, then we have

s :: (T -> (T -> T) -> T) -> (T -> (T -> T)) -> (T -> T)
k1 :: T -> (T -> T) -> T
k2 :: T -> T -> T
s k1 k2 :: T -> T