BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/focus.ps.Z
       ENTRY:: November 8, 1995
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Debugging Type Errors (Full version)
        TYPE:: Preprint
      AUTHOR:: Bernstein, Karen L., and Stark, Eugene W.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 516-632-8444 <stark@cs.sunysb.edu>
	DATE:: November, 1995
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~stark/REPORTS/debugtype.ps.gz

ABSTRACT::

Compilers for programming languages such as Standard ML are able to
find many programming errors at compile time, however the diagnostic
messages from the type inference algorithm do not always clearly
identify the source of type errors.  We argue that an extended type
definition, which assigns types to open expressions as well as closed
expressions, can serve as the basis for a programming environment that
helps programmers debug type errors.  We present such a type
definition, which is closely related to the Damas/Milner definition,
but which in addition provides principal typings for open expressions.
We present an algorithm that performs type inference with respect to
our type system and give a simple direct proof of its correctness.
Finally we describe a prototype implementation.