Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006023OCamlOCaml typingpublic2013-05-28 17:432014-09-24 16:52
Reporterfrisch 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target Versionafter-4.02.1Fixed in Version 
Summary0006023: Type-based selection of GADT constructors
DescriptionType-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?
Tagspatch
Attached Filesdiff file icon disambiguate_gadt.diff [^] (11,573 bytes) 2013-07-04 09:07 [Show Content]

- Relationships

-  Notes
(0009368)
garrigue (manager)
2013-05-29 06:13

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?
(0009369)
frisch (developer)
2013-05-29 09:59
edited on: 2013-05-29 09:59

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

(0009681)
garrigue (manager)
2013-07-04 09:09

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.
(0009683)
frisch (developer)
2013-07-04 10:07

Can you give an example where the trick about warnings is required?
(0009684)
garrigue (manager)
2013-07-04 10:41

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 = <fun>
(0009685)
frisch (developer)
2013-07-04 11:42

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?
(0009686)
frisch (developer)
2013-07-04 11:57

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).
(0009687)
garrigue (manager)
2013-07-04 11:57

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.
(0009688)
frisch (developer)
2013-07-04 12:00

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

Just restoring the list of pending warnings taken before the snapshot point.
(0009722)
frisch (developer)
2013-07-08 15:21

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?

- Issue History
Date Modified Username Field Change
2013-05-28 17:43 frisch New Issue
2013-05-29 06:13 garrigue Note Added: 0009368
2013-05-29 06:13 garrigue Assigned To => garrigue
2013-05-29 06:13 garrigue Status new => feedback
2013-05-29 09:59 frisch Note Added: 0009369
2013-05-29 09:59 frisch Status feedback => assigned
2013-05-29 09:59 frisch Note Edited: 0009369 View Revisions
2013-07-04 09:07 garrigue File Added: disambiguate_gadt.diff
2013-07-04 09:09 garrigue Note Added: 0009681
2013-07-04 10:07 frisch Note Added: 0009683
2013-07-04 10:41 garrigue Note Added: 0009684
2013-07-04 11:42 frisch Note Added: 0009685
2013-07-04 11:57 frisch Note Added: 0009686
2013-07-04 11:57 garrigue Note Added: 0009687
2013-07-04 12:00 frisch Note Added: 0009688
2013-07-08 15:21 frisch Note Added: 0009722
2013-07-12 17:03 doligez Target Version => 4.02.0+dev
2013-07-12 18:15 doligez Target Version 4.02.0+dev => 4.01.1+dev
2013-12-16 16:04 doligez Tag Attached: patch
2014-05-25 20:20 doligez Target Version 4.01.1+dev => 4.02.0+dev
2014-08-18 20:36 doligez Target Version 4.02.0+dev => 4.02.1+dev
2014-09-04 00:25 doligez Target Version 4.02.1+dev => undecided
2014-09-24 16:52 doligez Target Version undecided => after-4.02.1


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker