typer can wrongly eta-expand effectful expressions

[vicuna]

Original bug ID: 7657
Reporter: @sliquister
Assigned to: @alainfrisch
Status: resolved (set by @xavierleroy on 2017-10-19T13:25:38Z)
Resolution: fixed
Priority: normal
Severity: major
Version: 4.05.0
Target version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Monitored by: @gasche

Bug description

The following program should clearly raise:

let foo g () = g 1; ()
let f ?x y = ()

let _ = foo (assert false; f)

but it doesn't (with 4.05).

I think this is because the typer rewrites the argument of foo as:

let _ = foo (fun y -> (assert false; f) ?x:None y)

because it calls is_nonexpansive to decide if the expression is side-effect free, which doesn't work for sequences and other cases (the condition of if-then-else, patterns with lazy in them, etc).

(I didn't run into this in practice, I simply saw the call to
is_nonexpansive and thought that it couldn't be right)

[vicuna]

Comment author: @alainfrisch

I wonder whether the compiler shouldn't be less clever and always let-bind the argument outside the eta-expanded function (as it does today when is_nonexpansive returns false). The common case where the argument is a simple identifier would be simplified by the Simplif pass anyway.

[vicuna]

Comment author: @alainfrisch

is_nonexpansive also fails to detect reads from mutable locations, so

let foo g () = g 1; ()
let f1 ?x y = print_endline "f1"
let f2 ?x y = print_endline "f2"
let r = ref f1
let h = foo r.contents
let () = h (); r := f2; h ()

prints:

f1
f2

[vicuna]

Comment author: @alainfrisch

#1424

[vicuna]

Comment author: @xavierleroy

Pull request was merged in trunk and 4.06.