Ponyc: iso being a subtype of trn is unsound with covariant methods

[plietar]

class Counter

trait A
  fun ref get() : Counter trn

class B is A
  var f: Counter iso = Counter.create()
  fun ref get() : Counter iso => this.f

actor Main
  new create(env: Env) =>
    var b: B ref = B.create()
    var a: A ref = b

    var counter: Counter box = a.get()

    var counter': Counter iso = b.f = Counter.create()

Here the B class is correct because the return type Counter iso is a subtype of the return type in A, Counter trn.

However, in Main, the result of a.get() is aliased into a Counter box. There are now two stable paths to the same object, counter with type Counter box, and counter' with type Counter iso. This is a violation of the deny properties of iso.

This can be used to send the iso reference to the counter to another actor, while keeping the box one locally, which leads to data races.

class Counter
  var f: U32 = 0
  fun ref inc() =>
    this.f = this.f + 1

  fun box value() : U32 =>
    this.f

trait A
  fun ref get() : Counter trn

class B is A
  var f: Counter iso = Counter.create()

  fun ref get() : Counter iso => this.f

actor Main
  let counter: Counter box
  let env: Env

  new create(env': Env) =>
    this.env = env'

    var b: B ref = B.create()
    var a: A ref = b

    this.counter = a.get()

    let counter' : Counter iso = (b.f = Counter.create())

    Incrementer.increment(consume counter')
    this.print()

  be print() =>
    env.out.print(this.counter.value().string())
    this.print()

actor Incrementer
  be increment(counter: Counter iso) =>
    counter.inc()
    this.increment(consume counter)

[plietar]

This is another instance of where ephemeral caps should be treated differently from stable ones (see #1935). We shouldn't have iso < trn, but iso^ < trn is fine.

[sylvanc]

Nice catch! I suspect result type subtyping should require A <: B /\ A! <: B!.

[sylvanc]

That would account for iso^ <: trn, as iso^ <: trn /\ iso <: box.

Effectively, what is disallowed is iso <: {trn, ref, val, box} and trn <: {ref, val}.

[jemc]

Based on @sylvanc's suggestion, I've marked this as ready for work, and "easy", since it just means adding an extra is_subtype condition for the covariance check.

[plietar]

I'm not sure whether we should simply change the covariance check, or should we change the definition of subtyping of capabilities itself.

George's model of subtyping is very similar to this (Section 3.10, Figure 20)

---

This however requires changing the way subtyping is used when aliasing. The compiler is based on @sylvanc's original model Deny Capabilities for Safe, Fast Actors.

Under this model, an expression e can be aliased into a type T if it has type ET and the alias of ET is a subtype of T. (Section 4, Figure 3)

Here T would be the type of an argument or a local variable for example.

---

Changing the definition of capability subtyping requires changing this as well.

In George's model it is described by the T-Alias and T-Subsume typing rules. (Section 3.12, Figure 32).
.

Here if we want to alias an expression e as type DT0, we need to find a type DT such that DT' ≤ DT and the alias of DT is DT0, where DT' is the type of e,

fun m(x: DT0)

let e : DT'
m(e)

---

Unfortunately, this formulation is inconvenient, since it requires coming up with a type DT "out of thin air". An alternative formulation is to say we can alias e as type DT0 if DT is a subtype of
the unalias of DT0 . This however requires that the unalias of an ephemeral type is undefined.

[plietar]

So I just found that the compiler does what @sylvanc suggested when it comes to the return value: https://github.com/ponylang/ponyc/blob/a093b6084c1f3ba701dba2961819b6574b0e9d14/src/libponyc/expr/reference.c#L888-L896

It prevents this sort of thing :

class Counter

trait A
  fun ref get() : Counter trn
class B is A
  var f: Counter iso = Counter.create()
  fun ref get() : Counter trn => this.f

Error:
main.pony:8:38: function body isn't the result type
  fun ref get() : Counter trn => this.f
                                     ^
    Info:
    main.pony:8:19: function return type: Counter trn
      fun ref get() : Counter trn => this.f
                      ^
    main.pony:7:10: function body type: Counter iso
      var f: Counter iso = Counter.create()
             ^
    main.pony:7:10: Counter iso! is not a subtype of Counter trn!: iso! is not a subcap of trn!
      var f: Counter iso = Counter.create()

[jemc]

Backtracking a bit, is there a reason why George's model has not been incorporated into ponyc yet? Is it just that nobody has picked up that work, or are there incompatibilities or breaking changes that would need to be dealt with?