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

Bug description

Exhaustiveness messages for GADTs are a bit off. They will suggest patterns need to be inserted for constructors that are not actually legal to insert because they will not type check.

A simple example:

type _ value =
| String : string -> string value
| Float : float -> float value
| Any

let print_string_value (x : string value) =
  match x with
  | String s -> print_endline s

The resulting message:

File "test.ml", line 7, characters 2-46:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(Float _|Any)

But of course, inserting a pattern for Float _ won't go very well!