Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006395OCamlOCaml typingpublic2014-05-05 18:552014-07-16 18:21
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target Version4.03.0+devFixed in Version 
Summary0006395: Incorrect exhaustiveness warning with GADTs
DescriptionGiven the following type definitions:

  type p = P
  type q = Q

  type _ t =
    X : bool -> p t
  | Y : q t

the following code correctly compiles without exhaustiveness warnings

  let f : type a. a t * a t -> unit = function
  | X _, X _ -> ()
  | Y, Y -> ()

but the following code

  let g : type a. a t * a t -> unit = function
    | x, X false -> ()
    | X _, X _ -> ()
    | Y, Y -> ()

gives a warning:

   Warning 8: this pattern-matching is not exhaustive.
   Here is an example of a value that is not matched:
   (Y, X true)

TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0011422)
garrigue (manager)
2014-05-11 09:55

Another example which shows that the GADT exhaustiveness check, while sound, is extremely fragile.

- Issue History
Date Modified Username Field Change
2014-05-05 18:55 yallop New Issue
2014-05-08 00:46 yallop Relationship added child of 0005998
2014-05-11 09:55 garrigue Note Added: 0011422
2014-05-11 09:55 garrigue Assigned To => garrigue
2014-05-11 09:55 garrigue Status new => acknowledged
2014-07-16 18:21 doligez Target Version => 4.03.0+dev


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker