Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

another broken GADT exhaustiveness check #6403

Closed
vicuna opened this issue May 7, 2014 · 9 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented May 7, 2014

Original bug ID: 6403
Reporter: @gasche
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:14:46Z)
Resolution: fixed
Priority: low
Severity: minor
Version: 4.02.0+dev
Target version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Has duplicate: #6801
Related to: #6437 #6598
Child of: #5998
Monitored by: @yallop

Bug 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 =

File attachments

@vicuna

This comment has been minimized.

Copy link
Author

commented May 7, 2014

Comment author: @yallop

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

@vicuna

This comment has been minimized.

Copy link
Author

commented May 7, 2014

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented May 11, 2014

Comment author: @garrigue

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

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 27, 2015

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 27, 2015

Comment author: @yallop

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 _ -> ()

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 28, 2015

Comment author: @garrigue

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?

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 28, 2015

Comment author: @yallop

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.)

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 30, 2015

Comment author: @garrigue

See #6437 for a more powerful patch.

@vicuna

This comment has been minimized.

Copy link
Author

commented Oct 23, 2015

Comment author: @garrigue

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.