[Caml-list] Improved type error messages for Ocaml

["Arthur Charguéraud" <arthur.chargueraud@inria.fr>]

[-- Attachment #1: Type: text/plain, Size: 3148 bytes --]

Dear OCaml users,


It is my pleasure to announce the beta release of my patch for improved 
type error messages.

|    opam switch 4.02.2+improved-errors|


Quick demo:

*** With "ocamlc" ***


let _ = List.map (fun x -> x + 1) [2.0; 3.0]
                                    ^^^
Error: This expression has type float but an expression was expected of 
type int.

This message is very confusing to the user who intented to write: (fun x 
-> x +. 1.)


*** With "ocamlc -easy-type-errors" ***


let _ = List.map (fun x -> x + 1) [2.0; 3.0]
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Error: The function `List.map' cannot be applied to the arguments provided.

    | Types of the expected arguments:    | Types of the provided arguments:
---|-------------------------------------|------------------------------------
  1 | 'a -> 'b                            | int -> int
  2 | 'a list                             | float list


This new message show all the types involved, and does not attempt to 
guess whether the user intended to write [2; 3]  or intended to write 
(fun x -> x +. 1.); Trying to guess is a bad idea, because roughly half 
of the time the guess is wrong, and it just adds more confusion.



Many more (cool) demos are available from the following sources:

  * paper:
    http://www.chargueraud.org/research/2015/ocaml_errors/ocaml_errors.pdf
  * slides:
    http://www.chargueraud.org/talks/2014_09_05_talk_ocaml_errors.pdf
  * video: https://www.youtube.com/watch?v=V_ipQZeBueg



How it works (short version):

When the flag "-easy-type-errors" is activated, the compiler behaves 
exactly as usual, except when a top level definition fails to 
type-check. At such point, the definition is type-checked again, using a 
slightly modified unification algorithm, able to produce messages that 
are (I argue) more informative for locating the error. The patched 
compiler is thus able to provide alternative error messages with zero 
performance overhead on successful compilations. For ill-typed programs, 
the new typing algorithm may be slightly slower than the original one 
(as it performs a larger number of generalizations), but it should never 
be orders of magnitude slower.

Pretty much all of OCaml is supported, with the notable exceptions of 
GADTs (by lack of time of expertise), and record field name overloading 
(due to the fact that it depends on the order in which unifications are 
performed). Note that top-level definitions involving such features will 
still compile properly, as long as it they do not contain any type 
error; if they do, then the error message will likely be uninformative, 
in which case the flag "-easy-type-errors" needs to be turned off.


If you like this patch and would like to see it one day integrated in 
the main distribution, please post feedback on the mailing list, to 
convince the developers and myself that it is worth further investment. 
I am especially interested in feedback on the use of the new error 
messages in the context of teaching OCaml.


Enjoy!

+
Arthur

[Many thanks to Armaël Guéneau and Gabriel Scherer for their help with 
the opam packaging.]



[-- Attachment #2: Type: text/html, Size: 5319 bytes --]