Skip to content

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

Merged
merged 18 commits into from
Oct 15, 2022
Merged

Several fixes to box inference #16141

merged 18 commits into from
Oct 15, 2022

Conversation

Linyxus
Copy link
Contributor

@Linyxus Linyxus commented Oct 4, 2022

Inspired by the formalism, this PR changes the box adaptation logic to fix a bunch of problems.

The main fixes:

  • Correctly charging the capture set of the type being adapted. For example, the following code snippet should fail:
type Id[X] = [T] -> (op: X -> T) -> T
val x: Id[{io} Cap] = ???
x(cap => cap.use())  // error

Denote cap => cap.use() as f. 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.

  • Stop the newly-captured variables from escaping a box. Specifically, assuming that T is a function type, if the actual type is T while the expected type is □ U, the variables captured when adapting T to U will not get charged to the outer environment. For example, the following code should compile:
type Box[X] = X
type Id[X] = Box[X] -> Unit
type Op[X] = Unit -> Box[X]
val f: Unit -> ({io} Cap) -> Unit = ???
val g: {} Op[{io} Id[{io} Cap]] = f

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 an unbox is inferenced, outermost capture set is still empty due to the box we insert, which conforms to the expectation.

Besides, it also adds the support to adapting polymorphic function types.

@odersky odersky self-assigned this Oct 6, 2022
@Linyxus Linyxus requested a review from odersky October 7, 2022 07:40
Copy link
Contributor

@odersky odersky left a 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
Copy link
Contributor

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?

Copy link
Contributor Author

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.

@odersky odersky assigned Linyxus and unassigned odersky Oct 10, 2022
@Linyxus
Copy link
Contributor Author

Linyxus commented Oct 14, 2022

Thanks for your comment! I have addressed the reviews and the main changes include:

  • Named args and renaming to make the code easier to understand.
  • Remove the incorrect usage of markSolved and fix a limitation when comparing the function types in TypeComparer to make things work.
  • Improve the way of destructing expected type in adaptFun and adaptTypeFun to make them match better with each other and have a clear rationale.

@Linyxus Linyxus requested a review from odersky October 14, 2022 11:48
Copy link
Contributor

@odersky odersky left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@odersky odersky merged commit 92f6b8c into scala:main Oct 15, 2022
@Kordyjan Kordyjan added this to the 3.2.2 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants