Haskell has typeclasses (http://haskell.org/haskellwiki/A_brief_introduction_to_Haske...), though. They allow inference of required type characteristics ("requires a type which can be sorted", "requires a numeric type", etc.), rather than type identity, which can solve many of the same problems.
Right, that's part of what I'm trying to implement. They're well-covered in THiH.
Typeclasses have some pitfalls though: in particular, they are not types, so you can't have a typeclass as a field in a data structure. (You can have them as part of the context of an explicit forall, eg. existential types, but those are more complicated than the average programmer can understand.)
Bruno Oliveira and Martin Sulzmann have recently done some interesting work with unifying typeclasses and ordinary algebraic data types:
But currently type inference for this is "left to a future paper", so it's not all that useful for my purposes. I suspect it may be undecidable, given the known undecidability results for System F-omega and other type systems with subtyping.
