My three eurocents. I believe that the Author of the original query won't care more about undefined stuff than most of us. He wants truly polymorphic functions, of the type, say, a->b->a etc., without constraints.
The answer exists, although it is not always trivial to find interesting examples.
Imagine a (postulated) polymorphic type, say, (a->b)->(b->a) . Consider the symbol (->) to be an implication in logic. Ask yourself; "is it a tautology, valid for *any* objects of types "a" or "b"? If yes, then this is a type, and you can in principle find a model for it.
Example: composition
type: (a->b)->(c->a) -> (c->b) function: (.) (.) f g x = f (g x)
On the other hand the "type" (a->b) is *NOT* a valid theorem. This is not a type. You won't find any model of it. No, no, get out with your f x = undefined.
The "subst" combinator: subst f g x = f x (g x) has the type
(a->b->c) -> (a->b) -> a -> c (unless I've produced some mistake)
The time you grouped (a->b->c), you utilized the arrow type constructor to build a function type, it is no different that using a polymorphic list. I think I am not happy with the dual semantics of this arrow thingie. I have to ponder on this some more, I guess. Thanks for the response. Greatly appreciated.