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 constructors observably change sharing of types #7800
Comments
Comment author: @stedolan Wow, this looks tricky. Here's a slightly simpler (but essentially the same) example that I found helpful in trying to understand the problem: let inc : int -> int = (+) 1
type 'a is_int = Int : int is_int
let foo (type a) (Int : a is_int) (x : a) = inc x This typechecks, but it breaks if inc is redefined as follows: type 'a fn = 'a -> 'a
let inc : int fn = (+) 1 |
Comment author: @garrigue Indeed, interactions between sharing and type abbreviations are an open issue since the introduction of polymorphic methods (more than 15 years ago), and I have no good solution. By the way, the problem is actually the other way round: the specification says that if a type is shared then the levels should go down simultaneously, so what you describe is actually the correct behavior. |
Comment author: @garrigue To make it clearer, the behavior of the compiler here is the correct one (read the formal specification). |
Comment author: @garrigue And this is of course principal: if you add typing constraints, you increase the risk of failure. |
Comment author: @lpw25 Just to be clear, the current behaviour is not principal:
but you're saying that the problem should actually be fixed by enforcing the hidden sharing, since that is what the formal specification does (which one by the way? The semi-implicit polymorphism one?). I would suggest that this just shows that it is a bad formal specification. You have two types which are equal under type equality but which cannot be substituted one for another without breaking typing. The types don't even necessarily print differently! This example is just terrible:
|
Comment author: @garrigue This is exactly what I said in my previous answer: a type abbreviation which is not shared inside will hide the sharing, which of course loses the principality of sharing-tracking. The problem is that the specification was written without considering type abbreviations :-( Now, if you have a better specification that guarantees principality (at least in theory), then I'm interested. The fact the sharing is not printed is another problem. Printing it by default would confuse people. We could have a switch to do that, if debugging this really becomes a problem. |
Comment author: @garrigue Actually, there is a reasonably simple way to fix the hiding of sharing: in Tconstr, keep the expanded version of the abbreviation, at least until it is fully generalized. It is actually already there, in the memo field (to allow building regular types), but gets erased every time the environment is updated, and also by generalize_structure. |
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. |
I'm not sure what to do with issues like this. The problem still exists but we're not going to fix it with the current type checker implementation. However, we'd probably want to look at it as part of the "high road" work on a new type checker implementation. |
Then I'm taking the liberty to close. The resolution is too far in the future. |
Original bug ID: 7800
Reporter: @lpw25
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2018-06-10T14:38:41Z)
Resolution: open
Priority: normal
Severity: minor
Category: typing
Monitored by: @hhugo @yakobowski
Bug description
The following code type checks without issue:
However, if the type annotation on
ints
is changed fromint * int
toint pair
then we get an error:Since these two types are equal this obviously shouldn't happen, and it is also easy to show that this is not principal.
The underlying issue is that when we instantiate the type
int pair
we only create a single copy of theint
types, and so the expansion toint * int
shares the same type for bothint
s. Even thoughint
is "structure" (i.e. not a variable) it is still a mutable piece of state due to its level and scope. So anything which depends on these pieces of state (e.g. GADT ambiguity detection) is affected by the difference in sharing.This is a fairly fundamental issue. Much like #7636 the theoretical fix is just to always expand out aliases, but obviously we don't want to do that. An alternative would be to delay instantiation of type constructor parameters until after expansion. I think this is a viable fix and may even improve performance on average by avoiding unnecessary instantiation.
The text was updated successfully, but these errors were encountered: