I think generics in Java are quite nice, surface issues aside. (In theory, that is. In practice, "Java seems to have been designed to strike a careful balance between making the type system as obstructive as possible while minimizing any actual guarantees of correctness" →. I think this is mostly due to Java's lack of RTTI for generics. C# doesn't have the same problems, except in places where they intentionally copied Java.)
My first nice discovery was that there's a beautifully simple theory behind generics: F-bounded polymorphism. (Reassuringly, it wasn't developed in academia, but by practitioners at HP Labs.)
In ordinary bounded polymorphism, you can give bounds to your type parameters:
F-bounded polymorphism is a simple extension of ordinary bounded polymorphism, in which the bound may recursively contain the type it bounds:
Type constructor polymorphism is another beautifully simple theory. In type constructor polymorphism, the bounds of your types may not only be concrete types, but also functions from types to types:
My take-away: so far studying type systems has been a lot of fun, though extremely challenging, and the concepts are simpler and more profound than I thought. As long as we keep type systems optional, and never let them get in the way, I think we should strive to understand and apply them in new languages.