Do not allow capability subtyping when checking constraint subtyping. #1816
Conversation
|
@plietar - Yes, this looks like the right solution to me. Great work finding it. If you want to add your test case(s) to the PR, I think we can merge it. |
jemc
added
the
changelog - fixed
|
Yeah, I think all the type system bugs are definitely important enough to warrant a release. The only reason we may want to hold back on releasing them would be if we wanted to fit more than one of these bugfixes in before the release. So I'd just suggest we check in with @plietar to see if he's planning to file any more bugfixes in the near future that might want to make us wait for those for the next release. |
The compiler currently allows contravariant constraint for type
arguments. When doing so it allows capability subtyping.
In other words, it allows the following, where `X` is a type variable,
`λ` a capability and `DS` is a type name.
```
λ' ≤ λ
----------------------------------------
fun m[X: DS λ]() ≤ fun m[X: DS λ']()
```
This is however unsound, as shown in the example below. Bar's `alias`
method is able to create an `X^` from a `X!`, since `X` is a tag.
However, Foo's `alias` method is callable with an iso argument.
As a result, this can be used to duplicate an iso reference, as shown in
`Main`
```pony
trait Foo
fun alias[X: Any iso](x: X!) : X^
class Bar is Foo
fun alias[X: Any tag](x: X!) : X^ => x
class Baz
actor Main
new create(env: Env) =>
let foo : Foo = Bar
let x : Baz iso = Baz
let x' : Baz iso = foo.alias[Baz iso](x)
```
Instead, when checking constraint subtyping, the compiler should not
allow capabilities to be subtyped. This is similar to how type arguments
are checked to be within the constraint.
plietar
force-pushed
the
constrain-eq-cap
branch
from
65b0b39 to
7c154bf
Compare
|
I've added a test for this PR, it should be good to merge now. We should probably fix #1798 and make a release with the two, although I'm not sure how hard it is to fix. I've had a look at it and I have a few clues of what's going on, but I am not (yet) familiar enough with the typechecker implementation to fix it myself. I'll add a few notes over there. The other issues are about valid but fairly exotic programs which the compiler refuses/crashes on. Since they don't cause any unsoundness they are less important to fix and release IMO. I don't have anything else in the queue atm. |
test/libponyc/badpony.cc
Outdated
| "trait T\n" | ||
| " fun alias[X: Any iso](x: X!) : X^\n" | ||
| "class C is T\n" | ||
| " fun alias[X: Any tag](x: X!) : X^ => x\n"; |
There was a problem hiding this comment.
It's a small style point, but could you remove the "extra" space before the colon that precedes the return type?
This would make it more closely match the prevailing style in these tests and in the standard libraries.
SeanTAllen
added
the
triggers release
The compiler currently allows contravariant constraint for type arguments. When
doing so it allows capability subtyping.
In other words, it allows the following, where
Xis a type variable,λacapability and
DSis a type name.This is however unsound, as shown in the example below. Bar's
aliasmethod isable to create an
X^from aX!, sinceXis a tag. However, Foo'saliasmethod is callable with an iso argument.
As a result, this can be used to duplicate an iso reference, as shown in
MainInstead, when checking constraint subtyping, the compiler should not allow
capabilities to be subtyped. This is similar to how type arguments are
checked to be within the constraint.
Playground link with a more complete example: https://is.gd/vYNExP
I'll add tests soon, but I wanted to check first if this solution sounds right.