Linking modules compiled with -labels and -nolabels is not safe

[vicuna]

Original bug ID: 7432
Reporter: @yallop
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-12-17T01:38:18Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Category: typing
Monitored by: @hcarty

Bug description

The -labels and -nolabels modes of the compiler have different views of type equality. There are some types that are considered equal with -nolabels, but incompatible with -labels.

It's possible, therefore, to pass a witness of type equality (compiled with -nolabels) to a function compiled (with -labels) under the assumption that no such witness can exist, leading to a crash.

Here's a demonstration:

$ cat a.ml 
type (_,_) eql = Refl : ('a, 'a) eql
type s = x:int -> y:float -> unit
type t = y:int -> x:float -> unit
let eql : (s, t) eql = Refl
$ cat b.ml 
open A

type silly = {silly: 'a.'a}

let f : [`L of (s, t) eql | `R of silly] -> 'a =
   function `R {silly} -> silly
let () = print_endline (f (`L A.eql))
$ ocamlopt -c -nolabels a.ml  && ocamlopt -c  b.ml && ocamlopt a.cmx b.cmx -o a.out
$ ./a.out 
Segmentation fault

[vicuna]

Comment author: @garrigue

Fixed by commit 6e694c6.

mcomp was already doing the right thing (ignoring labels for non-optional arguments), but unify has to do the same thing when in Pattern mode.