Type systems for dynamic languages

In the past days I've studied type systems for OOP, with an eye towards making them work in a Lisp.

Cecil and its successor Diesel already do this. There, type systems are purely optional:

Diesel supports the view that static type checking is a useful tool for programmers willing to add extra annotations to their programs, but that all static efficiently-decidable checking techniques are ultimately limited in power, and programmers should not be constrained by the inherent limitations of static type checking. ... Accordingly, error reports do not prevent the user from executing the suspect code; users are free to ignore any type checking errors reported by the system, relying instead of dynamic type checks. Static type checking is a useful tool, not a complete solution

I think that's a good spirit.

Both languages support F-bounded polymorphism, which is a fancy way of saying that you allow recursive types, like T extends Foo<T>. With this simple mechanism, the expression problem can be typed, and that's something.

(Scala and O'Caml extend upon this, each in their own way (here and here), but I think they're much too complicated for what I have in mind.)