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

Jump to bottom

« match e with p -> » does not generalize « e » #6057

Closed
vicuna opened this issue Jun 28, 2013 · 3 comments
Closed

« match e with p -> » does not generalize « e » #6057

vicuna opened this issue Jun 28, 2013 · 3 comments
Assignees
@garrigue
Labels
bug typing

Comments

@vicuna
Copy link

vicuna commented Jun 28, 2013

Original bug ID: 6057
Reporter: @protz
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:20:01Z)
Resolution: not a bug
Priority: normal
Severity: minor
Category: typing
Related to: #6014 #6056
Monitored by: @gasche

Bug description

If I recall correctly my master's internship, there's no theoretical reason why the following should work:

# let x, y = (fun x -> x), fun x -> x;;
val x : 'a -> 'a = 
val y : 'a -> 'a =

while the following does not:

# match (fun x -> x), fun x -> x with x, y -> x, y;;
- : ('_a -> '_a) * ('_b -> '_b) = (, )

In other words, when writing match e with p, e should be generalized.

Jacques, is that difficult to implement?

Additional information

(This was initially filed as a companion issue to #6056 to make sure we have a separate bug for the separate issue.)
@vicuna
Copy link
Author

vicuna commented Jun 28, 2013

Comment author: @alainfrisch

Adding a relation to #6014, the common point being "bring the type-checking of 'let' and 'match' closer to each other."

@vicuna
Copy link
Author

vicuna commented Jun 28, 2013

Comment author: @gasche

I plan to suggest a patch for this one bug (it seems very easy to fix). #6506 seems more delicate.

@vicuna
Copy link
Author

vicuna commented Jun 28, 2013

Comment author: @garrigue

Actually, e is already generalized, you could see in

match fun x -> x with f -> f 1, f true;;

What you are seeing in your example is just that the match construct itself is considered as expansive, which is an orthogonal issue (6056).

@vicuna vicuna closed this as completed Dec 11, 2015
@vicuna vicuna added the typing label Mar 14, 2019
This was referenced Mar 7, 2017
Closed
Closed
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@garrigue garrigue

Labels
bug typing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@garrigue @vicuna