Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005892OCamlOCaml typingpublic2013-01-16 14:432013-04-23 02:41
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
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:

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
TagsNo tags attached.
Attached Files

- Relationships
related to 0005853resolvedgarrigue compiler is unable to detect unused cases in pattern matching on GADT 
child of 0005998assignedgarrigue 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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker