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
Comments
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;; Example 2 (no GADTs, but there's no value that can be bound to 'bottom'): type empty = { bottom: 'a. 'a } |
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. |
Comment author: @garrigue There is no real need to fix, as this is not a bug, but a more clever algorithm could help. |
Comment author: @garrigue The attached patch fixes the problem. In the above example it means that the missing pattern (Left _) is converted to (Left Refl), which is eventually disproved. |
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 = 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 = |
Comment author: @garrigue The problem with redundancy is orthogonal. 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? |
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 (Of course, guards already violate these properties, but I still think there's value in maintaining them as far as possible.) |
Comment author: @garrigue Branch gadt-warnings was merged in trunk at revision 16532. |
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
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
The text was updated successfully, but these errors were encountered: