Calling box methods on an iso reference replaces this by iso

[plietar]

Currently, when type checking box method bodies, this is reified by box, ref, val.
However, calling such methods only require the receiver to be a subtype of box, and replaces this by the receiver type, which could be iso or trn.

This means calling a box method through an iso receiver will reify a body which wasn't typechecked. This can lead to unsoundness, as shown below.

class Revealer
    fun box reveal(x: this->B ref) : B box => x

class B

actor Main
    new create(env: Env) =>
        let revealer : Revealer iso = Revealer.create()
        let opaque : B tag = B.create()
        let not_opaque : B box = (consume revealer).reveal(opaque)

When the body of reveal is typechecked, x can only have types box->B ref, ref->B ref and val->B ref, in other words B box, B ref and B val. These are all subtypes of the return type, so it type checks fine.

When the body of Main is typechecked, since reveal is called on a Revealer iso, this->B ref becomes iso->B ref, ie B tag. And we can successfully get a box from a tag.

---

This occurs at least in one place in the standard library.
The values method of Array[A] returns a ArrayValues[A, this->Array[A] ref], but the second argument of ArrayValues must be in #read. Again, when typechecking the body of values() this is fine.

However, calling the method on an Array[A] iso will succeed an return a ArrayValues[A, Array[A] tag]. This happens for example in ANSITerm. This leads to non-sensical types, such as the next function of ArrayValues returning a Array[A] tag->A.

I'm not sure why the code in ANSITerm compiles at the moment, but my fix for #1875 broke it.

---

TLDR: We need to make the restrictions on this the same from the caller's and the callee's points of views.

Possible solutions :

• Allow this to mean any subtype of box. This will probably break a lot of today's use cases.
• Only allow box methods to be called on #read receivers (ref, box, val), rather than all the box subtypes. This is inconsistent with other receiver capability.
• Automatically "decay" the receiver type when replacing this. So calling a box method on an iso receiver is allowed, but this is replaced by something in #read.

The last one is the most flexible option, but it's not obvious what to replace this with. ref and val give different but incompatible guarantees. In any case, the caller can always manually decay its iso reference into the type it wants, if the one the compiler picks doesn't have the right guarantees.

[plietar]

This ended up much longer than I expected. Just as a note, here's how I've formalised this viewpoints in my model :

I make the distinction between box methods and #read methods.
So below for example, get1 actually always return B box, since this is always box.
get2 on the other hand behaves like you would expect in normal Pony, where this can be any of box, ref or val.

class A
  fun box get1() : this->B ref
  fun #read get2() : this-> B ref
class B

Receivers can be approximated by implicit arguments, like so (this isn't really true, but its good enough just for explanations) :

class A
  fun get1[This: A box](this: This) : This->B ref
  fun get2[This: A #read](this: This) : This-> B ref

When calling a method, the receiver type must be specified explicitly, as the first type argument.
As you can see, This does not depend on the type of a, but on the type argument specified.

A::get1[A box](a)
A::get1[A ref](a) // error: A ref is not in constraint A box

A::get2[A box](a)
A::get2[A ref](a)
A::get2[A val](a)
A::get2[A iso](a) // error: A iso is not in constraint A #read

Using an iso receiver works, through normal subsumption. It won't be reflected in the signature though, since the type argument is still A ref

let x : A iso
A::get2[A ref](consume a)

---

My proposal for the compiler is to infer the receiver type argument, based on the type of the receiver expression, like is is done today. It is however necessary to decay this type in order to fit the receiver constraint.

[plietar]

I'm still getting used to triaging, I'm not sure what the standards are for difficulty and priority.
Feel free to adjust them.

[SeanTAllen]

@plietar have you seen the triaging guide on the website?

https://www.ponylang.org/contribute/triage

Would love your feedback/PRs to improve that.

[jemc]

@plietar - Quick thought experiment - what if we auto-decayed an iso to trn instead of ref or val?

I think that would "break" your Revealer vulnerability, and still allow more flexibility than ref or val. But it's not immediately clear to me whether it would still enable other vulnerabilities.

Also, it's not clear to me whether type checking the body of a fun box with trn would break any current user code - at first glance it doesn't seem so, because trn may be used freely as a box with no uniqueness restrictions, but maybe I'm missing something.

I'd definitely like to hear if @Praetonus and/or @sylvanc have any bright ideas here.

[plietar]

@jemc Looking at the viewpoint adaptation rules, it seems like decaying to trn would not cause any unsoundness. However this would be more of a coincidence than a clean solution.

Checking fun box methods with trn would break code like this

fun box m(x: this->A ref) =>
  let alias : this->A ref = x

It might be interesting to implement this and see how much code breaks. I'm not sure how it is implemented in the compiler, but it probably needs a new constraint with box, ref, val, trn.

[plietar]

Talked a bit about this in the sync this week with @jemc, and decaying to ref is probably what is the most flexible while still sound, and also breaks the least amount of code.

I have an extremely hacky implementation of it which only decays iso and trn when the receiver type is a simple TK_NOMINAL or TK_TYPEPARAMREF. All the test still pass and the standard library still builds. Additionally, applying #1888 (without the commit which does the decaying manually) now builds fine.

A proper implementation of this probably requires a deeper knowledge of the compiler than I currently have, and I won't have too much time until at least end of June to work on it.

Worth noting, this may interact with (auto) recovery, such that despite decaying to ref you can still get an iso back.

[Praetonus]

It looks like the root of the problem is in the viewpoint_replacethis function, with the following backtrace (irrelevant parts excluded):

1. lookup
2. member_access
3. entity_access
4. expr_dot

When looking up the function being called in order to assemble a function type, this viewpoint adapted types are reified immediately with the type of the receiver (iso here, causing the parameter type to be B tag in the call to reveal).

I think a simple solution would be to force the capability of the receiver to ref in viewpoint_replacethis if it is iso or trn. This function is only called from lookup so I don't think it would have unintended side-effects.

@jemc @plietar Does this look right to you?

[plietar]

I think a simple solution would be to force the capability of the receiver to ref in viewpoint_replacethis if it is iso or trn. This function is only called from lookup so I don't think it would have unintended side-effects.

Yes, this is exactly what my hacky fix does. However it's not obvious to me what to do when the receiver type isn't a TK_NOMINAL or TK_TYPEPARAMREF.

[Praetonus]

The most straightforward way would be to add a function recursively walking through the type AST and building the updated type. You can see various examples in alias.c.

[jemc]

In my opinion, we need to have a plan of action here before merging #1888.

I still think that auto-receiver recovery might be the key to pulling this off in a way that makes the maximum amount of safe code possible without extra burden on the user.

@sylvanc can you please weigh in on this ticket at some point?

[plietar]

@jemc We talked about this last week on the call.
It seems like replacing iso and trn by ref should would. I was unsure how to handle cases where the receiver type is an arrow, but it would seem that it is possible to just replace it the right hand side of the arrow, and it would be just fine.

[jemc]

As discussed on today's sync call, we need to implement this fix before merging #1888, then remove the workaround for this from #1888.

[SeanTAllen]

@plietar pinging for status on this as this now seems to be a blocker for @mfelsche's ponycheck.