Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Expand the "Unexpected existential" error message #1733

Merged
merged 4 commits into from Apr 26, 2018

Conversation

Projects
None yet
3 participants
@Octachron
Copy link
Contributor

commented Apr 21, 2018

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 comment has been minimized.

Copy link
Member

commented Apr 21, 2018

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 comment has been minimized.

Copy link
Contributor Author

commented Apr 21, 2018

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

This comment has been minimized.

Copy link
Member

commented Apr 21, 2018

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

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Apr 21, 2018

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

This comment has been minimized.

Copy link
Contributor Author

commented Apr 24, 2018

I have removed the offending adjective.

@gasche

gasche approved these changes Apr 25, 2018

Copy link
Member

left a comment

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

@gasche

This comment has been minimized.

Copy link
Member

commented Apr 25, 2018

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 Octachron force-pushed the Octachron:unexpected_existentials_msg branch from 9a08a6f to ce7ce2a Apr 25, 2018

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Apr 25, 2018

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

@gasche

This comment has been minimized.

Copy link
Member

commented Apr 25, 2018

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

This comment has been minimized.

Copy link
Contributor Author

commented Apr 25, 2018

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.)

@gasche gasche merged commit 1e59586 into ocaml:trunk Apr 26, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.