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

Do not allow capability subtyping when checking constraint subtyping. #1816

Merged
merged 2 commits into from Apr 7, 2017

Conversation

Projects
None yet
3 participants
@plietar
Contributor

plietar commented Apr 6, 2017

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

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.


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.

@jemc

This comment has been minimized.

Member

jemc commented Apr 6, 2017

@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.

@SeanTAllen

This comment has been minimized.

Member

SeanTAllen commented Apr 6, 2017

@jemc I think this is worthy of a release, all of @plietar's ones are. Thoughts?

@jemc

This comment has been minimized.

Member

jemc commented Apr 6, 2017

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.

Do not allow capability subtyping when checking constraint subtyping.
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 plietar force-pushed the plietar:constrain-eq-cap branch from 65b0b39 to 7c154bf Apr 6, 2017

@plietar

This comment has been minimized.

Contributor

plietar commented Apr 6, 2017

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.

"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";

This comment has been minimized.

@jemc

jemc Apr 6, 2017

Member

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.

@jemc jemc merged commit bf1f76e into ponylang:master Apr 7, 2017

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

ponylang-main added a commit that referenced this pull request Apr 7, 2017

@SeanTAllen SeanTAllen referenced this pull request Apr 7, 2017

Closed

Release 0.13.0 #1823

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment