strange existential type

Question

http://www.iai.uni-bonn.de/~jv/mpc08.pdf - in this article I cannot understand the following declaration:

instance TreeLike CTree where
...
abs :: CTree a -> Tree a
improve :: (forall m. TreeLike m => m a) -> Tree a
improve m = abs m

1. what difference (forall m. TreeLike m => m a) brings (I thought TreeLike m => m a would suffice here)

2. why does it permit abs here, if m in m a can be any TreeLike, not just CTree?

Answer 1

That's a rank-2 type, not an existential type. What that type means is the argument for improve must be polymorphic. You can't pass a value of type Ctree a (for instance) to improve. It cannot be concrete in the type constructor at all. It explicitly must be polymorphic in the type constructor, with the constraint that the type constructor implement the Treelike class.

For your second question, this allows the implementation of improve to pick whichever type for m it wants to - it's the implementation's choice, and it's hidden from the caller by the type system. The implementation happens to pick Ctree for m in this case. That's totally fine. The trick is that the caller of improve doesn't get to use that information anywhere.

This has the practical result that the value cannot be constructed using details of a type - it has to use the functions in the Treelike class to construct it, instead. But the implementation gets to pick a specific type for it to work, allowing it to use details of the representation internally.