We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Original bug ID: 6395 Reporter: @yallop Assigned to: @garrigue Status: closed (set by @xavierleroy on 2017-09-24T15:32:13Z) Resolution: fixed Priority: normal Severity: minor Target version: 4.03.1+dev Fixed in version: 4.03.0+dev / +beta1 Category: typing Child of: #5998 Monitored by: @hcarty
Given the following type definitions:
type p = P type q = Q
type _ t = X : bool -> p t | Y : q t
the following code correctly compiles without exhaustiveness warnings
let f : type a. a t * a t -> unit = function | X _, X _ -> () | Y, Y -> ()
but the following code
let g : type a. a t * a t -> unit = function | x, X false -> () | X _, X _ -> () | Y, Y -> ()
gives a warning:
Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (Y, X true)
The text was updated successfully, but these errors were encountered:
Comment author: @garrigue
Another example which shows that the GADT exhaustiveness check, while sound, is extremely fragile.
Sorry, something went wrong.
Fixed in 4.03 by the new exhaustuveness/redundancy check for GADTs. But one could probably other (more involved) cases of asymmetry.
garrigue
No branches or pull requests
Original bug ID: 6395
Reporter: @yallop
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:13Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.03.1+dev
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Child of: #5998
Monitored by: @hcarty
Bug description
Given the following type definitions:
type p = P
type q = Q
type _ t =
X : bool -> p t
| Y : q t
the following code correctly compiles without exhaustiveness warnings
let f : type a. a t * a t -> unit = function
| X _, X _ -> ()
| Y, Y -> ()
but the following code
let g : type a. a t * a t -> unit = function
| x, X false -> ()
| X _, X _ -> ()
| Y, Y -> ()
gives a warning:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(Y, X true)
The text was updated successfully, but these errors were encountered: