Erlang has also had a gradual type system (and a fairly interesting one at that[0]) for a long time: http://learnyousomeerlang.com/dialyzer

AFAIK there's no optimisation based on that, just typechecking.

[0] it's interesting in that where most typecheckers restrict language semantics as they require a form of correctness proof, dialyzer is optimistic and only errors out if types are clearly inconsistent