Improve Error Messages #350

Skyb0rg007 · 2025-03-28T19:26:31Z

Description

Currently, error messages have a lot of issues. I'll use the following output to demonstrate.

- fun f x y = f (f 3) ^ " str";
stdIn:7.13-7.29 Error: operator and operand do not agree [overload - bad instantiation]
  operator domain: string * string
  operand:         'Z[INT] * string
  in expression:
    f (f 3) ^ " str"
stdIn:7.5-7.29 Error: right-hand-side of clause does not agree with function result type [overload - bad instantiation]
  expression:  'Z -> _
  result type:  'Y[INT]
  in declaration:
    f =
      (fn arg =>
            (fn arg =>
                  (case (arg,arg)
                  of (x,y) => f (f <exp>) ^ " str")))

Error messages show overload type variables when they aren't relevant.
This example only uses 3 : int; its error has nothing to do with the overloading feature.
The 'Z[INT] syntax is very confusing to new users and the information is never useful to those familiar with the language: it should not appear in error messages.
Unification errors between tuples/records include parts that do successfully unify.
In this case, the first error should be reported as a disagreement between string and int, not string * string and int * string. This is often a big problem when working with records of 5 or more fields, since the error message does not tell you which field has the type error.
CoreML is output in a very odd way.
If SML/NJ is going to print out a desugared version of the code, it should make sure it is valid and readable.
This means something like:

val rec f = fn arg1 => fn arg2 =>
      (case (arg1, arg2)
        of (x, y) => f (f <exp>) ^ " str")

(* Or *)
fun f arg1 arg2 =
      (case (arg1, arg2)
        of (x, y) => f (f <exp>) ^ " str")

ie. Include val rec or convert to fun; don't put unnecessary parentheses and indentation for fns that came from the curried arguments of a fun; make sure that variable names don't collide (use arg1 and arg2 instead of arg for both); use better indentation rules for case (ensure that the of is not de-indented relative to case).

Even better would be to keep track of the original AST for error reporting purposes but this may be harder to implement

Align error output or don't: but don't be inconsistent.
The first error message aligns string * string and 'Z[INT] * string, while the second error message does not align 'Z -> _ and 'Y[INT].
Consistently report unconstrained type variables.
The second error message uses 'Z -> _, even though the error has no relation to the domain vs. range of the function.
It should either be reported as _ -> _, or as 'a -> 'b or similar.
Handling metavars in error messages in general is an issue.

Obviously this is a big feature with many parts, but I thought that there should be a GitHub issue to document the current problems.

The text was updated successfully, but these errors were encountered:

dmacqueen · 2025-03-28T23:19:35Z

These are all good points. There is a standing list of ways that type checking error messages could be improved, and someday, I hope, improvements will be implemented. Producing good error messages, especially if they are to be easily understood by language novices, is a challenging problem. One issue that you point out is how to present the relevant code where the error occurred, or rather where the error was detected, since the actual source of the error may be somewhere else entirely. Prettyprinting the abstract syntax (type Absyn.absyn) is what we currently do. Saving the Ast syntax trees might help, but the problem is that that representation of the code is only partially parsed because of the problem of statically scoped infix declarations, so some context information (static environment) would be needed to complete the parsing of expressions and patterns occurring in the syntax tree. Another alternative might be to extract the source code text from the source file or an accumulated history of interactive input. But then there would be the problem of highlighting particular elements (e.g. variables and constants) that might be involved in the type error when the program fragment is represented as a text string.

This general problem is hard and complex, and might require the expertise of a programming psychologist or human-computer interface expert. Meanwhile there are several limited fixes we could try, and some of these will be part of a new type checker I eventually plan to write as part of the NewFrontEnd project.

There is a fairly extensive literature on the topic of how to produce good or better error messages for Hindley-Milner type inference and type checking systems. These deal mainly with how to identify exactly which program elements are responsible for the error.

Skyb0rg007 · 2025-04-01T16:50:33Z

I don't think I necessarily agree with your assessment that these require complex engineering efforts.
While some features such as better type error locality would need a different inference algorithm, all the issues listed above can be solved without any changes to the core algorithms. Errors 1-4 can be solved through a post-processing of the current error messages.

Yes, a better inference algorithm would be good too, but I chose these errors specifically because they are low-hanging fruit.

dmacqueen · 2025-04-02T17:58:51Z

The cosmetic improvement of current error messages is not complex, but requires design taste and nontrivial effort. I've thought for a while that a promising approach might be to detect an error (usually a failure of unification) and then invoke a kind of retrospective process to try to find an explanation and present a good error message. This assumes that the Ast syntax (partially parsed syntax trees) and the Absyn and perhaps the types themselves are adequately "instrumented". For instance, occurrences of type constructors now carry an origin annotation that is carried along during type inference and that can be used to identify where the type constructors were introduced in case they are involved in a unification failure. This is part of my "Culprits" idea to improve error messages, which is a simple alternative to several published proposals to produce better error messages during type inference and checking by augmenting the HM inference algorithm in various ways. I know of no good alternative to the basic (Curry-Newman-)Hindley-Milner type inference algorithm. But the problem of identifying the cause of a type error is made difficult because the point in the program where the error is detected (where a unification fails) is often not the actual cause of the error. If two type constructors do not match during unification, you could go back to the (two) points in the program where those type constructors were introduced (via being in the type of a variable occurrence), but after they were introduced they flow around the program through the unification process and sometimes the error occurs somewhere midway through that "flow" (I can supply examples). So one might need to monitor not only the "sources" of clashing type constructors but what happens to them through the course of the type inference "flow". Other complicating factors are overloaded variables like "+" and overloaded literals like "3" and the not precisely defined "scopes" in which they must be resolved.
Also, the overloading resolution takes place after type inference is completed in some scope, so we are left with
"stand-in" type "variables" like 'Z[INT] that are not yet resolved.

In (S)ML, there is also a minor issue of (what I call) "explicit" type variable and their treatment in type checking (e.g. what is their implicit binding point and scope). This was partially fixed in SML '97, in which one can optionally explicitly bind a type variable in a value declaration. Consider the following mixed example in SML '97:

fun f (g: 'a -> unit) =
    let fun 'a f (e : 'a) = g e
    in ()
    end

when type checked in SML/NJ, this produces an error message that says that 'a does not match 'a, which is a bit confusing, especially when it arrises in a much larger and more complicated piece of code where it is not so obvious what is going wrong. [Hint: it just another case of "free variable capture".]

Skyb0rg007 added the enhancement New feature or request label Mar 28, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve Error Messages #350

Improve Error Messages #350

Improve Error Messages #350

Improve Error Messages #350

Comments

Description