I stumbled across this while looking for solutions to the expression problem:
Pure Subtype Systems: A Type Theory for Extensible Software [PDF] by DeLesley Hutchins, 2009.
Hutchins bases his type theory on subtyping rather than typing.
As far as the expression problem goes, one solution is to support late-binding for types. The author points to the gbeta programming language, which supports this feature.
Of the solutions I’ve seen, I think this is probably the best. Besides actually solving the problem, it also has the benefit of being easy to understand.