Re: Typing problem

[Pierre Weis <Pierre.Weis@inria.fr>]

> We recently found a quite annoying problem with the typing system in
> ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
> people might be be interested however.
> 
> The problem is summarized in the following code:
> 
> First let's define two types:
> type t1 = (?l:int -> unit -> unit)
> type t = Toto of t1
> 
> Then the function:
> let f1 g =
>   g l:3 ();
>   (Toto g);;
> 
> This function doesn't compile and the compiler error message is somewhat
> cryptic at first sight:
> File "toto.ml", line 11, characters 8-9:
> This expression has type int -> unit -> 'a but is here used with type
>   t1 = ?l:int -> unit -> unit

Thank you very much for pointing out this interesting problem: I'm
sure there is room for improvement here for our new label compiler.

If you use the -modern option of the compiler you would get a much
clearer message, namely:

# let f1 g =
    g l:3 ();
    (Toto g);;
This expression has type l:int -> unit -> 'a but is here used with
type
  t1 = ?l:int -> unit -> unit

This clearly states that the optional status of the label is involved
in the problem.

Hence, a language level fix could simply be to allow the user to write
the question mark with the label as:

let f1 g =
    g ?l:3 ();
    (Toto g);;

Now, in conjontion with the -modern option, this would be perfectly clear to
understand why g l:3 is rejected while g ?l:3 is not.

Unfortunately, this last program is not yet handled properly by the
compiler, since it causes an assertion failure into the typechecker:

# let f1 g =
      g ?l:3 ();
      (Toto g);;
This expression has type ?l:Uncaught exception: File
"typing/printtyp.ml", line 0, characters 6649-6661: Assertion failed

> We would very much like to see this clearly documented in ocaml 2.99
> reference manual, as it is a serious change in the behavior of the
> typing system. Determinism is lost, as typing f1 would succeed if typing
> was done in reverse order (from last line to first line).
> Perhaps also a different error message from the compiler would help in
> detecting such problems.

I don't think that determinism is lost, in the sense that the compiler
always output the same answers! But you're right to mention that this
would be another way to test in which order in which the type-checker
type-checks the sub-expressions of a program.

You're also right in that we always would like better and better error
messages, I would say particularly for the last program I wrote: we
would very much like the compiler not to fail to print the error
report!

No doubt that this erroneous error message will be corrected before
the experimental 2.99 version will turn into a stable 3.0 version of
Objective Caml. Also, may be Jacques could tell us what is his opinion
about the optional labels status in expressions (as in g ?l:3).

Best regards,
-- 
Pierre Weis

INRIA, Projet Cristal, http://pauillac.inria.fr/~weis