Compatibility check wrong for abstract type constructors

[vicuna]

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

Bug description

OCaml version 4.03.0+dev19-2016-04-15

type (_, _) eq = Eq : ('a, 'a) eq | Neq : int -> ('a, 'b) eq

module F (T : sig type _ t end) = struct
let f (type a) (Neq n : (a, a T.t) eq) = n
end
module M = F (struct type 'a t = 'a end)
let _ = M.f Eq;;
Segmentation fault

The 'Eq' case should not be judged impossible, and the exhaustiveness check should fail but does not. This is a regression since 4.02.3, which correctly prints an exhaustivity warning and then raises Match_failure.

[vicuna]

Comment author: @garrigue

Fixed in 4.03 and trunk by commits 06a0538 and a8a5da4.

New behavior is only not to add an equation when there is a contractiveness problem, so that both this PR and #6992 can be solved simultaneously (i.e., error message for #6992 changes)