-
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
Merged
Merged
Changes from all commits
Commits
Show all changes
18 commits
Select commit
Hold shift + click to select a range
3750dc6
refactor box adaptation
Linyxus ecf174b
refactor box inference again
Linyxus 0c96672
always box args of HKTypeLambda
Linyxus 297301c
debug tracing for box adaptation
Linyxus e0afeb9
cleanup
Linyxus f2bc25e
Revert "always box args of HKTypeLambda"
Linyxus 43ca7c6
strip nested capturing types before box adaptation
Linyxus ae3f52e
update check files after refactoring box adaptation
Linyxus 023283d
add box adaptation for poly functions
Linyxus daf6766
update test check files
Linyxus 363f142
refactor box adaptation
Linyxus 577b3a5
documenting box adaptation functions
Linyxus 3be18f5
add box adaptation test cases
Linyxus 21e90e2
Fix doc
Linyxus 7deb2b0
use named arg for nestedInOwner
Linyxus 0cf2f20
rename cs1 to leaked for better readability
Linyxus 3e690a8
remove markSolved
Linyxus 65e42d3
destruct expected type as (type-)functions with more rationale
Linyxus File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,38 @@ | ||
| trait Cap | ||
|
|
||
| def main(io: {*} Cap, fs: {*} Cap): Unit = { | ||
| val test1: {} Unit -> Unit = _ => { // error | ||
| type Op = [T] -> ({io} T -> Unit) -> Unit | ||
| val f: ({io} Cap) -> Unit = ??? | ||
| val op: Op = ??? | ||
| op[{io} Cap](f) | ||
| // expected type of f: {io} (box {io} Cap) -> Unit | ||
| // actual type: ({io} Cap) -> Unit | ||
| // adapting f to the expected type will also | ||
| // charge the environment with {io} | ||
| } | ||
|
|
||
| val test2: {} Unit -> Unit = _ => { | ||
| type Box[X] = X | ||
| type Op0[X] = Box[X] -> Unit | ||
| type Op1[X] = Unit -> Box[X] | ||
| val f: Unit -> ({io} Cap) -> Unit = ??? | ||
| val test: {} Op1[{io} Op0[{io} Cap]] = f | ||
| // expected: {} Unit -> box {io} (box {io} Cap) -> Unit | ||
| // actual: Unit -> ({io} Cap) -> Unit | ||
| // | ||
| // although adapting `({io} Cap) -> Unit` to | ||
| // `box {io} (box {io} Cap) -> Unit` will leak the | ||
| // captured variables {io}, but since it is inside a box, | ||
| // we will charge neither the outer type nor the environment | ||
| } | ||
|
|
||
| val test3 = { | ||
| 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[{fs} Id[{io} Cap]] = f // error | ||
| val h: {} Op[{io} Id[{io} Cap]] = f | ||
| } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| trait Cap { def use(): Int } | ||
|
|
||
| def test1(): Unit = { | ||
| type Id[X] = [T] -> (op: X => T) -> T | ||
|
|
||
| val x: Id[{*} Cap] = ??? | ||
| x(cap => cap.use()) // error | ||
| } | ||
|
|
||
| def test2(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: X -> T) -> T | ||
|
|
||
| val x: Id[{io} Cap] = ??? | ||
| x(cap => cap.use()) // error | ||
| } | ||
|
|
||
| def test3(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {io} X -> T) -> T | ||
|
|
||
| val x: Id[{io} Cap] = ??? | ||
| x(cap => cap.use()) // ok | ||
| } | ||
|
|
||
| def test4(io: {*} Cap, fs: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {io} X -> T) -> T | ||
|
|
||
| val x: Id[{io, fs} Cap] = ??? | ||
| x(cap => cap.use()) // error | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,14 @@ | ||
| trait Cap | ||
|
|
||
| def test1(io: {*} Cap) = { | ||
| type Op[X] = [T] -> Unit -> X | ||
| val f: Op[{io} Cap] = ??? | ||
| val x: [T] -> Unit -> ({io} Cap) = f // error | ||
| } | ||
|
|
||
| def test2(io: {*} Cap) = { | ||
| type Op[X] = [T] -> Unit -> {io} X | ||
| val f: Op[{io} Cap] = ??? | ||
| val x: Unit -> ({io} Cap) = f[Unit] // error | ||
| val x1: {io} Unit -> ({io} Cap) = f[Unit] // ok | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| trait Cap { def use(): Int } | ||
|
|
||
| def test1(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {io} X -> T) -> T | ||
|
|
||
| val x: Id[{io} Cap] = ??? | ||
| val f: ({*} Cap) -> Unit = ??? | ||
| x(f) // ok | ||
| // actual: {*} Cap -> Unit | ||
| // expected: {io} box {io} Cap -> Unit | ||
| } | ||
|
|
||
| def test2(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {*} X -> T) -> T | ||
|
|
||
| val x: Id[{*} Cap] = ??? | ||
| val f: ({io} Cap) -> Unit = ??? | ||
| x(f) // error | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| trait Cap { def use(): Int } | ||
|
|
||
| def test1(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {io} X -> T) -> T | ||
|
|
||
| val x: Id[{io} Cap] = ??? | ||
| x(cap => cap.use()) // ok | ||
| } | ||
|
|
||
| def test2(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {io} (x: X) -> T) -> T | ||
|
|
||
| val x: Id[{io} Cap] = ??? | ||
| x(cap => cap.use()) | ||
| // should work when the expected type is a dependent function | ||
| } | ||
|
|
||
| def test3(io: {*} Cap): Unit = { | ||
| type Id[X] = [T] -> (op: {} (x: X) -> T) -> T | ||
|
|
||
| val x: Id[{io} Cap] = ??? | ||
| x(cap => cap.use()) // error | ||
| } |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.