Refcap violation via gencap-constrained type parameter.

[Praetonus]

class Foo
  var i: USize = 0
  fun ref boom() => i = 3

actor Main
  new create(env: Env) =>
    let a: Foo val = Foo
    env.out.print(a.i.string())
    bla[Foo val](a)
    env.out.print(a.i.string())

  fun bla[A: Foo #read](x: A) =>
    x.boom()

This compiles fine and prints 0 then 3. The val object was indeed modified.

[jemc]

I'll do some investigation of this one.

[jemc]

FYI this works exactly the same way (broken) when using type parameters on a type instead of on a method (when fun bla is converted to primitive Bla fun apply):

class Foo
  var i: USize = 0
  fun ref boom() => i = 3

primitive Bla[A: Foo #read]
  fun apply(x: A) =>
    x.boom()

actor Main
  new create(env: Env) =>
    let a: Foo val = Foo
    env.out.print(a.i.string())
    Bla[Foo val](a)
    env.out.print(a.i.string())

[jemc]

The problem is somewhere in the logic for type params in type/subtype.h.

We need to figure out why the following is seen as true:

ast_t* sub = /*(typeparamref (id A) #read x)*/;
ast_t* sup = /*(typeparamref (id A) ref x)*/;
is_subtype(sub, sup, &info, opt); // should be false, but comes back as true

I'll look more into this later today.

[jemc]

The issue is that is_cap_sub_cap_bound is used, which sees #read as being a subtype of ref. So either calling is_cap_sub_cap_bound is not the right semantics for this situation (and we need to call a different method), or is_cap_sub_cap_bound is implemented with the wrong semantics and needs to be fixed.

[jemc]

Docs for is_cap_sub_cap_bound:

Check subtyping with the knowledge that the original bound rcap was the
same. This is used when checking if a typeparamref is a subtype of itself,
possibly with an altered rcap due to aliasing or viewpoint adaptation.

This doesn't seem correct in this situation, and we should use is_cap_sub_cap instead. However, more investigation is needed to be sure that we can change this situation to use is_cap_sub_cap, while still keeping is_cap_sub_cap_bound in use for situations where it is appropriate/correct.

[jemc]

Unassigning myself for now since I have knowledge-dumped what I have found, and I probably won't have time to work more on this in the next few days. Someone else can feel free to pick up where I left off if they wish, or I will come back to it later in the week.

[jemc]

I did take a little more of a look at this tonight, and I don't feel confident stepping in with a solution without @sylvanc dropping some type theory guidance on me first. I think the problem may be a bit more general than I first thought - requiring a careful approach to avoid making other mistakes in the solution.

[jemc]

The solution is to change the is_subtype call at reify.c:269 to be the only place where the is_cap_sub_cap_bound strategy is used (change it to call another "new" function). The is_cap_sub_cap_bound semantics are only correct for checking type parameter constraints during reification, and at all other times (for is_subtype itself), we need to use the "normal" strategy for comparing caps.

[Praetonus]

I've encountered another instance of this bug.

interface I
  fun ref foo() => None

class C
  fun ref foo() => None

actor Main
  new create(env: Env) =>
    foo[C tag](C)

  fun foo[A: I #any](a: A) =>
    a.foo()

Here, cap_aliasing treats #any! as #alias, and then is_cap_sub_cap_bound says that #alias is a subtype of ref.

[jemc]

To give an update on this, the fix that was discussed earlier seemed not to do the trick.

My plan is to check in with @sylvanc next wednesday to discuss the issue in depth and find the appropriate approach. However, I've unassigned myself in case anyone else wants to take a shot between now and then.

[jemc]

We got another report of this in #1549. I'll paste the repro here, so that we have another test case to check the fix against:

trait Foo
  fun foo()

class Bar is Foo
  fun foo() => None

actor Main
    fun call_foo[X: Foo #any](x: X) =>
      x.foo() // This works, but probably shouldn't work

    new create(e: Env) =>
      let x : Bar tag = Bar
      call_foo[Bar tag](x)

      // This fails to type check as expected
      // x.foo()