Lambda the Ultimate

Given the recent discussion in the Subtyping+overloading thread I wanted to ask a question which has been bugging me (for ages).

I assume we all known HM style type inference.

As I understand it, HM has been extended with quantifiers to allow multiple instantiations of the same type, or hiding of known types. I.e., the following good old example only type checks if 'id' has type 'forall a. a -> a':

let id = \x . x in
 (id true, id 1)

Great, problem solved, one would think.

My problem with the current definition of the quantifiers is the following. A bold statement: the types (1) 'forall a . a' and (2) 'forall a b . a -> b' should not exist! I find it strange for (1) that a term can be written which unifies with any given type, similar in case (2), where a result is produced which can get any type.

Let me define the predicate 'great!' as types I personally like.

A type 'forall a . a -> a' is 'great!' since you know that the first 'a' will be bound by an argument, and a term can then be generated which holds the same type. A type '(forall a . a) -> (exists b . b)' is also 'great!' since it takes a known type, and produces a value out of a hidden type.

I am wondering if the current quantifiers were too much inspired by HM [or type theory], and are a false solution to the multiple instantiation problem. So I am looking for non-standard approaches which tackle this.