John Max Skaller wrote (on 13-12-00 11:51 +1100):
> In Ocaml, terse expression with the _option_ of adding a type
> constraint isn't that unreasonable. The real problem is that
> the inference engine isn't smart enough to remember _how_ it
> deduced a type, and report _both_ locations when there is a
> conflict. I have a suspicion this is non-trivial: probably
> worth a PhD. :-)

Or at least a Master's. And by a fortuitous coincidence, one of our students
Bastiaan Heeren wrote a thesis on this essentially this topic. His type
inferencer uses heuristics to improve the quality of type-error messages; for
example, if x gets assigned type A in 2 places, and type B in only 1 place,
then the inferencer reports the latter as the source of the type conflict.

You can find his page, and the thesis, here:

  http://www.cs.uu.nl/people/bastiaan/

There is also some work by Dominic Duggan and Frederick Bent on "type
explanation":

  D. Duggan and Frederick Bent.  Explaining type inference.  Science of
  Computer Programming, 27,1, June 1996.

  Dominic Duggan. Correct Type Explanations  ACM ML Workshop, Baltimore,
  Maryland, September 1998.

and an implementation, SML/E: A Type Explanation Facility for Standard ML:

  http://guinness.cs.stevens-tech.edu/~dduggan/Public/Smle/index.html

-- 
Frank Atanassow, Information & Computing Sciences, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-3261 Fax +31 (030) 251-379