Original bug ID: 7241
Reporter: @stedolan
Assigned to: @maranget
Status: assigned (set by @mshinwell on 2017-03-09T12:39:53Z)
Resolution: open
Priority: normal
Severity: crash
Category: typing
Related to: #5992
Monitored by: junsli braibant @gasche @hcarty

Bug description

Optimised pattern matching skips checking conditions that seem redundant. However, since OCaml supports pattern-matching mutable fields, and code execution during matching via "lazy" patterns, the truth of some conditions can vary during matching.

This can cause seemingly-impossible cases to be taken, if forcing lazy values causes mutations that confuse the optimised matching logic. Due to the presence of GADTs, taking an impossible case is a soundness issue.

For example, this program segfaults:

type (_, _) eq = Refl : ('a, 'a) eq
type (_, _) deq = Deq : ('a, 'x) eq option * ('x, 'b) eq option -> ('a, 'b) deq

let deq1 = Deq (Some Refl, None)
let deq2 = Deq (None, Some Refl)

type ('a, 'b) t = { 
  a : bool; 
  mutable b : ('a, 'b) deq;
  mutable c : int Lazy.t
}

let g (type a) (type b) : (a, b) t -> (a, b) eq = function
| { a = true; b = Deq (None, _) }
| { a = true; b = Deq (Some _, _); c = lazy 1 }
| { a = false }
| { b = Deq (_, None) } -> 
   assert false
| { b = Deq (Some Refl, Some Refl) } ->
   Refl

let bad =
  let r = { a = true; b = deq1; c = lazy 1 } in
  r.c <- lazy (r.b <- deq2; 2);
  g r

let castint (type a) (Refl : (int, a) eq) (x : int) : a = x
let _ = print_string (castint bad 42)

This program uses mutation to change a field from "deq1" to "deq2" during matching, making it seem like the impossible "Deq (Some Refl, Some Refl)". (The behaviour is very dependent on the exact sequence of cases in "g", and seemingly-equivalent programs will often give different behaviour).