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

let-rec wellformedness check too permissive with nested recursive bindings #7231

Closed
vicuna opened this issue Apr 18, 2016 · 7 comments
Closed
Milestone

Comments

@vicuna
Copy link

vicuna commented Apr 18, 2016

Original bug ID: 7231
Reporter: @yallop
Assigned to: @yallop
Status: resolved (set by @yallop on 2017-09-25T14:11:51Z)
Resolution: fixed
Priority: normal
Severity: crash
Target version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Related to: #6738 #7215 #7447
Monitored by: runhang @stedolan @gasche

Bug description

$ ocaml
OCaml version 4.03.0+beta2

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

Characters 58-64:
let rec r = let rec x () = r and y () = x () in y () in r "oops";;
^^^^^^
Warning 20: this argument will not be used by the function.
Segmentation fault

This should be fixed by the fix for PR6738 (and PR7215), which is now almost complete.

@vicuna
Copy link
Author

vicuna commented Apr 19, 2016

Comment author: @stedolan

This seems like a thorny issue. How does the patch handle the following?

# 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

Note that in this example, the right-hand sides of each equation are more sensible, since no value is eliminated during its definition (the suspicious 'y ()' from the original test case has been removed).

(The polymorphic variant `A is used to allow recursive types, you can also try this example using plain variants and -rectypes.)

@vicuna
Copy link
Author

vicuna commented Apr 20, 2016

Comment author: @yallop

Indeed, that example looks innocuous. Why does it crash? I'd like

let rec r = (let rec x = `A r and y = fun () -> x in y)

to be equivalent to

let rec r = (let rec y = fun () -> `A r in y)

to be equivalent to

let rec r = (fun () -> `A r)

but it's obviously not the case.

@vicuna
Copy link
Author

vicuna commented Apr 20, 2016

Comment author: @garrigue

My understanding is that r may only occur inside a definition in the same mutually recursive block, as they are represented as a single block containing multiple closures and values.

I.e.
let rec r = A y and y = fun () -> r is ok because y can access r through its closure, but let rec r = let rec y = fun () -> A r in y
is not because one ends up copying the contents of r into the closure of y, before r is defined.

@vicuna
Copy link
Author

vicuna commented Apr 20, 2016

Comment author: @lpw25

Duplicating my response on caml-devel about Stephen's second example:

I don't think that the problem with this example is with the check but
with the compilation of recursive bindings. Both expr_size in
cmmgen.ml and size_of_lambda in bytegen.ml declare r to be
non-recursive but if they tracked the definitions of nested recursive
lets (as expr_size already does for nested non-recursive lets) then
they could easily see that it is potentially recursive.

Indeed, the patch below is enough to compile the example successfully
in ocamlopt. A similar change would be needed for size_of_lambda.

diff --git a/asmcomp/cmmgen.ml b/asmcomp/cmmgen.ml
index 8bafc5c..5cfbd7f 100644
--- a/asmcomp/cmmgen.ml
+++ b/asmcomp/cmmgen.ml
@@ -698,6 +698,11 @@ let rec expr_size env = function
| Ulet(id, exp, body) ->
expr_size (Ident.add id (expr_size env exp) env) body
| Uletrec(bindings, body) ->

  •  let env =
    
  •    List.fold_right
    
  •      (fun (id, exp) env -> Ident.add id (expr_size env exp) env)
    
  •      bindings env
    
  •  in
     expr_size env body
    
    | Uprim(Pmakeblock(tag, mut), args, _) ->
    RHS_block (List.length args)

@vicuna
Copy link
Author

vicuna commented Apr 20, 2016

Comment author: @stedolan

Note that OCaml does in fact reject:

let rec r = (let rec y = fun () -> `A r in y)

The crashing case is:

let rec r = (let rec x = `A r and y = fun () -> x in y)

Inlining the let recs, we get:

let rec r = y and x = `A r and y = fun () -> x

which is rejected (the r = y is disallowed).

It is in principle possible to compile "aliases" as part of a let rec, as long as all uses of the aliases are correctly guarded. However, the current back end does not compile these correctly, and the current type checker does not detect all aliases.

Fixing either would suffice to fix my example. I would mildly prefer fixing the back end and allowing aliases in the type checker if guarded (I find let rec f = Foo g and g = f` inoffensive), but I don't know which would require less effort.

@vicuna
Copy link
Author

vicuna commented Dec 7, 2016

Comment author: @mshinwell

#556

@vicuna
Copy link
Author

vicuna commented Sep 25, 2017

Comment author: @yallop

This is fixed in 4.06, now that GPR 556 is merged:

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

Characters 58-64:
let rec r = let rec x () = r and y () = x () in y () in r "oops";;
^^^^^^
Warning 20: this argument will not be used by the function.
Characters 12-52:
let rec r = let rec x () = r and y () = x () in y () in r "oops";;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This kind of expression is not allowed as right-hand side of `let rec'

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant