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

Closed
vicuna opened this issue Mar 3, 2015 · 2 comments
Closed
Assignees
Labels
bug duplicate typing typing-GADTS GADT typing and exhaustiveness bugs
Milestone

Comments

@vicuna
Copy link

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

@vicuna
Copy link
Author

vicuna commented May 18, 2015

Comment author: @garrigue

See #6437 for a patch which solves this problem.

@vicuna
Copy link
Author

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
Labels
bug duplicate typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants