Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006395OCamlOCaml typingpublic2014-05-05 18:552016-04-05 15:12
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target Version4.03.1+devFixed in Version4.03.0+dev / +beta1 
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.
(0015675)
garrigue (manager)
2016-04-05 15:12

Fixed in 4.03 by the new exhaustuveness/redundancy check for GADTs.
But one could probably other (more involved) cases of asymmetry.

- 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 / +beta1
2016-04-05 14:57 doligez Target Version 4.03.0+dev / +beta1 => 4.03.1+dev
2016-04-05 15:12 garrigue Note Added: 0015675
2016-04-05 15:12 garrigue Status acknowledged => resolved
2016-04-05 15:12 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-04-05 15:12 garrigue Resolution open => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker