I am implementing Algorithm W for a toy language. I came across a case that I imagined would type check, but doesn't. I tried the same in Haskell, and to my surprise it didn't work there either.
> (\id -> id id 'a') (\x -> x)
Couldn't match type ‘Char -> t’ with ‘Char’
Expected type: Char -> t
Actual type: (Char -> t) -> Char -> t
I assumed that id would be polymorphic, but it doesn't seem to be. Note that this example works if id is defined using let instead of passed as an argument:
let id x = x in id id 'a'
'a'
:: Char
Which makes sense when looking at the inference rules for Algorithm W, since it has a generalization rule for let expressions.
But I wonder if there is any reason for this? Couldn't the function parameter be generalized as well so it can be used polymorphically?
The problem with generalizing lambda-bound variables is that it requires higher-rank polymorphism. Take your example:
(\id -> id id 'a')
If the type of id here is forall a. a -> a, then the type of the whole lambda expression must be (forall a. a -> a) -> Char, which is a rank 2 type.
Besides that technical point there is also an argument that higher rank types are very uncommon, so instead of inferring a very uncommon type it might be more likely that the user has made a mistake.