Segfault from bug in GADT/module typing

[vicuna]

Original bug ID: 6992
Reporter: @stedolan
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:24Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.3
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Related to: #7234
Monitored by: @gasche @diml @yallop

Bug description

The following program is incorrectly accepted by OCaml 4.02.3 and causes a segfault:

type (_, _) eq = Eq : ('a, 'a) eq
let cast : type a b . (a, b) eq -> a -> b = fun Eq x -> x

module Fix (F : sig type 'a f end) = struct
type 'a fix = ('a, 'a F.f) eq
let uniq (type a) (type b) (Eq : a fix) (Eq : b fix) : (a, b) eq = Eq
end

module FixId = Fix (struct type 'a f = 'a end)
let bad : (int, string) eq = FixId.uniq Eq Eq
let _ = Printf.printf "Oh dear: %s" (cast bad 42)

The module type of "Fix" states than an arbitrary type constructor has at most one fixpoint, and "bad" uses this to conclude that string and int, both being fixpoints of the identity type constructor, must therefore be equal.

This seems to be the same sort of thing as #5343 and #6870 (incorrect internal assumptions about contractivity), but this one causes segfaults even without -rectypes.

Incidentally, 4.02.1 with -rectypes correctly rejects this program. 4.02.1 without -rectypes, and 4.02.2/3 with or without -rectypes all accept this program and segfault.

[vicuna]

Comment author: @garrigue

Fixed in trunk at revision 16427.

(At some point the check for recursive types was completely removed for local abbreviations, forgetting the contractiveness problem.)