Original bug ID: 5892
Reporter: @lpw25
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:42Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.00.1
Fixed in version: 4.00.2+dev
Category: typing
Related to: #5853
Child of: #5998
Monitored by: @gasche @diml

Bug description

I haven't explored the issue fully, but there is something wrong with the GADT exhaustivness check. The problem is probably in Ctype.mcomp.

The following files will give a segmentation fault when run:

testList.ml:

module type Num = sig
type nil
type _ cons
end

module Make (N: Num) = struct
type nil = N.nil
type 'a cons = 'a N.cons

type ('a,'b) t =
| Cons : 'a * ('a, 'b) t -> ('a, 'b N.cons) t
| Nil : ('a, N.nil) t

end

module Bad = struct
type nil
type _ cons = nil
end

module Types = Make(Bad)

let bad: (int, Types.nil Types.cons) Types.t = Types.Nil

testList.mli:

module Types : sig

type _ cons

type nil

type ('a,_) t =
| Cons : 'a * ('a, 'b) t -> ('a, 'b cons) t
| Nil : ('a, nil) t

end

val bad: (int, Types.nil Types.cons) Types.t

test.ml:

let hd: type a b . (a, b TestList.Types.cons) TestList.Types.t -> a =
fun (TestList.Types.Cons(x,_)) -> x

let _ = hd TestList.bad

Steps to reproduce

$ ocamlc -c testList.mli
$ ocamlc -c testList.ml
$ ocamlc -c test.ml
$ ./a.out
Segmentation fault