How to allow interaction with higher rank types in Haskell?

Question

I faced a mysterious situation with a higher type of rank. I figured out how to make it work, but I don’t understand the difference between working and non-working versions.

With these background definitions:

{-# LANGUAGE RankNTypes #-} data AugmentedRational = Exact Integer Rational -- Exact zq is q * pi^z | Approximate (forall a.Floating a => a) approximateValue :: Floating a => AugmentedRational -> a approximateValue (Exact zq) = (pi ** (fromInteger z)) * (fromRational q) approximateValue (Approximate x) = x 

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

Version A (what I originally wrote does not 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 

Result:

 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 prompts of unclean types that I don’t quite 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 that works

 {-# LANGUAGE NoMonomorphismRestriction #-} -- add this approx :: (forall a.Floating a => a -> a) -> AugmentedRational -> AugmentedRational approx fx = let fx = f $ approximateValue x in Approximate fx 

Other non-working versions

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

Summary

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

Edit Note: Removed erroneous claim that the type in question was existential.

Answer 1

(Nothing in your question uses existential types. You have an Approximate constructor that has a polymorphic argument, resulting in Approximate having a rank-2 type and leading to problems with higher-ranking types and output type.)

Short answer: style without dots and types of a higher rank do not combine with each other. Avoid using composition of functions if polymorphic arguments are involved and stick to a simple application or $ , and everything will be fine. The direct way to write approx in a way that is accepted is as follows:

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

The problem is that the GHC does not support the proper support for "unclean" types. This means: if a function is polymorphic, its type variables can be created with monomorphic types, but not with those types that are again polymorphic. Why does it matter here?

See what you wrote:

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

Here you use the composition function ( . ) Twice. The type of function composition is as follows:

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

So, the above definition is analyzed as

 Approximate . (f . approximateValue) 

But

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

has a rank-2 type. Thus, matching an Approximate type with the first argument (.) Means that:

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

.

This is a description of instance b for a polymorphic type that the GHC does not allow. It offers ImpredicativeTypes as a language extension that can make it work, but unfortunately it is a very fragile language extension, and using this is usually not recommended. And, as you saw, even with ImpredicativeTypes enabled, GHC, as a rule, still requires quite a few additional type annotations, so your program will not work without additional changes.

An application with a normal function is built into the GHC and is handled differently during type checking. This is why a more accurate definition of approx works. Using $ also good, but only because the GHC has a special hack telling about type checking that $ really no different from an application.