We speculate that partial revelations based on matching rather than subtyping may provide a better solution to this problem. There has much concern in the types community with the problem of type inference. However as the type systems become richer, the complexity of these systems can become very high, and the problem is known to be undecidable in some cases. Moreover, once subtyping is introduced, it is not clear whether the results returned by type inference will actually be useful to a programmer, as principal types are no longer available. As a result, it is worth asking whether full type inference for programs is a worth-while goal.
Most languages instead require programmers to over-specify the types of language constructs.
For instance, there is no reason for the compiler in Pascal to require the programmer to write down the return type of a user-defined function. The type-checker could just as easily deduce the return type. However, most languages require this sort of redundancy both to catch programmer errors and to provide better documentation to readers of the program. The functional languages ML, Miranda, and Haskell all come equipped with very powerful type-inference systems which are the result of very impressive research in types. In the case of polymorphic functions, a stronger case could be made for type inference, as type parameters can make function definitions and applications appear more complex.