Comment author: @stedolan

To expand on Jeremy's comment about laziness, here's an example using laziness that would segfault if the typing order were changed but the matching order were not.

type 'a is_str = Is_string : string is_str
type 'a box = { x : 'a; tag : 'a is_str Lazy.t }

let foo (type a) : a box -> bool = function
  | { tag = lazy Is_string; x = "foo" } -> true
  | _ -> false

let bang = foo { x = 42; tag = lazy (assert false) }

The field 'x' is only known to be of type 'string' after the match on field 'tag' has succeeded. Since it is a lazy pattern-match, this match could fail with an exception, in which case 'x' might not be a string.

So, if the equations gleaned from 'tag = lazy Is_string' are available when type-checking 'x = "foo"', then 'tag' must be evaluated before 'x' is matched. 4.06.1 types and matches 'x = "foo"' first, so this function gives a type error:

This pattern matches values of type string
but a pattern was expected which matches values of type a

It would also be fine to type and match 'tag = lazy Is_string' first, in which case this code would be type correct and fail with an assertion error, but soundness demands that the typing order and evaluation order do not contradict each other.

Comment author: @trefis

Thanks for the example.

What I meant was: we can get the same segfault without needing lazyness at all, if you have:

type 'a typ = Is_string : string typ | Is_int : int typ
type 'a box = { x : 'a; tag : 'a typ }

let foo (type a) : a box -> bool = function
  | { tag = Is_string; x = "foo" } -> true
  | _ -> false

you'll get into trouble just the same if you look at x first and you're passed { tag = Is_int, x = 42 }.

Comment author: @gasche

A comment on my different-field-orders-in-the-same-column point: (as Thomas already knows) we know how to compile this correctly, by splitting the matrix into several submatrices, one for different row orders. (In general "split more" is the magical solution to compilation correctness issue.) But this solution is a bit frustrating as it may degrade the performance of existing programs.

We could have a conservative criterion on when it is not needed to split, that is when it is valid to reorder field. It's clearly sound if the fields are all variables, and I think we can extend to the case where the fields are all exhaustive value patterns (value patterns as opposed to effectful patterns like "lazy"). In particular, it is non-trivial but I think checking a one-constructor GADT can be delayed to after accessing type-dependent patterns -- this is similar the logic used to shortcut the case switch when all type-valid GADT constructors return a field of interest in the same position.

With this improvement (a conservative criterion on when reordering is sound and splitting is thus not necessary), the impact on performance would probably be negligible, so it would be all dandy. But this is yet more complicated logic to implement and maintain, and nobody is positively excited by the idea.

Comment author: @trefis

I agree with this on principle, though I would probably use a slightly different criterion.

But indeed, I'm not excited by this either: keeping the current ordering seems "fine" for now; we can reconsider after an hypothetical cleanup/simplification of matching.ml

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.