There are a couple of levels to your first question. As an aside, though, I recommend learning about unification if you are not already familiar with it as it is a key part of understanding type checking and type inference.
To type check
selfApply provisionally give
f the type
a which we will solve for. (At this point it is just a unification variable, the key difference between Hindley-Milner type checking and type checking for simple types is that we'll generalize (quantify over) any unbound variables at the end.) Since we are using
f as a function we know
a = b -> c for new variables
c. Since we are applying
f to something of type
f itself, we know
b = a. There is no constraint on
c, so you are correct to be confused about the provided answer since
f isn't required to be
a -> a and it could indeed be
a -> a -> a or
a -> Bool as well. Of course, as you no doubt understand, the issue is solving the equation
a = a -> c. In attempting to unify these with traditional unification we will fail what is known as the occurs check. This check is to avoid infinite terms. Rational tree unification is, however, one way to deal with this issue and leads to equi-recursive types. Haskell intentionally does not support equi-recursive types, but O'Caml, for example, does with the
-rectypes flag. To validate that
c is free we can use an iso-recursive type, namely:
data X c = X (X c -> c)
selfApply f = f (X f)
which will type check, and, in particular,
selfApply :: (X c -> c) -> c.
There are two reasons Haskell (and almost all polymorphic languages) do not support equi-recursive types. First, pragmatically, many type errors show up as infinite types and if equi-recursive types were supported (tacitly) then they'd turn into broken but type correct programs. More philosophically, outlawing equi-recursive types and similar things was exactly why type systems were originally invented going all the way back to Bertrand Russell.