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
equality, moregen and unification force expansion of large, non-recursive type constructors #6970
Comments
Comment author: @garrigue I've added 2 patches. large_classes2 is a fix of your patch. It registers the type pair, for recursion going through parameters (see tests/typing-labels/mixin.ml), and backtracks in moregen to undo side-effects. It seems correct to me, but I have a slight concern about performance: it may actually be slower than just expanding in some cases. It is hard to measure. Also, currently the testsuite goes through (everything compiles), but some types are printed wrongly. Try doing |
Comment author: choeger The seemingly redundant expansion was required in practice, since compiling the 4.02.3 branch without yielded a "incosistent assumptions" error regarding the signature of hashtabl. I really do not understand why this occured, maybe I just misused the build system ;). |
Comment author: choeger
That is one aspect, I do not understand about injectivity analysis: When 'a is constrained by some type variable 'b and 'b is injective, how can 'a ever vanish through expansion? |
Comment author: @garrigue
This is the other way round: the expanded type is <m_1 : 'b; m_2 : 'b>. |
Comment author: choeger True. But that is not a problem, since (my understanding of) injectivity only gives t1 = t2 => t1 c = t2 c So IMO c is injective in its argument, since there exists a type variable that is bound by some constraint on its argument and appears in the expansion. Is that not correct? |
Comment author: @garrigue This one is not injectivity, but just functional equality, which is valid for any type definition (a type is entirely determined by its parameters). |
Comment author: choeger Of course. Sorry, that was plain wrong. |
Comment author: @garrigue Downgrade to feature, as it's not clear how big are the types we should actively support. |
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: 6970
Reporter: choeger
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2015-08-26T09:01:34Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.3
Target version: later
Category: typing
Monitored by: @gasche
Bug description
When a large hierarchy of type constructors shall be compiled, the type checking forces all constructors to be expanded early (to reduce potential non-injective arguments). This leads to a lot more work than actually necessary (at least O(n²) instead of O(n) for n constructors of the same complexity).
An example hierarchy can be created by the attached zsh script. The attached patch fixes the issue for Ctype.moregen and Ctype.eqtype, but is possibly unsound in the case of moregen (I simply do not understand the required side-effects here).
Steps to reproduce
Run the attached script and try to compile m_9.ml
File attachments
The text was updated successfully, but these errors were encountered: