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

Add two tests for -short-paths with existential types #12340

Merged
merged 1 commit into from
Jul 7, 2023

Conversation

shym
Copy link
Contributor

@shym shym commented Jun 29, 2023

As $ is used to prefix existential types, favor an alternative if it exists when -short-paths is enabled by using exactly the same penalty as for the _ prefix.

On the following program:

type _ ty = Char : char ty
type pair = Pair : 'a ty * 'a -> pair

let f = function
  | Pair (Char, x) -> x + 1

$ ocamlc -short-paths reported before:

5 |   | Pair (Char, x) -> x + 1
                          ^
Error: This expression has type $Pair_'a
       but an expression was expected of type int

while it now reports:

5 |   | Pair (Char, x) -> x + 1
                          ^
Error: This expression has type char
       but an expression was expected of type int

I'm not sure whether $ can appear in other cases than existential types.

@shym shym force-pushed the short-non-existential branch 2 times, most recently from 71e684a to ad1704f Compare June 30, 2023 10:33
Copy link
Contributor

@trefis trefis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

-short-paths is surely going to be completely rewritten soon, but this patch is very simple, reasonable and comes with a test, so let's merge it?

containing double underscores "__" incur a penalty of $+10$ when computing
their length.
warning messages. Identifier names starting with an underscore "_", a
dollar "$" or containing double underscores "__" incur a penalty of
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this be escaped?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

tools/texquote2 does escape it automatically.

@Octachron
Copy link
Member

@trefis I was a bit worried that the shortening logic might also happen within scope escape message leading to variations on int would escape its scope and friends.

Did you have the time to investigate this potential issue?

At the same time, many GADTs error messages are already worsened by -short-paths, so it might be not worth it to invest too much time.

@trefis
Copy link
Contributor

trefis commented Jun 30, 2023

So errr...
I used a slight variation of the given test:

type _ ty = Char : char ty
type pair = Pair : 'a ty * 'a -> pair

let f = function
  | Pair (Char, x) -> if true then x else 'd'

And got this before this PR:

$ ocamlc -version
4.14.1
$ ocamlc /tmp/sp.ml
File "/tmp/sp.ml", line 5, characters 35-36:
5 |   | Pair (Char, x) -> if true then x else 'd'
                                       ^
Error: This expression has type char but an expression was expected of type
         'a 
       This instance of char is ambiguous:
       it would escape the scope of its equation
$ ocamlc -short-paths /tmp/sp.ml
File "/tmp/sp.ml", line 5, characters 35-36:
5 |   | Pair (Char, x) -> if true then x else 'd'
                                       ^
Error: This expression has type $Pair_'a
       but an expression was expected of type 'a 
       This instance of $Pair_'a is ambiguous:
       it would escape the scope of its equation

Unless something major has changed in this area since 4.14, I'd say it can't be making things worse.

@Octachron
Copy link
Member

Octachron commented Jun 30, 2023

Thanks for the example!
And testing with this PR, it seems that we go back to

Error: This expression has type char but an expression was expected of type
         'a 
       This instance of char is ambiguous:
       it would escape the scope of its equation

with -short-paths because the previous behavior was due to the fact that '$'<'a' in lexicographic order. In other words, the penalty hides the existential in the escape error message, which I find is a disadvantage.

@shym
Copy link
Contributor Author

shym commented Jul 6, 2023

If that’s not always an improvement, maybe we should forget about it.
Would it still be useful to add the two tests to the test suite, as a way to guide the rewriting of -short-paths?

@Octachron
Copy link
Member

Adding the two examples in the short-path test does sound like a good idea.

@shym shym changed the title Penalize types starting with $ with -short-paths Add two tests for -short-paths with existential types Jul 7, 2023
@shym
Copy link
Contributor Author

shym commented Jul 7, 2023

I’ve renamed this PR and kept only the addition of the two tests.
I imagine a changelog entry is not really relevant for additional tests.

^
Error: This expression has type "$Pair_'a"
but an expression was expected of type "int"
|}]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would add a comment that we would like short-path to print char rather than $Pair_'a in this context.

but an expression was expected of type "'a"
This instance of "$Pair_'a" is ambiguous:
it would escape the scope of its equation
|}]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While in this context, it seems better to keep the existential type.

@@ -34,3 +34,35 @@ Line 7, characters 9-18:
Error: This expression has type "c"
It has no method "bar"
|}]

type _ ty = Char : char ty
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A short section title would be good to keep track of what those tests are asserting. Something like

(** Known issue: how to print existential types with equality in scope? *)

@Octachron
Copy link
Member

I think that a change entry "testsuite: collect known issues with current -short-paths implementation" could be useful, after all good test cases are a real necessity when improving error messages.

Add two tests combining `-short-paths` with existential types to help
guide future revisions of the `-short-paths` feature

Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr>
@shym
Copy link
Contributor Author

shym commented Jul 7, 2023

Thank you for all those suggestions. I’ve put you as a co-author, at that stage :-)

Copy link
Member

@gasche gasche left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(If @Octachron is co-author then you need another approval.)

@Octachron Octachron merged commit e869a1d into ocaml:trunk Jul 7, 2023
9 checks passed
@shym shym deleted the short-non-existential branch July 10, 2023 08:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants