Continuing the discussion from What are the biggest reasons newcomers give up on OCaml?:
I would expect this error message to be something like:
Error: expected type
('a, unit, string, node) format4
But got type
_ list
Is this doable? And how difficult would it be to get there?
Your proposed error message is erroneous. Consider:
type not_list = [] | (::) of int * int list
let () = Format.printf [0;1]
There is no list in sight here, and the current error message
Error: This variant expression is expected to have type
('a, Format.formatter, unit) format
There is no constructor :: within type format6
describes correctly the issue at hand: there is a mismatch between the constructor :: and the constructors that belongs to the format6 GADT.
To be a little less terse, I believe that error messages should be cautious to leave open all resolution paths. And in the case of mismatched constructor, this means keeping in mind that the real mistake might be an error on the constructor name
let f = function Some _ -> 1 | Nones -> 0
Error: This variant pattern is expected to have type 'a option
There is no constructor Nones within type option
Hint: Did you mean None?
We could try to add more hints, listing all types in scope that defines the mismatched constructors for instance, or all constructors of the expected types. However, going back to the format6 example, I find that those hints only add noise
Error: This variant expression is expected to have type
('a, unit, string, node) format4
There is no constructor :: within type format6
Hint: In the current scope, only the list type defines a `(::)` constructor.
Hint: The format4 types defines the constructor:
CamlinternalFormatBasics.Format
since the core of the error is that the function was expecting a format string. I am not sure that mentioning list helps.
In this case the :: does not appear in the code and is desugared from the list syntax. Maybe the error could say
Error: This variant expression is expected to have type
('a, unit, string, node) format4
List syntax cannot be used: there is no constructor :: within type format6
Also it says is expected to have type _ format4 but then within type format6, maybe we should mention somewhere in the error that format4 is defined from format6.
We could probably keep the original type name indeed.
Concerning the list syntax, thatâs a real pain point in error messages, but the compiler does not make any difference between 1::2::[] and [1;2] after parsing. So we cannot know if the user wrote 1::[] or [1] We could add a hint (with the hint semantic being that sometimes they convey non-useful information):
Error: This variant expression is expected to have type
('a, unit, string, node) format4
There is no constructor :: within type format6
Hint: List literal syntax [a; b; ...] is equivalent to a :: b :: ...
The other option that I have been thinking about would be to keep track of desugaring transformations in the AST as an attribute: [1;..] would be desugared into (::)(1,...)[@ocaml.sugar "list-literal"]
In the example you gave then the error message should be:
Error: expected type
('a, unit, string, node) format4
But got type
not_list
My point is that the type error message should be expressed in terms of types.
But this is neither the error happening at the type level nor a good indication of the way to fix the error.
You are asking to degrade the error message in
type t = Alea
type nearby = Ala
let f Alea = ()
let () = f Ala
from
Error: This variant expression is expected to have type t
There is no constructor Ala within type t
Hint: Did you mean Alea?
to
Error: This expression has type nearby but an expression was expected of type t
And this issue is aggravated by the fact that a constructor can belong to multiple types.
Are we sure this is a downgrade? 
Itâs clearly telling you the type doesnât match, and in the full message it will highlight the constructor Ala. If you are puzzled by this message it should only take a few seconds to jump to the definition of Ala and realize itâs the wrong type.
Yes, the same constructor can appear in multiple type definitions, and the types can even have the same name. But if both constructors with the same name are in scope, the first one is shadowed, and the only way you access it is with a variable or function that evaluates to it, in which case the compiler already gives you a type error message today without mentioning any constructor names. What I am suggesting is regularizing to this type error message in all cases.
You also gave an example of Nones i.e. just a typo, that is arguably not a type error, and we already have error reporting for âUnbound constructorâ. EDIT: in fact the error we have today for your example of _ -> Nones is arguably somewhat misleading, it says there is no constructor Nones in option, which can cause a red herring thinking about where the constructor is defined. It would be simpler to just use the âunbound constructorâ error here and make it unambiguous.
Yes. As you said yourself
if you need extra-information from remote part of a project documentation to understand the error message, the error message is a failure.
Thatâs wrong in presence of type-directed disambiguation, which is the whole point of this error message.
The current error message is accurate from the point of view of the typechecker, and follows from the rules of the type-directed disambiguation of constructors and labels. Trying to hide this part of the OCaml type system behind erroneous approximations would not do any favor to anyone.
Would you mind trying to explain why you think this is ambiguous?
I also said that âin the full message it will highlight the constructor Alaâ. In a world before we have full-fledged code extract in the error report, that clearly and unambiguously points to Ala, the existing error message makes sense. But now that we have clear and unambiguous pointer to Ala directly in the error report, itâs not really ambiguous any more to point to Ala and say that itâs not the expected type. Both pieces of needed information are provided:
Alat but we got type nearbyAnd it follows the pattern established by simpler type error messages like:
# 1 +. 1;;
Error: This expression has type int but an expression was expected of type
float
Hint: Did you mean `1.'?
Thatâs wrong in presence of type-directed disambiguation
Can you provide a little more explanation about how my suggested error message is wrong in the presence of type-directed disambiguation?
Would you mind trying to explain why you think this is ambiguous?
Because itâs adding extra details (the constructor Nones does not exist in type option, OK so where is it then?) that are not needed to solve the error. We already have an error report that can do the job by itself:
# Nones;;
Error: Unbound constructor Nones
Hint: Did you mean None?
It is not only your suggested error message that is wrong, it is your whole paragraph. The idea that there is only one type which defines a given constructor in scope is simply wrong in OCaml.
type t = Ax
type s = Ax
type u = Ax
type v = A
let f : t -> s -> u -> v -> unit = fun _ _ _ _ -> ()
let error = f Ax Ax Ax Ax
Error: This variant expression is expected to have type v
There is no constructor Ax within type v
In this case couldnât we say:
Error: expected type
v
But got type
u
Type-directed disambiguation should kick in (as you show here) for the other parameters, because the types are known at those points and the constructors are valid. But type-directed disambiguation is not relevant in the case of the last argument because the expected type is v, not one of the types that can be disambiguated. So shouldnât we fall back to the old logic and just infer the type as the last one that was defined with the constructor Ax?
Please donât. Iâd be okay if it did a fuzzy match for Ax against the valid constructors in type v and offered Hint: did you mean âAâ? However, suggesting that I meant to use a type that I was not meaning to use is just going to add to my confusion.
Note that this is the current behavior, but the fuzzy matching is disable for constructors or fields with less than 3 characters to avoid too many false positive:
type t = Abc let f Abc = ()
let () = f Abd
Error: This variant expression is expected to have type t
There is no constructor Abd within type t
Hint: Did you mean Abc?
Seems like it would help if that disabling only happened for types with enough constructors that âtoo many false positivesâ is an actual problem that can happen.
Isnât this the way type errors already work in OCaml? It doesnât suggest that you really meant to use this or that type, it just says that this type was expected but that type was found. My suggestion is to just regularize type errors so they all follow a predictable pattern. And if you take a look at the initial message in the thread, you can understand why I am trying to simplify that message, right?
OK, let me make one adjustment, inspired by Scala 3âs nice error messages:
File "./test.ml", line 6, characters 23-25:
6 | let error = f Ax Ax Ax Ax
^^
Error: expected type
v
But got
Ax : u
Regarding type-directed disambiguationâin the case of a straight-up type mismatch, disambiguation doesnât matter any more. Thereâs nothing to disambiguate when the candidate types are {t,s,u} but the required type is v. So we might as well fall back to the old algorithm for inferring the type. It will at least make it clear to the reader that Ax is definitely a mismatching type.
Iâm not familiar with Scala3 error messages, can you show or point at relevant examples?
I am sorry, but would you mind listening to what I have been explaining to you since the start of this strange discussion?
I can see that the name type-directed disambiguation might have induced you in error, but I assure you that the error is a type-directed constructor resolution error, not a type error mismatch error.
Since the introduction of type-directed constructor resolution, constructors (and fields) are not uniquely
associate to a type. And when a constructor resolution fails it doesnât make sense to pick arbitrarily one non-matching type in order to fail in a familiar but unrelated way.
This is what happens today in OCaml typechecker. This is a fact, and not a point that you can discuss.
Rather than trying to fight the reality of OCaml type system to make it fit your perception, I believe that you would better spend your time and energy explaining what you find so confusing in the initial error message. Because, yes, my point of view is biased (after all I am one of the author of this error message), but I fail to see what is so problematic with
Error: This variant expression is expected to have type
('a, unit, string, node) format4
There is no constructor (::) within type format6
maybe corrected to
Error: This variant expression is expected to have type
('a, unit, string, node) format4
There is no constructor (::) within type format4 = format6
Hint: List literal `[x;...] can also be read as `x:: ... `.
Indeed, the error message is to the point, it indicates that we had an expected type and explicit variant constructor ::, and that the two cannot match.
Even reading the initial report, I fail to see how your proposed correction would help.
because the core part of the error, that we expected a format string and got a mismatched constructor is already here.
We clearly ought to make clearer the connection with the list literals, maybe we can reword the mismatching constructor error message to make it clearer that we compared the present constructors with the one available in the expected type; but there is no reason to evoke the list type here.
Maybe we could reword the error message to:
Error: This variant constructor `(::)` is expected to have type
('a, unit, string, node) format4
There is no variant constructor (::) within type format4 = format6
Hint: List literal `[x;...] can also be read as `x:: ... `.
or if the information about the sugared list literal syntax was available:
Error: This list literal is expected to have type
('a, unit, string, node) format4
There is no list constructor (::) within type format4 = format6
('a, unit, string, node) format4:: is a constructor (too), they think that is is (only) a infix operator. So there is no connection to a list.[So the information they read out of the error message is âError: This variant expression is expected to have SOME OTHER TYPEâ with no idea how that type should look like or whatâs wrong.
The message would be less confusing if it just pointed at the variant expression and said something like âThere is something wrong!â