>>1,2
You can statically infer types ala SML, but you have to limit expressiveness of the type system. With full type inference you would struggle to implement an object system for example. Alternatively the route of Idris is to ignore inference for the sake of having a very expressive type system (e.g. dependent types) such that it can express constraints which are more meaningful, and less suffocating. Often languages achieve neither however and chart a route in the middle, having types which can be inferred, while most type them explicitly, and with limited expressiveness.