Skip to content
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

Unmapped type from capture checking with levels #18554

Open
EugeneFlesselle opened this issue Sep 14, 2023 · 1 comment
Open

Unmapped type from capture checking with levels #18554

EugeneFlesselle opened this issue Sep 14, 2023 · 1 comment
Labels
area:experimental:cc Capture checking related

Comments

@EugeneFlesselle
Copy link
Contributor

Adding MapView to the capture checking standard library tests (here) works fine before using levels for capture escape checking.

However, on the main branch after #18463, we get the following error:

-- [E007] Type Mismatch Error: tests/pos-special/stdlib/collection/MapView.scala:45:99 ---------------------------------
45 |  override def filterKeys(p: K => Boolean): MapView[K, V]^{this, p} = new MapView.FilterKeys(this, p)
   |                                                                                                   ^
   |                                                                                    Found:    K ->{p} Boolean
   |                                                                                    Required: box K^? => Boolean
   |--------------------------------------------------------------------------------------------------------------------
   | Explanation (enabled by `-explain`)
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |
   | Tree: p
   | I tried to show that
   |   K ->{p} Boolean
   | conforms to
   |   box K^? => Boolean
   | but the comparison trace ended with `false`:
   |
   |   ==> K ->{p} Boolean  <:  box K^? => Boolean
   |     ==> subcaptures {p} <:< {cap} 
   |     <== subcaptures {p} <:< {cap}  = {cap}
   |     ==> subcaptures {p} <:< {cap} 
   |     <== subcaptures {p} <:< {cap}  = {cap}
   |   <== K ->{p} Boolean  <:  box K^? => Boolean = false
   |
   | The tests were made under the empty constraint
    --------------------------------------------------------------------------------------------------------------------

I still expected it to conform, but I am not familiar with the new changes using levels.

@EugeneFlesselle EugeneFlesselle added the stat:needs triage Every issue needs to have an "area" and "itype" label label Sep 14, 2023
@EugeneFlesselle
Copy link
Contributor Author

Explicitly declaring the self type of MapView also introduces the following error (not present before levels):

-- [E007] Type Mismatch Error: tests/pos-special/stdlib/collection/MapView.scala:46:93 ---------------------------------
46 |  override def filterKeys(p: K => Boolean): MapView[K, V]^{this, p} = new MapView.FilterKeys(this, p)
   |                                                                                             ^^^^
   |            Found:    (MapView.this : scala.collection.MapView[K, V]^{cap[MapView]})
   |            Required: scala.collection.MapOps[box K^?, box V^?, scala.collection.MapView.SomeIterableConstr, ?]^
   |--------------------------------------------------------------------------------------------------------------------
   | Explanation (enabled by `-explain`)
   |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   |
   | Tree: this
   | I tried to show that
   |   (MapView.this : scala.collection.MapView[K, V]^{cap[MapView]})
   | conforms to
   |   scala.collection.MapOps[box K^?, box V^?, scala.collection.MapView.SomeIterableConstr, ?]^
   | but the comparison trace ended with `false`:
   |
   |   ==> (MapView.this : scala.collection.MapView[K, V]^{cap[MapView]})  <:  scala.collection.MapOps[box K^?, box V^?, scala.collection.MapView.SomeIterableConstr, ?]^
   |     ==> subcaptures {MapView.this} <:< {cap} 
   |     <== subcaptures {MapView.this} <:< {cap}  = {cap}
   |     ==> scala.collection.MapView[K, V]^{MapView.this}  <:  scala.collection.MapOps[box K^?, box V^?, scala.collection.MapView.SomeIterableConstr, ?]^ (left is approximated)
   |       ==> subcaptures {MapView.this} <:< {cap} 
   |       <== subcaptures {MapView.this} <:< {cap}  = {cap}
   |       ==> subcaptures {MapView.this} <:< {cap} 
   |       <== subcaptures {MapView.this} <:< {cap}  = {cap}
   |     <== scala.collection.MapView[K, V]^{MapView.this}  <:  scala.collection.MapOps[box K^?, box V^?, scala.collection.MapView.SomeIterableConstr, ?]^ (left is approximated) = false
   |   <== (MapView.this : scala.collection.MapView[K, V]^{cap[MapView]})  <:  scala.collection.MapOps[box K^?, box V^?, scala.collection.MapView.SomeIterableConstr, ?]^ = false
   |
   | The tests were made under the empty constraint
    --------------------------------------------------------------------------------------------------------------------

@EugeneFlesselle EugeneFlesselle changed the title Capture checking levels introduce capability not covered by root Unmapped type from capture checking with levels Sep 15, 2023
@mbovel mbovel added area:experimental:cc Capture checking related and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Sep 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:experimental:cc Capture checking related
Projects
None yet
Development

No branches or pull requests

2 participants