Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006403OCamlOCaml typingpublic2014-05-07 18:102014-10-04 14:04
Reportergasche 
Assigned Togarrigue 
PrioritylowSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.02.0+dev 
Target Version4.03.0+devFixed in Version 
Summary0006403: another broken GADT exhaustiveness check
Description        OCaml version 4.02.0+dev5-2014-04-29

# type (_, _) eq = Refl : ('a, 'a) eq;;
# type empty = { bottom : 'a . 'a };;
# type ('a, 'b) sum = Left of 'a | Right of 'b;;

# let notequal : ((int, bool) eq, empty) sum -> empty = function
    | Right empty -> empty;;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Left _
val notequal : ((int, bool) eq, empty) sum -> empty = <fun>
TagsNo tags attached.
Attached Files

- Relationships
related to 0006598acknowledgedgarrigue lack of syntax for pattern-matching with no branches 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0011390)
yallop (developer)
2014-05-07 18:23

Hmm. I'm not sure I agree that we should be giving a warning here. The pattern 'Left _' is valid in that context (since it doesn't introduce new type equalities) even if there are no values that match it (which is something we can't determine in general).

We also accept the following simpler examples, and should probably continue to do so, even though neither function can ever be called by a well-typed program:

Example 1 (note that replacing '_' with 'Refl' causes typechecking to fail):

  type (_, _) eq = Refl : ('a, 'a) eq;;
  let unexamined : (int, bool) eq -> unit = fun _ -> ()

Example 2 (no GADTs, but there's no value that can be bound to 'bottom'):

  type empty = { bottom: 'a. 'a }
  let ex_falso_quodlibet : empty -> 'a = fun { bottom } -> bottom
(0011396)
garrigue (manager)
2014-05-07 23:21

The exhaustiveness check is known to be incomplete: it cannot prove all impossible cases to be impossible. So this is not really a bug.
This example comes from the fact it only tries to negate positions that are at least matched once, to avoid a combinatory explosion.
I'll try to see whether this can be improved, without changing the complexity.
(0011421)
garrigue (manager)
2014-05-11 09:53

There is no real need to fix, as this is not a bug, but a more clever algorithm could help.

- Issue History
Date Modified Username Field Change
2014-05-07 18:10 gasche New Issue
2014-05-07 18:11 gasche Relationship added child of 0005998
2014-05-07 18:23 yallop Note Added: 0011390
2014-05-07 23:21 garrigue Note Added: 0011396
2014-05-11 09:53 garrigue Note Added: 0011421
2014-05-11 09:53 garrigue Assigned To => garrigue
2014-05-11 09:53 garrigue Status new => acknowledged
2014-07-16 18:21 doligez Target Version => 4.03.0+dev
2014-10-04 14:04 gasche Relationship added related to 0006598


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker