And it turns out, the theory behind that looks simpler, and thus sexier:
(types) T ::= (K K*)I like the definition of types: a type's the application of a constructor to zero or more other constructors. Constructors may be variables (X), classes (C), or functions taking zero or more parameters and returning a type. (So you basically have a lambda calculus at the type-level.) A type parameter is a variable constructor with zero or more parameters, optionally bounded to a class type with zero or more type arguments. Class definitions are parameterized over zero or more type parameters, and extend zero or more existing classes. (I'm taking some liberties with adding multiple inheritance, hoping it doesn't mess up the theory. :P) Method definitions are, as usual, parameterized on the type- and term-level and have a result type.
(type constructors) K ::= X | C | (P* => T)
(type param defs) P ::= (X P*) | (<: (X P*) (C K*))
(class defs) D ::= DEFCLASS (C P*) ((C K*)*)
(method defs) M ::= DEFMETHOD (m P*) ((param T)* -> T)
It's kinda embarrassing to post this stuff here, since I'm so bad at type theory, but I think I can make it work. One insight giving me this faith is that none of this stuff survives till runtime: at runtime, only concrete instantiations, such as List