Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006403OCamlOCaml typingpublic2014-05-07 18:102015-10-23 10:35
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.02.0+dev 
Target Version4.03.0+devFixed in Version4.03.0+dev 
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 Filesdiff file icon parmatch_nested_gadt.diff [^] (6,200 bytes) 2015-04-27 12:08 [Show Content]

- Relationships
has duplicate 0006801resolvedgarrigue Exhaustiveness messages for GADTs suggest patterns that will not type check 
related to 0006598resolvedgarrigue lack of syntax for pattern-matching with no branches 
related to 0006437resolvedgarrigue GADT exhaustiveness check incompleteness 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
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
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.
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.
garrigue (manager)
2015-04-27 12:13

The attached patch fixes the problem.
The idea is to expand gadts that appear as arguments to a non-gadt sum type.
(The restriction to non-gadt sum types is to avoid the need to backtrack unification)

In the above example it means that the missing pattern (Left _) is converted to (Left Refl), which is eventually disproved.
More experiments would be needed to see whether there is a large associated cost.
yallop (developer)
2015-04-27 12:50

Is it possible to extend the patch to do a little more with redundancy? For example, the following code no longer gives an exhaustiveness warning:

   let f : (int, (int, string) eql) sum -> unit =
     function Left _ -> ()

but if you add a case for Right then there's no warning that it's redundant:

   let f : (int, (int, string) eql) sum -> unit =
     function Left _ -> () | Right _ -> ()
garrigue (manager)
2015-04-28 15:43

The problem with redundancy is orthogonal.
The algorithm used there is a bit optimized, and doesn't take gadts into account.
It would be easy to just reuse the code for exhaustiveness, but this would mean repeating the same computation again for each extra line.

I personally never cared much about redundancy (it is not a soundness problem), but do you see cases where missing a warning makes a difference?
yallop (developer)
2015-04-28 16:10

I think consistent warnings make a difference in understanding the code. Long-time ML programmers tend to interpret a lack of redundancy warnings as an indication that every branch is reachable.

It's useful to have the properties that

(1) removing cases from the end of an exhaustive match causes an exhaustivity warning
(2) adding cases to the end of an exhaustive match causes a redundancy warning

(Of course, guards already violate these properties, but I still think there's value in maintaining them as far as possible.)
garrigue (manager)
2015-04-30 14:02

See PR#6437 for a more powerful patch.
garrigue (manager)
2015-10-23 10:35

Branch gadt-warnings was merged in trunk at revision 16532.

- 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
2015-04-27 12:08 garrigue File Added: parmatch_nested_gadt.diff
2015-04-27 12:13 garrigue Note Added: 0013738
2015-04-27 12:21 garrigue Relationship added related to 0006437
2015-04-27 12:29 garrigue Relationship added has duplicate 0006801
2015-04-27 12:50 yallop Note Added: 0013741
2015-04-28 15:43 garrigue Note Added: 0013744
2015-04-28 16:10 yallop Note Added: 0013745
2015-04-30 14:02 garrigue Note Added: 0013769
2015-10-23 10:35 garrigue Note Added: 0014608
2015-10-23 10:35 garrigue Status acknowledged => resolved
2015-10-23 10:35 garrigue Fixed in Version => 4.03.0+dev
2015-10-23 10:35 garrigue Resolution open => fixed

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker