Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005892OCamltypingpublic2013-01-16 14:432015-12-11 19:18
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.00.1 
Target VersionFixed in Version4.00.2+dev 
Summary0005892: GADT exhaustiveness check is broken
DescriptionI 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:

  module type Num = sig
    type nil
    type _ cons

  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

  module Bad = struct
    type nil
    type _ cons = nil

  module Types = Make(Bad)

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


  module Types : sig

    type _ cons

    type nil

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

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

  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
$ ocamlc -c
$ ./a.out
Segmentation fault
TagsNo tags attached.
Attached Files

- Relationships
related to 0005853closedgarrigue compiler is unable to detect unused cases in pattern matching on GADT 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
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 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
2015-12-11 19:18 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker