{"action":"created","issue":{"url":"https://api.github.com/repos/ocaml/ocaml/issues/556","repository_url":"https://api.github.com/repos/ocaml/ocaml","labels_url":"https://api.github.com/repos/ocaml/ocaml/issues/556/labels{/name}","comments_url":"https://api.github.com/repos/ocaml/ocaml/issues/556/comments","events_url":"https://api.github.com/repos/ocaml/ocaml/issues/556/events","html_url":"https://github.com/ocaml/ocaml/pull/556","id":149697827,"number":556,"title":"A new check that 'let rec' bindings are well formed","user":{"login":"yallop","id":1736496,"avatar_url":"https://avatars.githubusercontent.com/u/1736496?v=3","gravatar_id":"","url":"https://api.github.com/users/yallop","html_url":"https://github.com/yallop","followers_url":"https://api.github.com/users/yallop/followers","following_url":"https://api.github.com/users/yallop/following{/other_user}","gists_url":"https://api.github.com/users/yallop/gists{/gist_id}","starred_url":"https://api.github.com/users/yallop/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yallop/subscriptions","organizations_url":"https://api.github.com/users/yallop/orgs","repos_url":"https://api.github.com/users/yallop/repos","events_url":"https://api.github.com/users/yallop/events{/privacy}","received_events_url":"https://api.github.com/users/yallop/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":55,"created_at":"2016-04-20T08:29:37Z","updated_at":"2017-01-02T20:03:53Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/ocaml/ocaml/pulls/556","html_url":"https://github.com/ocaml/ocaml/pull/556","diff_url":"https://github.com/ocaml/ocaml/pull/556.diff","patch_url":"https://github.com/ocaml/ocaml/pull/556.patch"},"body":"This pull request introduces a new check that `let rec` bindings are well-formed, replacing the existing check in the compiler.\n## Background: checking `let rec`\n\nIn addition to types, there are two constraints on the form of a `let rec` binding:\n- 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:\n\n``` ocaml\nlet rec (x, y) = (e1, e2)\n```\n- 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:\n\n``` ocaml\nlet rec f =\nlet y = f () in (fun () -> ())\n```\n\nHowever, 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:\n\n``` ocaml\ntype t = { next: unit -> t }\nlet rec f =\n   let r = ref 0 in\n      { next = fun () -> incr r; print_int !r; f }\n```\n\nThis reflects a more liberal policy (described in more detail below) than some other ML-family languages, such as SML98:\n\n> 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.\n> (from the _Revised Definition_, p10)\n\nCode which makes use of OCaml's relaxed restrictions is fairly common (e.g. [[1]](https://github.com/c-cube/gen/blob/0719c2451a12d586d6b06c378d9021e21d31c82f/bench/bench_persistent.ml#L26-L27), [[2]](https://github.com/janestreet/async_extended/blob/eba34d2caab2a29879f5b3853ee7159cac372362/src/generator.ml#L23-L27))\n## Where should the check be performed?\n\nAn 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](https://github.com/ocaml/ocaml/blob/trunk/bytecomp/lambda.mli). \n### Advantages of Lambda\n\nLambda is a good place to perform the check, for several reasons.\n\nFirst, 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\n\n``` ocaml\n{ x = 3; y = 4 }\n```\n\nis translated to the same Lambda code as the following expression, which constructs a value of variant type:\n\n``` ocaml\nT (3, 4)\n```\n\nSince the Lambda language is smaller than the languages used earlier , the check is also smaller and simpler.\n\nSecond, 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.\n\nThird, 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.\n### Advantages of Typedtree\n\nHowever, there are also a number of advantages to placing the check for `let rec` wellformedness at an earlier stage in the compiler.\n\nFirst, developing an OCaml program often involves running only a part of the compiler.  For example, [Merlin](https://github.com/the-lambda-church/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:\n\n``` ocaml\nlet rec x = x\n```\n\nwhich 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.\n\nSimilarly, the multi-stage language [MetaOCaml](http://okmij.org/ftp/ML/MetaOCaml.html) 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:\n\n``` ocaml\n# .< fun () -> let rec x = () in () >.;;\nCharacters 21-27:\n  .< fun () -> let rec x = () in () >.;;\n                       ^^^^^^\nRecursive let binding must be to a function\n```\n\nThird, 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.\n\nFinally, 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](http://caml.inria.fr/mantis/view.php?id=7215) 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.\n## How does the new check work?\n\nThis 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](https://github.com/ocaml/ocaml/blob/trunk/typing/typedtree.mli) 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.\n\nThe new check distinguishes various ways of accessing a variable.\n- 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`.\n- An **unguarded** use of a variable uses the variable without inspecting its value.  The expression `x` is an unguarded use of the variable `x`.\n- 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`\n- A **discarded** use of a variable is like an unguarded use, but discards the value of the variable entirely, like this: `(x; ())`\n\nThe 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:\n- 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.\n- A function expression guards all uses of variables in its body.  For example, in `fun () -> f x`, both `f` and `x` appear guarded.\n\nThe 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:\n\n``` ocaml\nlet x = [y] in x\n```\n\nHowever, in the following expression, `y` is considered to be inspected, because its value may be inspected by the function `f`:\n\n``` ocaml\nlet x = [y] in f x \n```\n\nTracing 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.\n\nThese 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_.\n## Examples and changes\n### Bug fixes\n\nMoving the check from Lambda to Typedtree fixes several open bugs, including\n- [Mantis PR7215](http://caml.inria.fr/mantis/view.php?id=7215): Unsoundness with GADTs and let rec\n  Here is the offending code, which caused a segmentation fault:\n  \n  ``` ocaml\n  let rec (p : (int, a) eq) = match p with Refl -> Refl in\n  ```\n  \n  This is now rejected, because `p` is inspected in its own definition.\n- [Mantis PR7231](http://caml.inria.fr/mantis/view.php?id=7231): let-rec wellformedness check too permissive with nested recursive bindings\n  Here is the offending code, which caused a segmentation fault:\n  \n  ``` ocaml\n  let rec r = let rec x () = r and y () = x () in y () in r \"oops\"\n  ```\n  \n  This is now rejected because the call to `y` involves inspecting `x`, and inspecting `x` involves inspecting `r`, which is not allowed.\n- [Mantis PR6738](http://caml.inria.fr/mantis/view.php?id=6738): Check for the well-formedness of let rec earlier, before or at type checking\n\nThere should no regression to the `let rec` problems that have been previously reported and fixed, such as \n- [Mantis PR1497](http://caml.inria.fr/mantis/view.php?id=1497): Segmentation fault error by infinite loop\n- [Mantis PR6939](http://caml.inria.fr/mantis/view.php?id=6939): Segfault with improper use of let-rec\n### Incompatibilities\n\nMoving the `let rec` check from Lambda to Typedtree also introduces a number of small incompatibilities:\n- Array constructors are now considered inspections.\n  \n  Should the following program be accepted or rejected?\n  \n  ``` ocaml\n  let rec x = [| y; z |] and y = z in x\n  ```\n  \n  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.\n  \n  The new check is simpler, but a little less generous, and rejects the program regardless of the type of `z`. \n- A call to `ref` is now considered an inspection.\n  \n  The following program is accepted by the current implemenation, even though `y` is passed to the function `ref`:\n  \n  ``` ocaml\n  let rec x = ref y and y () = ()\n  ```\n  \n  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:\n  \n  ``` ocaml\n  let rec x = { contents = y } and y () = ()\n  ```\n- Record overriding is always considered an inspection, even when there are no fields retained:\n  \n  The following rather odd program is currently accepted, but rejected by the new check:\n  \n  ``` ocaml\n  let rec x = { x with contents = 3 }\n  ```\n### Other improvements\n\nA few programs that were previously rejected are now accepted.  For example, this program was previously accepted\n\n``` ocaml\nlet rec x = (x; ())\n```\n\nwhile this one was rejected\n\n``` ocaml\nlet rec x = let y = (x; ()) in y\n```\n\nWith the new check both are accepted.\n\nI'm grateful to @mshinwell, @lpw25, @garrigue and @stedolan for help, suggestions and testing.\n\nI would very much appreciate a review of both the new approach and the new code.\n"},"comment":{"url":"https://api.github.com/repos/ocaml/ocaml/issues/comments/270014786","html_url":"https://github.com/ocaml/ocaml/pull/556#issuecomment-270014786","issue_url":"https://api.github.com/repos/ocaml/ocaml/issues/556","id":270014786,"user":{"login":"yallop","id":1736496,"avatar_url":"https://avatars.githubusercontent.com/u/1736496?v=3","gravatar_id":"","url":"https://api.github.com/users/yallop","html_url":"https://github.com/yallop","followers_url":"https://api.github.com/users/yallop/followers","following_url":"https://api.github.com/users/yallop/following{/other_user}","gists_url":"https://api.github.com/users/yallop/gists{/gist_id}","starred_url":"https://api.github.com/users/yallop/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yallop/subscriptions","organizations_url":"https://api.github.com/users/yallop/orgs","repos_url":"https://api.github.com/users/yallop/repos","events_url":"https://api.github.com/users/yallop/events{/privacy}","received_events_url":"https://api.github.com/users/yallop/received_events","type":"User","site_admin":false},"created_at":"2017-01-02T20:03:53Z","updated_at":"2017-01-02T20:03:53Z","body":"Yes, I'll look at fixing bytecode compilation."}}
{"actor":{"display_login":"yallop"}}