The following code indicates an incorrect error diagnostic:

type t = T;;

let rec g (x:int) = 
  (let (aT:t) = f x in ())
and f x : unit = ();;

Line 5 characters 17-19:
This expression has type unit but is here used with type t.


The function f is explicitly declared with return type unit,
and clearly returns the unit value: there is no error
in f, and certainly the () is _not_ being used 'here'
with type t. 

The error may be considered to be in the call of f, 
in the function g, or it may be considered to be 
in the explicit declaration of the return type of f,
which clashes with the infered return type,
or even in the whole of f,
but it cannot be in the body of f: f is internally
consistent.

In my actual code, I got an error
in a 5000 character expression, and it took three
days to figure out the error wasn't in that expression
at all. 

I can guess how the problem arises in the inference
algorithm, but now I can't figure out a policy for tracking
down type errors (since they can no longer be trusted).
I found previously that adding explicit types helped
isolate errors, but in this case it didn't.

-------------------------------------------------------
John Skaller    email: skaller@maxtal.com.au
		http://www.maxtal.com.au/~skaller
		phone: 61-2-96600850
		snail: 10/1 Toxteth Rd, Glebe NSW 2037, Australia