Earlier quoted context omitted.
Unfortunately, there is no type inference system (that I know of) that can handle types that programmers use in dynamically typed languages on a daily basis. For example, consider the Django admin property 'list_filter' [1] or the Clojure metaprogramming functions 'proxy' [2] and 'defrecord' [3]. [1] https://docs.djangoproject.com/en/dev/ref/contrib/admin/#dja... [2] http://clojure.github.com/clojure/clojure.core-api…
list_filter seems to be a closed sum type -- why do you think it's not simple to encode or infer as a static type? I'm not sure what Proxy is used for -- but it sounds like Template Haskell can probably implement it? defrecord seems like it refers to defining new types at runtime -- which is also possible via either late type-check or Template Haskell.
String | `a
Now, this type is certainly encodable in a modern advanced type system (although most statically typed languages utilize type erasure for compilation, so you would need tagged unions (Algebraic Data Types) for this), but I cannot imagine that any language is capable of inferring such a type. Maybe OCaml, but again, we would need polymorphic variants for that.