Expand the "Unexpected existential" error message

[Octachron]

Currently when the type-checker encounters unexpected existentially quantified types, e.g.

   type any = Any : 'any -> any
   let Any x = Any ()
   class c (Any x) = object end
   class c = object(Any x) end

it emits the following errror message

Error: Unexpected existential

If this terse message is clear from the perspective of the type-checker, it may seem mysterious from an user perspective.

This PR proposes thus to focus on the user perspective in this error message by making clear in which contexts existential types are not allowed and from where the problematic existential types come from:

let Any x = Any ()

Error: Existential types are not allowed in toplevel bindings,
but this pattern introduces the existential type $Any_'a.

class c (Any x) = object end

Error: Existential types are not allowed in class arguments,
but this pattern introduces the existential type $Any_'a.

class c = object(Any x) end

Error: Existential types are not allowed in self patterns,
but this pattern introduces the existential type $Any_'a.

The error message directly refers to an existential type name if one is available, otherwise it names the constructor itself:

type other = C: _ -> other
let C x = C ()

Error: Existential types are not allowed in toplevel bindings,
but the constructor C introduces unnamed existential types.

[yallop]

This looks like a clear improvement.

One case that's not handled correctly yet: existential types are not allowed in let...and bindings. For example, OCaml rejects the following program

let Any _ = Any ()
and () = ()
 in ()

and with this PR, the error is misreported as a problem with a toplevel binding:

Error: Existential types are not allowed in toplevel bindings,
but this pattern introduces the existential type $Any_'any.

[Octachron]

This is a great point, thanks for pointing the issue. I have fixed the error message in all case where existentials are not allowed inside a local let-binding, e.g.

let () =
  let Any x = Any () and () = () in
  ()

Error: Existential types are not allowed in "let ... and ..." bindings,
but this pattern introduces the existential type $Any_'a.

but also

let () =
  let rec Any x = Any () in
  ()

Error: Existential types are not allowed in recursive bindings,
but this pattern introduces the existential type $Any_'a.

let () =
  let[@attribute] Any x = Any () in
  ()

Error: Existential types are not allowed in presence of attributes,
but this pattern introduces the existential type $Any_'a.

and

class c = let Any _x = () in object end

Error: Existential types are not allowed in bindings inside class definition,
but the constructor Any introduces unnamed existential types.

[gasche]

Nitpicking, I don't like "unnamed existential types", I think you should just say "existential types" when you cannot get a specific name.

[Octachron]

I will remove the unnamed adjective; but I would like to convey the notion that all existential types were left unnamed in the definition of the constructor. Do you have any idea? (I imagine that anonymous also does not fit)

[Octachron]

I have removed the offending adjective.

[gasche]

Approved in principle. Could you fix the conflict and rebase?

[gasche]

cc @Armael: there is no need for you to work on this PR, but it is similar to work that you did adding explanation markers, so I thought you may be interested.

[Octachron]

The conflict has been solved and the reviewers have been credited.

[gasche]

I had a look at the code again and I realize only now that I have an implementation question: why are we exposing this somewhat-weird existential_name function to compute user-friendly names from the field cstr_existentials, instead of having cstr_existentials contain the user-friendly names in the first place, which would be easily obtained by applying the transformation in typing/datarepr.ml:constructor_existentials, and, unless I am mistaken, would result in code with exactly the same behavior?

[Octachron]

Do you mean expanding the Tvar name in datarepr.ml? It could work but then both instance_constructor and the unexpected existential error path would have to extract back the string name from the type_expr which is unusal by itself (the only other part of the typechecker that seems to look at the content of this name is Printtyp). Thus, I am not sure if it would make the code less weird/specific than having a special function for computing user-friendly existential type names.

(Replacing the type_expr itself in cstr_existentials by the user-friendly string names seems like it would involve quite a lot of complication in the type copies perfomed by instance_constructor.)