-
Notifications
You must be signed in to change notification settings - Fork 1.2k
Incorrect exhaustiveness warning with GADTs #6395
Description
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)