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

Type-based selection of GADT constructors #6023

Closed
vicuna opened this issue May 28, 2013 · 12 comments
Closed

Type-based selection of GADT constructors #6023

vicuna opened this issue May 28, 2013 · 12 comments

Comments

@vicuna
Copy link

vicuna commented May 28, 2013

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

@vicuna
Copy link
Author

vicuna commented May 29, 2013

Comment author: @garrigue

This is not particularly difficult to allow it.
The only reason is that there are two code paths, depending on whether a pattern contains a GADT or not.
It can be done at least in two ways:

  • use only one code path, assuming that all patterns may contain GADTs
  • delay detection of GADTs, and use backtracking to revert to the GADT code path if needed

Yet, I'm wondering what kind of code you are using that creates so much need of type-based selection.
Is it constructor overloading, or using constructors without opening their module?

@vicuna
Copy link
Author

vicuna commented May 29, 2013

Comment author: @alainfrisch

Yet, I'm wondering what kind of code you are using that creates so much need of type-based selection.

We have a variety of ways to inspect values representing types at runtime. One of them looks like:

type _ head =
| Int: int head
| List: 'a. 'a ty -> 'a list head
| ...

val head: 'a ty -> 'a head

And we'd like to write:

match Ttype.head ty with
| Int -> ...
| List -> ...

Is it constructor overloading, or using constructors without opening their module?

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

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

Comment author: @garrigue

Added a patch disambiguating GADTs, based on backtracking.
Seems to work fine, but needed a trick to avoid spurious warning.
Also, this does not apply to let-in at this point.

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

Comment author: @alainfrisch

Can you give an example where the trick about warnings is required?

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

Comment author: @garrigue

It's just that we end up typing the same pattern twice.
So for instance warning 40 is going to be generated twice.
By keeping a log of generated warnings one can avoid that.
The log is reset each time check_fatal is called.
It should actually be done in a better way, keeping the location too.

Here is an example without the log:

module M : sig type _ t = Int : int t end

let f (type a) (x : a M.t) (y : a) = match x with Int -> y+1;;
Characters 50-53:
let f (type a) (x : a M.t) (y : a) = match x with Int -> y+1;;
^^^
Warning 40: Int was selected from type M.t.
It is not visible in the current scope, and will not
be selected if the type becomes unknown.
Characters 50-53:
let f (type a) (x : a M.t) (y : a) = match x with Int -> y+1;;
^^^
Warning 40: Int was selected from type M.t.
It is not visible in the current scope, and will not
be selected if the type becomes unknown.
val f : 'a M.t -> 'a -> int =

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

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?

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

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).

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

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.
In general I agree that the ability to delay warnings and replay them later would be useful.
I'm not sure what "backtrack" would mean for warnings.

@vicuna
Copy link
Author

vicuna commented Jul 4, 2013

Comment author: @alainfrisch

I'm not sure what "backtrack" would mean for warnings.

Just restoring the list of pending warnings taken before the snapshot point.

@vicuna
Copy link
Author

vicuna commented Jul 8, 2013

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?

@vicuna
Copy link
Author

vicuna commented Mar 19, 2015

Comment author: @garrigue

The GADT code path is more intricate.
Of course merging the two code-paths could help discover bugs.
However, these bugs may be hard to fix :-)
And the added complexity may make it harder to fix other bugs, by obscuring their cause.

A first step might be to simplify the GADT code path, but I have no idea.

@vicuna
Copy link
Author

vicuna commented Jun 12, 2018

Comment author: @gasche

This has been fixed in 4.07 by Thomas Refis:

#1648

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants