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.