Original bug ID: 6405
Reporter: @gasche
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:26:54Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.02.0+dev
Category: typing
Child of: #5998

Bug description

GADT type-checking currently accepts to consider as different types that become unifiable in presence of -rectypes. When linking modules that use -rectypes and other that do not, this allows to break typing soundness.

In blah.ml:

type ('a, 'b, 'c) eqtest =
| Refl : ('a, 'a, float) eqtest
| Diff : ('a, 'b, int) eqtest

let test : type a b . (unit -> a, a, b) eqtest -> b = function
| Diff -> 42

In bluh.ml:

let () =
print_float Blah.(test (Refl : (unit -> 'a as 'a, 'a, _) eqtest))

To test:

ocamlc -c blah.ml &&
ocamlc -rectypes -c bluh.ml &&
ocamlc blah.cmo bluh.cmo -o bang &&
./bang

Result:

Segmentation fault

Reproduced under 4.01 and trunk.

Additional information

A good share of the credit for this bug goes to Benoît Vaugon, for
trying to show me that surely the format6 type I expected for "%(%)%d"
was unsound, as -rectypes would allow to perform
a seemingly-impossible unification.