0005892: GADT exhaustiveness check is broken

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005892

OCaml

OCaml typing

public

2013-01-16 14:43

2013-04-23 02:41

Reporter

lpw25

Assigned To

garrigue

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

OS Version

Product Version

4.00.1

Target Version

Fixed in Version

4.00.2+dev

Summary

0005892: GADT exhaustiveness check is broken

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

Tags

No tags attached.

Attached Files

Relationships

related to	0005853	resolved	garrigue	compiler is unable to detect unused cases in pattern matching on GADT
child of	0005998	assigned	garrigue	GADT typing and exhaustiveness bugs

Notes
(0008762) garrigue (manager) 2013-01-16 18:39	Fixed in 4.00 and trunk, revisions 13250 and 13252. Ctype.in_pervasives was broken: looking for a path TestList.nil in the empty environment also looks it up inside testList.cmi... Now we also require that the path has no prefix (subsumed by Ctype.in_current_module). As a result, Pervasives.in_channel and Pervasives.out_channel are no longer recognized as incompatible types (only those in predef.ml are incompatible).

Issue History
Date Modified	Username	Field	Change
2013-01-16 14:43	lpw25	New Issue
2013-01-16 15:06	gasche	Relationship added	related to 0005853
2013-01-16 18:39	garrigue	Note Added: 0008762
2013-01-16 18:39	garrigue	Status	new => resolved
2013-01-16 18:39	garrigue	Fixed in Version	=> 4.00.2+dev
2013-01-16 18:39	garrigue	Resolution	open => fixed
2013-01-16 18:39	garrigue	Assigned To	=> garrigue
2013-04-23 02:41	garrigue	Relationship added	child of 0005998