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
Type-based selection of GADT constructors #6023
Comments
Comment author: @garrigue This is not particularly difficult to allow it.
Yet, I'm wondering what kind of code you are using that creates so much need of type-based selection. |
Comment author: @alainfrisch
We have a variety of ways to inspect values representing types at runtime. One of them looks like: type _ head = val head: 'a ty -> 'a head And we'd like to write: match Ttype.head ty with
If we open the module defining the GADT, it becomes a matter of constructor overloading (the same constructors are used to represent variants or in any concrete representation of types, etc). We'd prefer not having to do it; then it's a matter of "using constructors without opening their module". |
Comment author: @garrigue Added a patch disambiguating GADTs, based on backtracking. |
Comment author: @alainfrisch Can you give an example where the trick about warnings is required? |
Comment author: @garrigue It's just that we end up typing the same pattern twice. Here is an example without the log: module M : sig type _ t = Int : int t endlet f (type a) (x : a M.t) (y : a) = match x with Int -> y+1;; |
Comment author: @alainfrisch I'd suggest to "backtrack" warnings (generated during the first pass) as well instead of keeping a log. One simple possibility would be to report warnings using add_delayed_check, and take a snapshot of the delayed_checks reference (in addition to Btype.snapshot). The only drawback I can see is that delayed_checks are not run in case of a fatal typing error, but this is minor. Otherwise, we can just have a notion of "suspended warning mode", where calls to print_warning collects the warning in a list which is flushed when we leave that mode. Do you agree that backtracking warnings is preferable? |
Comment author: @alainfrisch Actually, it would probably be a good idea to always collect warnings instead of printing them on the fly (and only print them after type-checking is finished, even in case of error). This makes it very simple to backtrack them, and also to sort them by increased location (nicer to the user and more robust w.r.t. non-regression tests). |
Comment author: @garrigue In this precise case, backtracking or avoiding duplication of warnings should not make a difference: we're going to have the same warnings anyway. |
Comment author: @alainfrisch
Just restoring the list of pending warnings taken before the snapshot point. |
Comment author: @alainfrisch I'm still unclear about the need for having two code paths (and backtracking). What happens if we always follow the GADT path? Is it only a matter of performance, or is there something deeper? |
Comment author: @garrigue The GADT code path is more intricate. A first step might be to simplify the GADT code path, but I have no idea. |
Original bug ID: 6023
Reporter: @alainfrisch
Assigned to: @garrigue
Status: resolved (set by @gasche on 2018-06-12T03:36:18Z)
Resolution: fixed
Priority: normal
Severity: feature
Target version: later
Fixed in version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Tags: patch
Has duplicate: #6852
Child of: #6951
Monitored by: @Drup @gasche @alainfrisch
Bug description
Type-based selection of constructors currently does not work for GADTs. This is a known limitation (with an explicit error message), which we encounter quite often. Any hope to have it fixed, or is it really difficult?
File attachments
The text was updated successfully, but these errors were encountered: