Lambda the Ultimate

First, I don't really agree with your description of the situation in Java. I haven't thought about it particularly hard, but I would say that the situation of class parameters and generic method parameters works exactly the same. Either way, you just need to introduce a variable name before you use it:
class Foo<A,B> /* A and B introduced here */ { ... }
vs.
public static <A,B> /* A and B introduced here */ void foo(...) {...}

In both cases, the variables are implicitly universally quantified.

Some languages (those in the Haskell/ML family) will also infer the scope of type variables and so don't require these declarations. But in those cases as well, the quantification of the variables is implicitly universal.

Haskell provides the option to explicitly quantify type variables, which as you note is necessary in some cases. Using that syntax, one explicitly introduces the scope of the variable as well. So, I would say we have the following three possibilities:

1. explicitly introduced, implicitly quantified
2. implicitly introduced, implicitly quantified
3. explicitly introduced, explicitly qunatified

As far as I know, Java does not provide any mechanism for making the quantification of type variables explicit. You are right in mentioning that explicit introduction of type variables is necessary in Java because otherwise there is no syntactic distinction between type variables and type constants (i.e., actual class names).

So, in sum, yes, you can eliminate the explicit declaration of type variables if there is some lexical way to distinguish them. But regarding actual explicit quantification, I don't think it's ever necessary unless you either (a) have other quantifiers (e.g., existential types) or (b) need to control the scope of quantification more precisely (e.g., you want to support rank-two types or other fancy stuff).

I'm curious though, whether others have different views.

I see two different aspects to your question. I will answer in the context of the ML family (SML, OCaml, Haskell) wich I know better than Java.

1. Why is quantification left implicit in types ?

In ML polymorphic types, quantification over type variable is left implicit because they always happen at the beginning of the type. That's a property of the ML type system. For example, we write ('a -> 'a) for the type of the identity, but what we really mean is (forall 'a. 'a -> 'a). Recovering the explicitely quantified type is easy : just add a forall for each free type variable.

This isn't possible anymore if you want higher-ranked polymorphism, that is, type quantification inside types. For example, ((forall 'a . list 'a -> list 'a) -> int) is a function taking a polymorphic function as parameter. The ML type system isn't able to express that. If you want your language to consider such types, you must give up the simplification that quantifiers only occur at the beginning of types. Such local polymorphism has practical uses, see e.g. the Haskell ST Monad:

runST :: forall α. (forall s. ST s α) -> α

2. Why is type variable scope left implicit in terms ?

In System F, when you write the identity function (Λα λ(x:α) x), the type variable α in the annotation λ(x:α) is not implicitly quantified : it is bound in the context (by the type introduction Λα).

ML-inspired languages have for a long time neglected proper scope rules for type variables. The implicit quantification of types, and the sometimes ad-hoc status of unification variables have lead to rather shadowy scope rules. When you write (let (x : 'a) = .. and (y : 'a) = ..), are the two occurences of ('a) unified or considered independent ?

This situation has improved recently, as the ML languages have added features to more rigourously specify the lexical scope of a type variable. See for example the new (type t) syntax of OCaml 3.12 (which has been mentioned on LtU) and the following Haskell paper :
Lexically scoped type variables

As type inference systems become more sophisticated, it becomes increasingly important to allow the programmer to give type annotations that both document the program and guide type inference. In Haskell 98, it is not possible to write certain type annotations, because they must mention a type that is "in scope" and the language provides no way to name such types.
The obvious solution is to provide language support for lexically-scoped type variables, an area whose design space has not been systematically explored. Our contribution is to bring together the relevant folk lore, in coherent form, and make it accessible to a much larger community than hitherto. In particular, we describe and contrast two main alternative designs --- the "type-lambda" approach of SML 97, and an alternative "type-sharing" approach which is used by the Glasgow Haskell Compiler and OCaml --- and survey some alternative design choices.

Scoped type variables will play a key role in the type systems of the future; they can no longer be added as an afterthought to language implementations.

Thanks for the replies. I think I understand it more clearly now.