Skip to content

Incorrect exhaustiveness warning with GADTs #6395

@vicuna

Description

@vicuna

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)

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions