Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006220OCamlOCaml typingpublic2013-11-02 17:482015-04-30 04:41
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version4.01.0 
Target Version4.03.0+devFixed in Version 
Summary0006220: GADT type information is not used to detect unused match cases
DescriptionIt seems that warning 11 ("this match case is unused") does not take account of the type information of GADTs.

For example:

  # type 'a t = I : int t | F : float t;;
  type 'a t = I : int t | F : float t

  # let f : int t -> int = function
      I -> 1;;
    val f : int t -> int = <fun>

  # let f : int t -> int = function
      I -> 1
    | _ -> 2;;
      val f : int t -> int = <fun>

I would have expected the second declaration of `f` to raise warning 11, but it does not.
TagsNo tags attached.
Attached Files

- Relationships
child of 0006437confirmedgarrigue GADT exhaustiveness check incompleteness 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0013740)
garrigue (manager)
2015-04-27 12:26

Indeed, the refined information is not used here.
Not completely clear how to do it, as inclusion is not easy in presence of gadts.

- Issue History
Date Modified Username Field Change
2013-11-02 17:48 lpw25 New Issue
2013-11-02 17:49 lpw25 Description Updated View Revisions
2014-05-30 15:20 shinwell Assigned To => garrigue
2014-05-30 15:20 shinwell Status new => assigned
2014-05-31 15:33 garrigue Relationship added child of 0006437
2014-07-16 17:39 doligez Target Version => 4.03.0+dev
2015-04-27 12:26 garrigue Note Added: 0013740
2015-04-30 04:41 garrigue Relationship added child of 0005998


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker