= Solution
Let `x :: a` and `g :: a -> b`, as required by the inner application `g x`. Using `g x` as the next argument of that same `g` forces `b = a`. Thus `g (g x) :: a`. Applying that result to `x` requires a function type `a -> c`, giving
$$
\boxed{a=a\to c.}
$$
This equation fails the <occurs check>: the type variable `a` occurs inside the type with which it would be unified. These constraints have no solution in the <Hindley-Milner type system>. Therefore \b[the definition has no type in ordinary <Haskell>]. The obstruction is to <type inference>, independently of which particular values might later be supplied.
Back to article page
