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
what difference (forall m. TreeLike m => m a) brings (I thought TreeLike m => m a would suffice here)
why does it permit abs here, if m in m a can be any TreeLike, not just CTree?
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.
Whether m can be "any TreeLike" depends on your perspective.
From the perspective of implementing improve, it's true--m can be any TreeLike, so it picks one that's convenient, and uses abs.
From the perspective of the argument m--which is to say, the perspective of whatever is applying improve to some argument, something that's rather the opposite holds: m in fact must be able to be any TreeLike, not a single one that we choose.
Compare this to the type of numeric literals--something like (5 :: forall a. Num a => a) means that it's any Num instance we want it to be, but if a function expects an argument of type (forall a. Num a => a) it wants something that can be any Num instance it chooses. So we could give it a polymorphic 5 but not, say, the Integer 5.
You can, in many ways, think of polymorphic types as meaning that the function takes a type as an extra argument, which tells it what specific type we want to use for each type variable. So to see the difference between (forall m. TreeLike m => m a) -> Tree a and forall m. TreeLike m => m a -> Tree a you can read them as something like (M -> M a) -> Tree a vs. M -> M a -> Tree a.
