I'm not convinced by this change.

inactive is documented as "matching on them does not incur any computation", which I understand is a way to guard against provoking side-effects affecting matches in the current clause set. (There were bugs with lazy thunk forcing invalidating the assumptions made by the pattern-matching compiler).

The current PR overloads the name with something that becomes false when reading mutable state (arrays or mutable records), apparently getting closer to a notion of "pure" pattern, but it does not update the documentation comment nor explain why the change of semantics is desirable in general.

I don't have a full understanding of the issue, but I have the impression that an optimization was wrong to rely on only this notion of "inactivity" (it needs a stricter check with different semantics), but that you fixed the symptoms by changing the definition instead of changing the optimization.

but I have the impression that an optimization was wrong to rely on only this notion of "inactivity" (it needs a stricter check with different semantics), but that you fixed the symptoms by changing the definition instead of changing the optimization.

The inactive function only exists for this optimisation. It is supposed to mean a notion of "pure" pattern and was just incorrect before. I can change the documentation if you like, although for me reading a mutable variable is clearly not "trivial computations" meaning that the documentation is still correct.

I looked at the story of this code in more details:

• I think the bug was already in the first implementation of curryfication by @xavierleroy in 1995 ( 62bfd98 )
• Some version of this bug for match-failure (instead of delayed side-effects) was spotted and fixed by @mauny in 2008 ( 6373550 ), as part of Michel's work on lazy pattern that led to lazy patterns being singled out in the later "fluid" definition ( 6ba024a )

Some remarks:

• this is unrelated to @maranget's recent work on interaction of side-effects with pattern-matching compilation, contrarily to what I assumed above (by the way, his work appears to be still-unmerged in Fix MPR7241: Pattern matching with mutable and lazy patterns is unsound #717 )
• it would be correct to change the definition of "fluid" as this optimization test is the only user
• there should be a clear semantic explanation for when currification (which delays evaluation) is valid or not, to use as documentation comment for the function used in this code path
• an extremely similar bug has been discussed in the past, PR#7531, "Delayed effects in partially applied functions"; a careful study of the issue would have caught this
• The issue above was found by differential fuzz-testing the OCaml compilers, as reported in an upcoming ICFP 2017 article. I wondered why this fuzzer did not catch the current bug; the answer is that it does differential testing of native vs. bytecode compilation, and both are affected. We need to plug a naive reference evaluator (@johnwhitington's ocamli?) in their tool to catch more bugs.

It is supposed to mean a notion of "pure" pattern and was just incorrect before. I can change the documentation if you like, although for me reading a mutable variable is clearly not "trivial computations" meaning that the documentation is still correct.

This is not at all how I read the current documentation. I quote:

(* An inactive pattern is a pattern whose matching needs only
   trivial computations (tag/equality tests).
   Patterns containing (lazy _) subpatterns are active. *)

let rec inactive pat = match pat with
| Tpat_lazy _ ->
    false
| Tpat_any | Tpat_var _ | Tpat_constant _ | Tpat_variant (_, None, _) ->
    true
| Tpat_tuple ps | Tpat_construct (_, _, ps) | Tpat_array ps ->
    List.for_all (fun p -> inactive p.pat_desc) ps
| Tpat_alias (p,_,_) | Tpat_variant (_, Some p, _) ->
    inactive p.pat_desc
| Tpat_record (ldps,_) ->
    List.exists (fun (_, _, p) -> inactive p.pat_desc) ldps
| Tpat_or (p,q,_) ->
    inactive p.pat_desc && inactive q.pat_desc

(* A `fluid' pattern is both irrefutable and inactive *)

let fluid pat =  irrefutable pat && inactive pat.pat_desc

Indeed the notion of "trivial" computation is not defined, but I don't see how one would assume that reading from an immutable block is "trivial" while reading from a mutable block is "not trivial". The implementation and the documentation both only mention forcing a lazy subpattern as the only source of "non-trivial computation", making it pretty clear to me that the intent is "executing OCaml code" versus "only accessing already-evaluated values".

(By the way, Alain would chime in to point out that re-boxing unboxed floating-point values on the fly may execute arbitrary OCaml code if the GC kicks in, but let's ignore that issue for now, just as it is ignored in the rest of the pattern-matching machinery.)

I don't see how one would assume that reading from an immutable block is "trivial" while reading from a mutable block is "not trivial"

Well, personally I would never use "trivial" to describe a computation that does side-effects. Still I take your point about the documentation. I'll change it to something more explicit.

Alain would chime in to point out that re-boxing unboxed floating-point values on the fly may execute arbitrary OCaml code if the GC kicks in

Maybe I'm missing something, but I don't see how that is relevant here. We're only concerned here with not pushing the pattern's side-effects under a lambda.

My point is that you are silently changing the intent of the inactive function from something that was inadequate (it does not prevent wrong optimizations) but well-defined (imho) to something that may be more correct but that you have not clearly defined. Please clearly specify what we are checking in the pattern (what does impure mean) and why it should now be adequate (why is this particular notion of impurity used here? would it have caught previous similar issues such as MPR#7531?).

Maybe I'm missing something, but I don't see how that is relevant here.

The point was that reading a floating-point number from a pure (unboxed) record may execute code, and thus that curryfication, by delaying this read (and the underlying allocation), changes the observable behavior of the code. Apologies for the distraction.

My point is that you are silently changing the intent of the inactive function from something that was inadequate (it does not prevent wrong optimizations) but well-defined (imho) to something that may be more correct but that you have not clearly defined.

I really don't see how the old definition was any more well defined than the new one, but I've replaced "needs only trivial computations" with "does not perform side-effects".

and thus that curryfication, by delaying this read (and the underlying allocation), changes the observable behavior of the code. Apologies for the distraction.

Curryfication can always change the allocation behavior, and interleaving of effects between threads and from finalizer codes is not specified. So I don't think there is any issue here with the possibility of triggering the GC because of boxing, since the pattern is irrefutable. (The problem is for pattern-matching, where the "asynchronous" effects can break invariants assumed by the pattern matching compiler and lead to unsound code.)

I apologize for the final nitpicking, but the current definition of inactive does not quite match the specification, given that it does not check for partiality (erasing/dropping the check of a partial pattern is invalid if the matching would raise a faliure). This could be fixed by either:

1. checking for totality in this function as before (but I don't understand if it can be done in a type-informed way)
2. adding a ~partial:Typedtree.partial parameter to the function that makes it explicit that the context should provide the totality information, and uses it to return the result
3. just adding to the documentation an indication that totality is assumed / a precondition (I don't like this choice very much)

I think (2) would be the nicest choice.

@lpw25 : could you please address @gasche 's nitpicking and @alainfrisch 's suggestion for an extra test? I think this PR should be part of 4.06, but for this to happen you need to act quickly.

Ok, nitpicking attended too, branch rebased, and change entry added.

Is the following behaviour intended (i.e. is the pattern supposed to be evaluated before all arguments of f are passed) ? See https://caml.inria.fr/mantis/view.php?id=7789:

# let f {contents = c} () = c;;
val f : 'a ref -> unit -> 'a = <fun>
# let r = ref 10;;
val r : int ref = {contents = 10}
# let g = f r;;
val g : unit -> int = <fun>
# g ();;
- : int = 10
# r := 20;;
- : unit = ()
# g ();;
- : int = 10

Yes, the semantics of let f p q = ... are intended to be the same as let f = fun p -> (fun q -> ...).