Type error with partial application and optional argument

[mbouaziz]

Instrumented with bisect_ppx (since v2), this code:

let f y ?(x=0) z = x + y + z

let l = List.map (f 1) [1]

produces this type error:

File "bin/main.ml", line 3, characters 18-19:
3 | let l = List.map (f 1) [1]
                      ^
Error: This expression has type ?x:int -> int -> int
       but an expression was expected of type 'a -> 'b

There are several ways to avoid it:

1. change argument order: let f ?(x=0) y z;
2. explicit optional argument: (f 1 ?x:None);
3. function wrapper: (fun z -> f 1 z);
4. annotation to ignore specific location.

I have a first issue though: there is some code I cannot change.
Given that I control the surroundings, I could still:

• add an exclusion (but it can't be defined at the expression level), or
• write a patch and apply it before compiling (I don't need to maintain it because the code is frozen).

Second issue for my project: by default code coverage instrumentation is not enable, and code coverage is not run on the CI, so external contributors may not know about this issue and may break coverage instrumentation even though everything else is fine.
Since it happens only very rarely, I can fix it myself, but it doesn't feel very satisfying.

The best solution would be to fix bisect_ppx to do the rewriting whenever needed but I don't see how given that ppx's don't have access to types, right?

[aantron]

The best solution would be to fix bisect_ppx to do the rewriting whenever needed but I don't see how given that ppx's don't have access to types, right?

Yes. This is a consequence of Bisect_ppx instrumenting "exit edges" (in the control-flow graph sense) of application expressions, to indicate whether functions return. This can interfere with how optional arguments are eliminated.

I ran into this case while implementing that instrumentation, but decided it is rare enough and easy enough to fix any code that triggers it., whether by applying to the optional argument explicitly, or with [@coverage off].

I understood that this isn't true in the case you are facing right now. What would be most helpful to you?

To my knowledge, there is no way for Bisect to know whether any particular application will trigger this.

[mbouaziz]

That's what I expected, I opened the issue mostly for documentation and being able to link to it 😉

For frozen code, I'd like to be able to define exclusions at the expression level, e.g. using the location number used by the instrumenter (I'd have to look at the .pp.ml file, I don't know if there's anything easier), or using the offset in the file.
I reckon this is brittle and may break with an update of bisect_ppx, or even its dependencies, or if I'm allowed to reformat the code, but that shouldn't be often so I'm ok with that.

For code under development, I guess I could still add a CI step to compile the instrumented code but not run the tests.

[aantron]

Have you already considered excluding the top-level value that contains the call site using the instructions here? This would only be useful if the top-level value is bound to an expression that isn't very complicated, of course.

[mbouaziz]

I did. These patterns have the annoying tendency to happen in the middle of big values: https://gitlab.com/tezos/tezos/-/merge_requests/1714/diffs?commit_id=daf5dd10eebf7a46da0b5db3a9cbdf629a57b030, so I'll lose quite a bit of precision.

Anyway, I'll close this issue as there's no magical solution on bisect_ppx side.
The best I can do if I want to keep precision high is implement exclusion at offset level.

[aantron]

Another option might be a command-line flag that disables instrumentation of application expression exit edges.

[ejgallego]

I've run into this which makes bisect_ppx unusable with Coq. I don't see easy workarounds.

Note that this is a regression as bisect_ppx 1.4.2 does work fine with Coq ; IMO this issue should be reopened.

[aantron]

I propose to either

1. Disable this instrumentation by default, and make it opt-in by a flag to the PPX.

2. Leave it enabled by default, but make it possible to opt out.

@ejgallego do you have a preference for either one of these?

[aantron]

I looked at your commit message and "pretty bad, no other choice" is definitely not the kind of ergonomics Bisect_ppx is aiming for, so please let me know :) I have to address it in Bisect.

[aantron]

I'm leaning towards opt-in, as then Bisect can be used with no surprises, and if someone learns about the option, they learn about the risk at the same time, and they will know what they have changed to trigger the error if it occurs.

[ejgallego]

Hi @aantron , this was not so bad after all, thanks for having a look. I am mostly afraid of the response this could have with the rest of Coq developers when they find the CI is failing because of this.

But given the size of the changes it turns out it was not as bad as I was expecting [see updated commit message :)]

IMO we could live with any choice you propose, but yeah, this should be at least added to the FAQ.

Personally I think that keeping it on by default is fine.

[mbouaziz]

Another solution could be to eta-unexpand those cases. Are there side effects I don't see?

[ejgallego]

By the way, we are getting magic numbers errors (for example https://gitlab.com/coq/coq/-/jobs/540786885 )

Any idea what could be going on [my previous setup for Coq was on the 1.x branch]

These are the corresponding changes to Coq, we are using the freshly-added dune support coq/coq#12259

[aantron]

Thanks. I noticed the change in the commit message :P

As @mbouaziz has pointed out, this will be an ongoing problem for Coq, most likely, though.

In a codebase that has functions whose call sites can trigger this bug, a developer or contributor could trigger it in CI without ever observing it locally, and there is no easy way for them to predict this. I think this will be an annoyance, especially since I expect most contributors don't care about coverage or want to administer it or deal with it in any way — it should just be a separate aspect of code maintenance, as orthogonal and automated as possible.

So I'll go with disabling it, and add a loud note to the README about enabling it.

[ejgallego]

So I'll go with disabling it, and add a loud note to the README about enabling it.

Ok, sounds good thanks, still we may try to enable it in Coq for now, I need to check if Dune support does allow to set the parameter tho.

[aantron]

Another solution could be to eta-unexpand those cases. Are there side effects I don't see?

@mbouaziz What do you mean by this? Also note that IIRC, and AFAIK, Bisect can't detect these sites specifically, so any solution will have to be applied to all application expressions.

@ejgallego That error doesn't look like a magic number mismatch, but perhaps an empty or otherwise truncated file. Not immediately sure what would cause it. I've never observed it before.

[ejgallego]

@ejgallego That error doesn't look like a magic number mismatch, but perhaps an empty or otherwise truncated file. Not immediately sure what would cause it. I've never observed it before.

I will open a new issue about it, sorry for the noise here.

[SkySkimmer]

Are these bugged spots exactly the ones pointed out by warning 48 "Implicit elimination of optional arguments" or is there a difference?
For the OP examples I can find no difference.

[aantron]

I believe they are the same.

[aantron]

Your question made me think that there might be some other way to rewrite the expressions, so I am considering that now.

[aantron]

The above commit changes instrumentation of applications f x with instrumentation point n from

let ___bisect_result___ = f x in
___bisect_visit___ n;
___bisect_result___

to

___bisect_post_visit___ n (f x)

where

let ___bisect_post_visit___ n result =
  ___bisect_visit___ n;
  result

is defined globally.

This seems to interact better with type inference in the presence of optional arguments when it is nested in larger application expressions. It seems to fix the issue at least for @mbouaziz's example, which I added as a test case.

It also seems to trigger the optional argument elimination warning if and only if the uninstrumented code triggers it (note: seems).

@ejgallego, would you mind trying Bisect_ppx master on Coq from before your patch?

[ejgallego]

@ejgallego, would you mind trying Bisect_ppx master on Coq from before your patch?

Sure! With current Coq master, and bisect_ppx from master things seem to work correctly indeed!

[aantron]

The fix is now out in Bisect_ppx 2.4.1.

[mbouaziz]

Btw I can confirm I don't encounter the issue any more with 2.4.1, thanks a lot!

[aantron]

Great, thanks for confirming!