Lambda the Ultimate

I find myself in need of a type system which can deal well with types that are unknown at compile time, by doing as much static type-checking as possible and then inserting downcasts to deal with unknown types at runtime. Is anybody aware of such a system already in use? Let me motivate this by a short example in some functional pseudo-code:

useNumber(number) = number + 2
useList(list) = head(list)
googleURL = "http://api.google.com/GoogleSearch.wsdl"
google = Webservice(googleURL)
results = google.search("testing")
a = useNumber(results)
b = useList(results)


Clearly the type of a dynamically-generated proxy like google may be, in general, unknowable at compile time. The obvious way to handle this is to use a Univ type which is downcast, either implicitly or explicitly, as needed. That approach seems to be typical for current languages from Java to Haskell. However I'd like to go a bit further and reject programs like the above where it's clear that some variable (in this case results) could never satisfy the constraints on its type.

This sounds to me (perhaps deceptively) like a simple problem which someone is bound to have solved already, but if so I have yet to find the solution in the literature. Maybe that's because it's so simple that it's not worth publishing, and I just need to think about it a bit.

Here are some examples of ideas I have reviewed and rejected:

• Static Typing Where Possible, Dynamic Typing When Needed -- a provocative title, unfortunately not borne out by the content of the paper.
• Cartwright and Fagan's "Soft Typing" (1991). If I have understood this paper, soft typing cannot distinguish between programs which it merely cannot prove are correct and programs which are obviously incorrect. In both cases, types simply fail to unify. However I would like to make such a distinction, so that at least some programs can be definitively rejected at compile time, and I don't mind forcing programmers to make some concessions to the type system to allow this.
• Boo is a language I've seen mentioned as supporting both static and latent typing with type inference. Based on a cursory review of their documentation, it seems they just have a Univ type with implicit casting (and a somewhat ad hoc type system in general).
• HaXe is another such language, which I rejected when I saw that their idea of type inference is "the first time the function is used, the type of the parameter will be set to the type it was used with".

Thank you for your help.