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
Existentials not allowed with 'let and' #6014
Comments
Comment author: @garrigue Indeed, |
Comment author: @alainfrisch Is there any hope to have "built-in" support for opening GADTs while type-checking let bindings? |
Comment author: @garrigue
There are several cases:
So don't hold your breath. |
Comment author: @gasche
How can the propagation be a problem? Can we run into, say, ambiguity errors that wouldn't have existed in absence of propagation? I think people would expect
Pattern-matching is not allowed as the defined-part of a let rec (only in function arguments), so I don't see how GADTs can be opened in that case. |
Comment author: @alainfrisch
My question was rather: can we support directly, at reasonable cost, the opening of GADTs existentials in the normal type-checking of let bindings, without going to an encoding into a "match". Non-recursive "let and" bindings are not very different from a sequence of single let bindings, except for scope management, but this does not seem very deep (we could just type-check each let-binding in the same initial environment, no?). So supporting them again by a translation to match cases should be doable (but it might not justify the effort, I agree). |
Comment author: @garrigue I don't think it would be a good idea to duplicate the code in type_let, as this just increases the chances for bugs. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
If anybody is still interested by that, we can go through the tuple encoding. |
I'm still in favour of this feature. But I'm not sure about the tuple encoding, especially for equalities. Currently let p1 = e1 and p2 = e2 in e can be (and is) evaluated in the order let p1, p2 = e1, e2 in e the order changes to |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 6014
Reporter: @yallop
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2013-05-14T10:33:02Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Related to: #6057
Monitored by: @gasche @lpw25 @alainfrisch
Bug description
Given
the following is accepted:
but a slight variant using 'let and' (or 'let rec and') is rejected:
with the message:
The text was updated successfully, but these errors were encountered: