Original bug ID: 7390
Reporter: @stedolan
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-10-19T14:08:45Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.03.0
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: @yallop

Bug description

Here's a slightly odd implementation of a sum type:

type empty = Empty and filled = Filled
type ('a,'fout,'fin) opt =
  | N : ('a, 'f, 'f) opt
  | Y : 'a -> ('a, filled, empty) opt

type 'fill either =
  | Either : (string, 'fill, 'f) opt * (int, 'f, empty) opt -> 'fill either

The intent is that a 'filled either' has values 'Either (Y a, N)' and 'Either (N, Y b)'. However, OCaml accepts the following as exhaustive (both 4.03.0 and 4.02.1):

let f (* : filled either -> string *) =
  fun (Either (Y a, N)) -> a

'f' is inferred to have the commented-out type, but curiously OCaml gives an exhaustivity warning if the annotation is uncommented. If accepted as exhaustive, such a type for 'f' is unsound:

# print_string (f (Either (N, Y 4)));;
Segmentation fault