In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$, but there is a term of type $\forall \alpha.\; \alpha\mathbin\rightarrow\alpha$ (the identity function $\lambda x.x$).
Intuitively, a term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$ requires being able to build an expression of type $\beta$ from thin air. It is easy to see that there is no value which has such a type. More precisely, if the type variable $\beta$ does not appear in the type of any term variable in the environment, then there is no term of type $\beta$ which is in head normal form. You can prove this by structural induction on the term: either the variable at the head would have to have the type $\beta$, or one of the arguments would have to have a principal type involving $\beta$, i.e. there would be a smaller suitable term.
Just because there is no value of a certain type doesn't mean that there is no term of that type: there could be a term with no value, i.e. a non-terminating term (precisely speaking, a term with no normal form). The reason why there is no lambda term with such types is that all well-typed HM terms are strongly normalizing. This is a generalization of the result that states that simply typed lambda calculus is strongly normalizing. It is a consequence of the fact that System F is strongly normalizing: System F is like HM, but allows type quantifiers everywhere in types, not just at the toplevel. For example, in System F, $\Delta = \lambda x. x \, x$ has the type $(\forall \alpha. \alpha) \rightarrow (\forall \alpha. \alpha)$ — but $\Delta\,\Delta$ is not well-typed.
HM and System F are examples of type systems that have a Curry-Howard correspondence: well-typed terms correspond to proofs in a certain logic, and types correspond to formula. If a type system corresponds to a consistent theory, then that theory does not allow proving theorems such as $\forall A, \forall B, A \Rightarrow B$; therefore there is no term of the corresponding type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$. The type system allows one to deduce “theorems for free” about functions over data structures.
This result breaks down as soon as you add certain constants to the calculus. For example, if you allow a general fixpoint combinator such as $Y$, it is possible to build terms of arbitrary type: $Y (\lambda x.x)$ has the type $\forall \alpha. \alpha$. The equivalent of a general fixpoint combinator in the Curry-Howard correspondence is an axiom that states $\forall A, \forall B, A \Rightarrow B$, which makes the logic obviously unsound.
Finding the fine line between type systems that ensure strong normalization and type systems that don't is a difficult and interesting problem. It is an important problem because it determines which logics are sound, in other words which programs embody proofs of theorems. You can go a lot further than System F, but the rules become more complex. For example, the calculus of inductive constructions which is the basis of the Coq proof assistant, is strongly normalizing yet is capable of describing common inductive data structures and algorithms over them, and more.
As soon as you get to real programming languages, the correspondence breaks down. Real programming languages have features such as general recursive functions (which may not terminate), exceptions (an expression that always raises an exception never returns a value and hence can have any type in most type systems), recursive types (which allow non-termination to sneak in), etc.
