Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Functional programming, design and analysis of algorithms / 1 / c / 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, givingThis 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 the definition has no type in ordinary Haskell. The obstruction is to type inference, independently of which particular values might later be supplied.