A new check that 'let rec' bindings are well formed

[yallop]

This pull request introduces a new check that let rec bindings are well-formed, replacing the existing check in the compiler.

Background: checking let rec

In addition to types, there are two constraints on the form of a let rec binding:

• The left-hand side may only be a variable or an underscore. The following is not allowed, for example, because the left-hand side is a more complex pattern:

let rec (x, y) = (e1, e2)

• The right-hand-side may be any expression. However, there are restrictions on how the variables bound on the left can be used on the right. For example, the following is not allowed, even though it can be given a type:

let rec f =
let y = f () in (fun () -> ())

However, it is not necessary for the right-hand side of a let rec binding to be a function, or even to be in the form of a value. For example, the following is allowed:

type t = { next: unit -> t }
let rec f =
   let r = ref 0 in
      { next = fun () -> incr r; print_int !r; f }

This reflects a more liberal policy (described in more detail below) than some other ML-family languages, such as SML98:

For each value binding pat = exp within rec, exp must be of the form fn match. The derived form of function-value binding given in Appendix A, page 71, necessarily obeys this restriction.
(from the Revised Definition, p10)

Code which makes use of OCaml's relaxed restrictions is fairly common (e.g. [1], [2])

Where should the check be performed?

An OCaml program takes on several forms as it passes through the compiler. Source code is scanned, parsed, type-checked, and translated into a series of intermediate forms, before finally emerging as byte code or machine code. At present the check for whether a let rec binding is well-formed is performed on one of these intermediate languages, called Lambda.

Advantages of Lambda

Lambda is a good place to perform the check, for several reasons.

First, it's a comparatively small, simple language. Source expressions that have quite different syntax and types may take the same form when converted to Lambda. For example, the following expression, that builds a record

{ x = 3; y = 4 }

is translated to the same Lambda code as the following expression, which constructs a value of variant type:

T (3, 4)

Since the Lambda language is smaller than the languages used earlier , the check is also smaller and simpler.

Second, the Lambda language is comparatively stable. It is often possible to leave Lambda unchanged when adding features to the OCaml language. As long as Lambda remains unchanged, the check that let rec bindings --- or rather, their translation into Lambda code --- can also be left unchanged.

Third, the form of Lambda code reflects the run-time behaviour of OCaml programs quite closely. Whether a let rec binding is considered well-formed is in a sense determined by the behaviour of the program, not by its type or surface syntax. It's easier to determine how a program will behave at the point when it's in Lambda form than at earlier stages of the compiler.

Advantages of Typedtree

However, there are also a number of advantages to placing the check for let rec wellformedness at an earlier stage in the compiler.

First, developing an OCaml program often involves running only a part of the compiler. For example, Merlin uses the OCaml type checker to check the types of a program as you type it into your editor. However, Merlin does not perform the additional work of translation into Lambda code at this stage, and so the check that let rec bindings are well-formed does not take place. It sometimes happens that Merlin reports no errors in a program such as this one:

let rec x = x

which is then rejected when it is eventually passed to the OCaml compiler. If the let rec check took place during type checking then Merlin could offer more comprehensive feedback to the user at an early stage, and every program accepted by Merlin would be guaranteed to compile successfully.

Similarly, the multi-stage language MetaOCaml uses OCaml's parser and type checker to ensure that code that appears within quotations is correct. However, checking quoted code does not involve translation into Lambda, and so the let rec check is not performed. Instead, MetaOCaml performs a much simpler and more restrictive check which rejects some valid OCaml programs:

# .< fun () -> let rec x = () in () >.;;
Characters 21-27:
  .< fun () -> let rec x = () in () >.;;
                       ^^^^^^
Recursive let binding must be to a function

Third, performing the check on Lambda makes its behaviour more difficult to explain to users. Lambda is an internal language of the compiler, not part of the OCaml definition. However, the let rec check is defined by a combination of the translation into Lambda and a test of the resulting Lambda code. It is difficult to explain precisely which programs will be accepted or rejected without also describing the translation.

Finally, some recent additions to the langauge make it more difficult to check let rec bindings using Lambda code. A few days ago @stedolan posted a program on Mantis that uses a combination of GADTs and a let rec binding to cause OCaml to crash. Unfortunately, there is not enough information available in the Lambda form of his program to distinguish it from harmless programs that should be accepted. Moving the check to an earlier phase of the compiler would make it possible to distinguish the harmful program from the harmless program before the information is thrown away.

How does the new check work?

This pull request adds a new implementation of the let rec check to the type checking phase of the OCaml compiler. At this stage, programs are represented in the Typedtree language. Programs in the the Typedtree form still resemble source programs quite closely, but they have been checked for type correctness, and annotated with some additional useful information, such as a way of distinguishing identifiers with the same name.

The new check distinguishes various ways of accessing a variable.

• An inspection of a variable is the most dangerous sort of access. Inspection involves accessing the actual value (or "shape") of a variable, which requires that the value be already fully defined. There are various kinds of inspection: one might call a function f, match against a variant v, or access a field of a record r.
• An unguarded use of a variable uses the variable without inspecting its value. The expression x is an unguarded use of the variable x.
• A guarded use of a variable is like an unguarded use, but additionally wraps the variable in a constructor. The expressions [x], { l = x } and fun () -> x are all guarded uses of the variable x
• A discarded use of a variable is like an unguarded use, but discards the value of the variable entirely, like this: (x; ())

The way that a variable is used in an expression is determined both by the form of the expression and the way that the variable is used in subexpressions. Here are some examples:

• A constructor such as Some changes uses of a variable in its argument from unguarded to guarded, but does not affect inspections. For example, in Some f, f is guarded, but in Some (f x), f is used.
• A function expression guards all uses of variables in its body. For example, in fun () -> f x, both f and x appear guarded.

The full let rec check involves tracing the uses of variables through bindings. For example in the following expression, y is considered guarded, because it appears guarded in the binding for x, and because the bound variable x is not inspected:

let x = [y] in x

However, in the following expression, y is considered to be inspected, because its value may be inspected by the function f:

let x = [y] in f x 

Tracing uses in this way necessarily involves some approximation, and in some cases the implementation in this PR approximates quite coarsely. For example, any appearance of a variable within a class or recursive module definition is treated as an inspection.

These different types of variable access are key to the definition of let rec wellformedness, which is as follows: every access to a variable bound by let rec in its own definition must be guarded.

Examples and changes

Bug fixes

Moving the check from Lambda to Typedtree fixes several open bugs, including

• Mantis PR7215: Unsoundness with GADTs and let rec
  Here is the offending code, which caused a segmentation fault:

  let rec (p : (int, a) eq) = match p with Refl -> Refl in

  This is now rejected, because p is inspected in its own definition.

• Mantis PR7231: let-rec wellformedness check too permissive with nested recursive bindings
  Here is the offending code, which caused a segmentation fault:

  let rec r = let rec x () = r and y () = x () in y () in r "oops"

  This is now rejected because the call to y involves inspecting x, and inspecting x involves inspecting r, which is not allowed.

• Mantis PR6738: Check for the well-formedness of let rec earlier, before or at type checking

There should no regression to the let rec problems that have been previously reported and fixed, such as

• Mantis PR1497: Segmentation fault error by infinite loop
• Mantis PR6939: Segfault with improper use of let-rec

Incompatibilities

Moving the let rec check from Lambda to Typedtree also introduces a number of small incompatibilities:

• Array constructors are now considered inspections.

  Should the following program be accepted or rejected?

  let rec x = [| y; z |] and y = z in x

  In the current implementation the answer depends on the type of z. If z has some concrete type, such as int or float, then the program is accepted. In other cases, such as where z is bound as the parameter of a polymorphic function, the program is rejected.

  The new check is simpler, but a little less generous, and rejects the program regardless of the type of z.

• A call to ref is now considered an inspection.

  The following program is accepted by the current implemenation, even though y is passed to the function ref:

  let rec x = ref y and y () = ()

  The new check rejects the program, since ref is not distinguished from other functions at the type-checking stage. However, the program can be easily rewritten to an acceptable form:

  let rec x = { contents = y } and y () = ()

• Record overriding is always considered an inspection, even when there are no fields retained:

  The following rather odd program is currently accepted, but rejected by the new check:

  let rec x = { x with contents = 3 }

Other improvements

A few programs that were previously rejected are now accepted. For example, this program was previously accepted

let rec x = (x; ())

while this one was rejected

let rec x = let y = (x; ()) in y

With the new check both are accepted.

I'm grateful to @mshinwell, @lpw25, @garrigue and @stedolan for help, suggestions and testing.

I would very much appreciate a review of both the new approach and the new code.

[yallop]

@stedolan has given an additional example which is accepted by both the existing check and the check in this pull request:

# let rec r = (let rec x = `A r and y = fun () -> x in y);;
val r : unit -> [> `A of 'a ] as 'a = <fun>
# let (`A x) = r () in x ();;
Segmentation fault

At the moment it's not clear to me whether the problem is that the check is too permissive or that the translation of nested recursive bindings is incorrect.

[lpw25]

every access to a variable bound by let rec in its own definition must be guarded

I believe that this constraint is sufficient to restrict programs to those which could be compiled. However, I'm not sure it is strong enough to restrict programs to those which OCaml's current backends can compile (even after fixing the issue with nested recursive bindings).

The problem is that OCaml currently handles recursive bindings by allocating a dummy block before executing the bindings and then filling in the fields of the block from the defined value. In order to do this is must know the size of the result in advance. For example, the following code is accepted by the check in this patch but refused by the old check, and results in a segfault at runtime:

let foo p x =
  let rec f =
    if p then (fun y -> x + g y) else (fun y -> g y)
  and g =
    if not p then (fun y -> x - f y) else (fun y -> f y)
  in
  (f, g)

let f, g = foo true 9

let _ = f 10
let _ = g 11

As I said, I believe that any code which passes the constraint in this patch can be compiled. For example, the above definition could be translated to something equivalent to:

  let f, g =
    match p, not p with
    | true, true ->
        let rec f = (fun y -> x + g y)
        and g = (fun y -> x - f y) in
          f, g
    | true, false ->
        let rec f = (fun y -> x + g y)
        and g = (fun y -> f y) in
          f, g
    | false, true ->
        let rec f = (fun y -> g y)
        and g = (fun y -> x - f y) in
          f, g
    | false, false ->
        let rec f = (fun y -> g y)
        and g = (fun y -> f y) in
          f, g

but until the OCaml backend is smart enough to do this I think the check will need to be stronger.

[yallop]

Thanks, @lpw25 .

One approach that would both fix the open PRs and avoid introducing new unsoundness would be to keep both checks (i.e. on Lambda and Typedtree) for the moment.

[lpw25]

One approach that would both fix the open PRs and avoid introducing new unsoundness would be to keep both checks (i.e. on Lambda and Typedtree) for the moment.

Yes, I think that is a good idea. Fixes the immediate issues with substantially lower risk.

[yallop]

Here's another size-related problem with the new check:

# let rec y = (if true then [| |] else y); [| |] in y;;
Characters 26-31:
  let rec y = (if true then [| |] else y); [| |] in y;;
                            ^^^^^
Warning 10: this expression should have type unit.
Fatal error: exception File "bytecomp/bytegen.ml", line 163, characters 47-53: Assertion failed

[gasche]

We should not have to write this. What about some recordification work in typeclass.ml?

[yallop]

That's a good idea, and I think it'd make a suitable project for a compiler hacking evening. I've added it to the wiki.

[gasche]

Excellent, exemplare PR description!

(Your example of issue not caught by Merlin is let x = x, it should be let rec x = x.)

Have you thought of expressing the analysis as a usage-aware typing system? Not only could that be an excellent proposal for the ML workshop, and provide a readable, declarative presentation of the analysis, I think that it could also clarify some subtle point, such as the way you propagate information from the left-hand expression of a let-binding (does this system has an admissible substitution rule?).

I'm worried about the ref change. I think this is the single part of the work that has the highest regression potential, and I would recommend special-casing it.

In the future, we can ask about giving some usage-type information in value definitions in interfaces, and this would let us make the check more modular -- un-special-case ref.

[gasche]

It is not clear to me why this case is rejected (or the one below), given that method calls delay evaluation (object method m = fun () -> x end is delayed as well). Isn't this just a matter of how object declarations are elaborated in practice, that could change with a refined implementation? If so, then maybe it would make sense to add a comment to say it explicitly.

[gasche]

I noticed with interest that you have a good testsuite; it may be helpful to add some comments on the less-obvious cases of the testsuite.

Also, I think that your work would bring us much closer to the situation of having sensibly better error messages in this case. Instead of " this kind of expression is not allowed on the right-hand-side of a let rec", I would like to read something like " this recursive definition is ill-formed as the variable x is forced but not yet fully defined". How much more work would that be?

Finally, I'm lukewarm about the word "inspection". Wouldn't "evaluation" or "forcing" be clearer? (For example I find it clearer to say that x + 1 forces x than to say that it inspects x.)

[gasche]

Also, you forgot a Changes entry.

[stedolan]

This paper by Hirschowitz, Leroy and Wells is definitely relevant, and deals with the issue of correctly sizing blocks. It also contains a correctness proof, although I haven't read it enough to know how this differs from the current implementation.

[stedolan]

Is there a good reason why the rules for let rec should be different from those for module rec?

[lpw25]

Is there a good reason why the rules for let rec should be different from those for module rec?

module rec is more relaxed because it can fail at runtime. Personally, I would rather it didn't do this and just used the same rules as let rec, since you can get the relaxed behaviour by using lazy, but it is a large backwards incompatible change.

[damiendoligez]

@gasche

I'm worried about the ref change. I think this is the single part of the work that has the highest regression potential, and I would recommend special-casing it.

Indeed. I'm testing the patch against OPAM, and so far (about 15% into the list of packages) it's failing three packages:

• biniou (in a test file)

let rec deep_cycle = `Tuple [| `Shared deep_cycle |]

• lwt

    let rec waiter = ref (Some handle_result)
    and handle_result state =
      ...

• ocamlgraph

  let rec dummy_arc =
    { vert = Infinity; next = dummy_arc;
      inst = ref (Terminal dummy_arc); mate = -1 }

[gasche]

Given how late we are in the 4.03 release cycle, I think we should consider either delaying for 4.04 (remember, we are shooting for a shorter release cycle next time, so it's not as big of a deal), or making the stricter check optional, à la -strict-value-rec (please also add -no-strict-value-rec even if it's the default).

It seems rather clear to me, given the state of PR#7231, that more work will be needed both to refine your proposed check and the compiler backend. Given that refinement to your check will decrease its potential for compatibility-breaking changes, I think it would be a mistake to rush the current check by default on 4.03 users.

[damiendoligez]

I'm strongly leaning toward postponing. @garrigue what do you think?

[garrigue]

The question is how much we value soundness.
It disturbs me to leave such a hole open while we know about it.
Having a sufficiently restrictive check on the Typedtree, while keeping the backend unchanged (i.e. leave the original check there), would put us on the safe side.
This means breaking some packages, but the fix is trivial.
However, if your tests show more breakage than expected, I would reconsider.

If we keep the check in the backend, another option would be to make the typedtree check a warning.
Seems strange to me, but this could solve the compatibility problem for a while.

[gasche]

However, if your tests show more breakage than expected, I would reconsider.

Note that the amount of breakage expected should be zero: it seems extremely unlikely to me that code in the wild would actually use an unsound recursive value definition. The examples that breaks type soundness using a recursively-defined GADT (PR#7215) could exist in theory, but it seems rather implausible. The examples that segfault by allowing unsound definitions (PR#7231) are unlikely to be present in released code, but they could be exploited by malicious users as security flaws.

We already have evidence that the ref part breaks code in the wild. Even if @yallop special-cases this one, I wouldn't be confident enough to include the test by default in a release branch that should have already been released by now, and will not be extensively re-tested before the actual release.

I think that making the added check optional could strike a nice balance: safety-conscious user could use the flag (I think that 4.03 comes with a feature to easily add a flag to all compilations; is this in Changes?), but we would have more time to study the check before imposing it on all codebases.

[stedolan]

@damiendoligez

This example from lwt:

let rec waiter = ref (Some handle_result)
and handle_result state =
  ...

relies on ref having being inlined (it is not sound for nonstandard definitions of ref).

This is dubious: whether code is accepted by the compiler depends on the vagaries of the inliner (which are increasingly vague, thanks to Flambda).

This also breaks the invariant that compiling with opaque does not break things: this code is accepted only if the compiler can see the definition of ref.

If this example is to be allowed, perhaps ref should be made a keyword?

[lpw25]

relies on ref having being inlined

To be fair this relies on ref being an external which is actually part of the module type of Pervasives so it not really relying on the inliner.

That being said I think it would be better not to special case ref (or more accurately the %makemutable external) and instead just expect people to write { contents = ... } when using recursion like this.

[damiendoligez]

relies on ref having being inlined (it is not sound for nonstandard definitions of ref).

I agree, and indeed it should be refused, according to the existing documentation. But we have to strike a balance between theory and practice: I'm really wary of introducing an incompatibility a few hours before the release, when we know some important packages will be broken, and we don't know of any problem caused by the bug in the wild.

BTW, another broken package (due to ref) is markup.

[lpw25]

I'm favour of releasing without the fix and then releasing the fix in 4.03.1 (which will probably be needed no matter how many bugs we fix before the release). That should give us a bit more scope to do things like change the ref behaviour.

[mshinwell]

That sounds like the prudent approach to me, too.

[yallop]

I've added some new commits which address some of the comments above:

• 9caaa56 adds a special case to treat Pervasives.ref as a constructor to improve backwards compatibility.
• 0e7dbfb restores the check in Lambda. I've kept this commit separate to keep the history of this change clear, but it should probably be squashed onto 0313fcd to keep the repository history more intact.
• 4650024 updates the test suite to reflect the fact that only code that passes both checks is accepted
• c116b03 adds an entry to Changes

[stedolan]

@lpw25

To be fair this relies on ref being an external which is actually part of the module type of Pervasives so it not really relying on the inliner.

I didn't realise ref was implemented as an external! I don't really have an objection in that case. I think the typechecker should only use knowledge that can be gleaned from module signatures, but if the external "%makemutable" appears there then it's fair game.

@yallop

9caaa56 adds a special case to treat Pervasives.ref as a constructor to improve backwards compatibility.

Looking at the patch, I see that it treats %makemutable as a constructor, rather than the specific identifier Pervasives.ref. This seems quite principled, I think: %makemutable is indeed a constructor.

[damiendoligez]

Let's go with Leo's plan: release without this patch, then we'll have at least a few weeks to refine it and check compatibility.

[damiendoligez]

@gasche I'm in favor of merging the rebased PR.

[gasche]

I also like it, so I went ahead and merged. Thanks @yallop.

[gasche]

Over at MPR#7653 I started investigating what appeared to be, at first, an infinite loop of the compiler on a file of the Frama-C codebase, which I bisected and was provoked by the present PR.

After trying to look at traces in various way, I am starting to realize that this may be not an infinite loop, but a sign of a performance issue related to the design of the current check: on certain large expressions, it may be that the environment grows to extremely large sizes.

On the faulty file in the PR, I added logging to measure the size of the env structure at each recursive expression call. It keeps growing until the compiler stack-overflows. When it overflows, it contains 81 bindings (this is the number of local bindings in scope for code written by humans, so it makes sense), but the largest of these 81 use-sets contains 1 046 688 bindings, and the sum in total contains 3 164 206 bindings. There seems to be a large blowup occurring. (There may be sharing within the use-set representation and across the environment, so the memory usage may not grow as fast.)

I have the impression that, if the environment structure is already large, then a sequence of let-bindings may result in each new variable being added with a fairly large use-set, resulting in a sort of exponential growth of the use-set size. I don't have a firm understanding of how precisely that would be happening yet.

[gasche]

Ready the discussion again, this performance issue was already noticed by @yallop in #556 (comment) and he pushed a commit ( cbc66ff ) to fix it, but it seems that this commit was missed from later merges.

I'm going to stop looking at this for the week-end, and hopefully get things as they should be next week, possibly with @yallop's help.

[gasche]

I got in touch with Jeremy, and I will be taking care of merging cbc66ff back into trunk and 4.06, and checking that the performance regression went away.

[gasche]

I pushed Jeremy's patch ( cbc66ff ) into trunk ( 776387b ) and 4.06 ( ca1441b ), and the frama-C performance problem indeed went away.

[gasche]

For fun, I ran the same size-instrumentation code on the patched version.

Before: largest use set has 1 046 688 bindings, total sum 3 164 206 bindings

After: largest use set has 2 bindings, total sum 82 bindings

[ivg]

Just in case if you're interested, I've referenced a few examples of real-world code that was rejected by the new let-rec checker. I've read through the comments in this PR and didn't find anything that will state that such code should be rejected. And although, I'm pretty fine with the new behavior of the let-rec checker, I decided to submit an issue to Mantis, as I'm not sure whether this regression was anticipated or not.

[damiendoligez]

See #1712