-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Several fixes to box inference #16141
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
Conversation
This reverts commit 0c96672.
- special handling for the env created during box adaptation - rewrite `adapt` to make it cleaner and easier to understand
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Overall it looks really good!
try | ||
val (eargs, eres) = expected.dealias match | ||
case defn.FunctionOf(eargs, eres, _, _) => (eargs, eres) | ||
case expected => expected.stripped match |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why do you need a separate match on expected.stripped
?. Can't you match everything with expected.dealias
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The reason why stripped
is used here is because the expected type can have a capture set but dealias
does not drop the capturing annotation. However, I think what we want here is expected.dealias.stripCapturing
, just like what we do for type functions. I have changed this pattern matching in both adaptFun
and adaptTypeFun
to make them match with each other and have a better rationale.
Thanks for your comment! I have addressed the reviews and the main changes include:
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
Inspired by the formalism, this PR changes the box adaptation logic to fix a bunch of problems.
The main fixes:
Denote
cap => cap.use()
asf
. The expected type is(□ {io} Cap) -> Int
, while the actual type is({io} Cap) -> Int
. The function should be adapted as(x: □ {io} Cap) => f(unbox {io} x)
, whose capture set is{io}
because of the unbox.T
is a function type, if the actual type isT
while the expected type is□ U
, the variables captured when adaptingT
toU
will not get charged to the outer environment. For example, the following code should compile:The expected type of
f
in the last statement is{} Unit -> □ {io} (□ {io} Cap) -> Unit
. The function would be adapted as(x: Unit) => let g = (y: □ {io} Cap) => f(unbox {io} y) in box g
. Note that although anunbox
is inferenced, outermost capture set is still empty due to thebox
we insert, which conforms to the expectation.Besides, it also adds the support to adapting polymorphic function types.