How does let interact with higher rank types in Haskell?

Question

I ran in to a puzzling situation with a higher rank type. I figured out how to make it work, but I don't understand the difference between the working and non-working versions.

With these background definitions:

{-# LANGUAGE RankNTypes #-}

data AugmentedRational = Exact Integer Rational -- Exact z q is q * pi^z
                       | Approximate (forall a.Floating a => a)

approximateValue :: Floating a => AugmentedRational -> a
approximateValue (Exact z q) = (pi ** (fromInteger z)) * (fromRational q)
approximateValue (Approximate x) = x

... what is the difference between these two functions.

Version A (what I initially wrote, doesn't work)

-- lift a floating function to operate on augmented rationals, treating the function as approximate
approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f = Approximate . f . approximateValue

Resulting in:

Cannot instantiate unification variable `b0'
with a type involving foralls: forall a. Floating a => a
  Perhaps you want ImpredicativeTypes
In the first argument of `(.)', namely `Approximate'
In the expression: Approximate . f . approximateValue

If you follow the impredicative types suggestion, which I don't fully understand, the error message changes to:

No instance for (Floating (forall a. Floating a => a))
  arising from a use of `f'
In the first argument of `(.)', namely `f'
In the second argument of `(.)', namely `f . approximateValue'
In the expression: Approximate . f . approximateValue

Version B, which does work

{-# LANGUAGE NoMonomorphismRestriction #-} -- add this

approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f x = let fx = f $ approximateValue x
              in Approximate fx

Other nonworking versions

-- this one is "perhaps you meant impredicative types"
approx f x = Approximate . f . approximateValue $ x
-- these ones give the no instance Floating (forall a.Floating a => a) message
approx f x = Approximate . f $ approximateValue x
approx f x = let x' = approximateValue x
              in Approximate . f $ x'

Summary

What is going on here? In my head these 5 definitions are all syntactically different ways of saying the exact same thing.

Edit note: Removed mistaken claim that the type in question was an existential one.

Answer 1

(Nothing in your question uses existential types. What you have is a constructor Approximate that has a polymorphic argument, resulting in Approximate having a rank-2 type and leading to issues with higher-rank types and type inference.)

The short answer is: Point-free style and higher-rank types don't go well together. Avoid the use of function composition if polymorphic arguments are involved and stick to plain function application or $, and everything will be fine. The straight-forward way to write approx in a way that is accepted is this:

approx :: (forall a . Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f ar = Approximate (f (approximateValue ar))

The problem is that GHC doesn't properly support "impredicative" types. This means: If a function is polymorphic, its type variables can be instantiated with monomorphic types, but not with types that are in itself polymorphic again. Why is this relevant here?

Let's look at what you wrote:

approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational
approx f = Approximate . f . approximateValue

You're using function composition (.) here, twice. The type of function composition is this:

(.) :: (b -> c) -> (a -> b) -> a -> c
infixr 9 .

So the definition above is parsed as

Approximate . (f . approximateValue)

But

Approximate :: (forall a. Floating a => a) -> AugmentedRational

has a rank-2 type. So matching the type of Approximate with the first argument of (.) means that:

b = forall a. Floating a => a
c = AugmentedRational

has to hold.

It's this instantiation of b to a polymorphic type that GHC does not allow. It suggests ImpredicativeTypes as a language extension that might make it work, but unfortunately, it's a very fragile language extension, and the use of this is generally discouraged. And as you've seen, even with ImpredicativeTypes enabled, GHC will typically still require quite a few additional type annotations, so your program won't work without additional changes.

Normal function application is built into GHC and treated differently during type-checking. That's why the more direct definition of approx works. Using $ is also ok, but only because there's a special hack implemented in GHC telling the type checker that $ is really no different from function application.