[shadowfox]

There is always idea of Gradual Typing [1] which has been implemented with varying degrees of success. There are also a large set of static analysis theories/tools which can help here.

It is also worth noting that if you dont want (global) type inference, you can get far in a language with permissive casting, type annotations and local inference. The results aren't a panacea though.

> Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing.

I am not quite sure what you mean by this. Care to elaborate? (In general, with inference systems, missing type information is hard(ish) to localize. So pointing out where exactly a type error occurred is non-trivial)

[1] https://en.wikipedia.org/wiki/Gradual_typing

[tailrecursion]

I'm thinking of a system with valueset inference where valuesets are not necessarily disjoint. So the system may infer that a return value is the disjunction {INTEGER | REAL}.

In order to get precision in checking, a lot of computation needs to be done so the compiler relaxes the precision when facing large disjunctions (networks) of constraints.

Dynamic checks are inserted as necessary but a system that relaxes when things get hairy can't guarantee that it will find all errors at compile time.

The idea is similar to Soft Typing of Cartwright and others, but they were thinking of an interactive system, some kind of programmer's aid. If I recall they ran into problems giving reasonable error messages.

[tomp]

The problem with this idea, at least compared with current implementations of Haskell and OCaml, is that it requires runtime type information. Right now, Haskell and OCaml both perform erasure, and the only kind of runtime type information used is for the GC, but if you have two ADTs with identical structure (number of branches, payloads) but different names (i.e. they are different types), they will be encoded in the same way. So, in order to tell them apart, you would need some additional type information, which would require changes to compilers and would probably performance characteristics.