Skip to content
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

Exhaustiveness messages for GADTs suggest patterns that will not type check #6801

vicuna opened this issue Mar 3, 2015 · 2 comments
bug duplicate typing typing-GADTS


Copy link

@vicuna vicuna commented Mar 3, 2015

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 "", 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!

Copy link

@vicuna vicuna commented May 18, 2015

Comment author: @garrigue

See #6437 for a patch which solves this problem.

Copy link

@vicuna vicuna commented Oct 23, 2015

Comment author: @garrigue

Branch gadt-warnings was merged in trunk at revision 16532.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
bug duplicate typing typing-GADTS
None yet

No branches or pull requests

3 participants