Resolving the type of `f = f (<*>) pure`

Question

Recently I noticed that humourously liftA can be written as

liftA (<*>) pure

I thought this was neat and so as a bit of a joke I thought I would make a new "definition" of liftA based on this property:

f = f (<*>) pure

Now I had expected that this would be something of the same type as liftA that just never halted. However it fails to compile.

• Occurs check: cannot construct the infinite type:
    t ~ (f (a -> b) -> f a -> f b) -> (a1 -> f1 a1) -> t
• In the expression: f (<*>) pure
  In an equation for ‘f’: f = f (<*>) pure
• Relevant bindings include
    f :: (f (a -> b) -> f a -> f b) -> (a1 -> f1 a1) -> t
      (bound at liftA.hs:2:1)

This seems sensible, I see how the compiler has an issue. However things get a little weird because when I add an annotation:

f :: Applicative f => (a -> b) -> f a -> f b
f = f (<*>) pure

It suddenly compiles.

Now my initial suspicion was that the type I was annotating f with was not the most general type and that by restricting the type I had made it possible to unify things. However looking at the types this doesn't seem to be the case my type seems to be more general than the type that the compiler was trying to derive.

What is going on here? I am a bit out of my depth here but I am curious as to what the compiler is thinking in each scenario and why it encounters an issue in one but not the other.

Answer 1

It’s because the f used in the body of the definition of f has a different type than the definition. This is called polymorphic recursion, and Haskell only allows that if you provide a type signature. The reason for requiring a type signature is that type inference for polymorphic recursion is undecidable in the general case.