Lwt: PPX bug when a binding is type constrained with OCaml >=4.06

[let-def]

The issue was discovered by @gabelevi and reported in https://github.com/ocaml-ppx/ppx_tools_versioned/issues/4 (however I don't think ppx_tools can do anything about that and that it should be handled in each ppx rewriter).

Prior to 4.06, let x : t = u was parsed as let x = (u : t): type constraint is on body.
Starting with 4.06, it is parsed as let (x : t) = (u : t): the constraint is duplicated on pattern and body.

So let%lwt x : t = u in v is now turned into something like (intentionnally simplified :P) Lwt.bind (u : t) (fun (x : t) -> v) (instead of Lwt.bind (u : t) (fun x -> v) as in previous versions of OCaml).

The constraint can't be correct: the type of the pattern is out of lwt, the type of the expression in lwt ('type_of_pattern Lwt.t).
I am not sure what the proper fix is, but dropping the constraint from the pattern would at least restore previous behavior.
It shouldn't always be dropped: the new case only applies when the input is directly an identifier.
In particular, let (x : t) = u is parsed as let (x : t) = u, only let x : t = u is rewritten to let (x : t) = (u : t).

[aantron]

@let-def do you know which PR this was done in in the compiler? This seems like a somewhat ill-conceived change at first.

[aantron]

It doesn't look like type constraints let%lwt x : foo = ... worked correctly to begin with, as the type had to be foo Lwt.t instead of foo, which is misleading, because the type of x is foo. I suppose we could parse the type AST to check for foo Lwt.t, but that won't help in general, say when Lwt.t is rebound in an IO module, Lwt is used through some wrapper library, or Lwt.t is aliased to promise, etc. So, given that we can't do a thorough job here, perhaps maybe we shouldn't support this at all?

We could have the PPX emit a warning if it detects this construct. I think it would only work in 4.06, because before 4.05 we can't reliably distinguish an unsupported constraint on the pattern from an unsupported constraint on the expression. So, this also seems not very attractive.

Opinions welcome.

[let-def]

The change has been implemented in: https://github.com/ocaml/ocaml/commit/fd0dc6a0fbf73323c37a73ea7e8ffc150059d6ff and discussed in https://caml.inria.fr/mantis/view.php?id=7344 .

[let-def]

since lwt (x : t) = ... works as expected, my suggestion would be to make lwt x : t = ... behave the same.
Either by detecting the case where the ast as the shape (x : t1) = (expr : t2) where t1 == t2 and they have ghost locations (... reverse engineering the job of the parser) or maybe changing the behavior of the parser upstream, however I suspect this behavior is on purpose and affect typechecking.

[Drup]

That's an interesting issue. The parser doing some fancy duplication is not very nice, to say the least.
I would propose to:

1. Open a bug on mantis to make sure this behavior is going to stay. This really shouldn't be done at the parser level, so we might be able to convince the core dev to do that properly, during typechecking.
2. If it's going to stay, do what @let-def proposed, ie, "reserve engineer the job of the parser".

[aantron]

It seems like very dubious parsing behavior. As @let-def suggested,

let%lwt () : unit = Lwt.return () in
let%lwt x  : unit = Lwt.return () in

are parsed differently. Even in 4.05.0, the first one is parsed "correctly," but the second one results in a type error, as the constraint is moved to the body.

I'm inclined to address this by documenting that (x : unit) (i.e. in parentheses) is the correct way to write constraints in let%lwt, since that works on all versions and with all patterns.

[Drup]

@aantron Please at least open a mantis ticket to signal the fact that this parsing is problematic for lwt's ppx. :)

[aantron]

Ok, I'll do it with ETA Monday :)

[aantron]

https://caml.inria.fr/mantis/view.php?id=7758