Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006220OCamlOCaml typingpublic2013-11-02 17:482015-12-04 01:46
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.01.0 
Target Version4.03.0+devFixed in Version4.03.0+dev 
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 0006437resolvedgarrigue 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.
(0015004)
frisch (developer)
2015-12-03 13:32

Now we get warning 56 ("this match case is unreachable"). Is this considered ok (or should warning 11 be raised) ? I did not follow the discussion about "_ -> ." clauses, but I don't see offhand why this should be a different warning number.
(0015023)
garrigue (manager)
2015-12-04 01:46

Solved together with its parent.

This has to be a different warning, because if a case is only unreachable (rather than unused), you cannot just remove it, but have to replace it by a refutation case.
Note that 56 is a subcase of 11: you only get warning 56 if both 11 and 56 are turned on.

- 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
2015-12-03 13:32 frisch Note Added: 0015004
2015-12-04 01:46 garrigue Note Added: 0015023
2015-12-04 01:46 garrigue Status assigned => closed
2015-12-04 01:46 garrigue Resolution open => fixed
2015-12-04 01:46 garrigue Fixed in Version => 4.03.0+dev


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker