stedolan / counterexamples

Counterexamples in Type Systems
http://counterexamples.org
372 stars 23 forks source link

Counterexample proposal: cross-stage persistence #13

Open yallop opened 2 years ago

yallop commented 2 years ago

The following MetaOCaml code, distilled from

Generating code with polymorphic let a ballad of value restriction, copying and sharing Oleg Kiselyov

involves an unsound interaction between three MetaOCaml features:

let lift x = .<x>.

let foo = Runcode.run
  .<let f () = .~(lift (ref None)) in
   f () := Some 2;
   match !(f ()) with Some x ->  x ^ "3" | None -> "" >.

Running it in (the latest versions of) BER MetaOCaml produces a segmentation fault.