The difficulty with type errors partly arises out of inference. The program assumes NOTHING about the type of the expressions and instead collects constraints

The difficulty with type errors partly arises out of inference. The program assumes NOTHING about the type of the expressions and instead collects constraints as it descends into sub-expressions. Once it has finished collecting constraints for the all the sub-expressions it attempts to satisfy those constraints. If the constraints can't be satisfied there are two problems. First, you have to know where you got the constraint from. This is fairly easy to solve in implementation you can tag the constraints for example. Second, is that the way in which the constraint "fails" or is unsatisfiable doesn't always give you enough information. For example: \x -> if x then x else 1 Here the constraints basically say that x has type Bool and 1 has type Int. This is obviously wrong because the `if x then x else 1` has to be either Bool or Int. Now the question is, which one is wrong? Is the use of the second x wrong or is the use of the 1 wrong. You can't know so you have to report something and this is only a trivial example. [edit]: I said "mostly" but I changed that to be "partly" because type systems like Haskell's are very complex and in some cases type inference is undecideable (rank n polymorphism) so that obviously makes reporting an error very hard :)