this->X! should not be a subtype of this->X

[plietar]

Reduced test case, this creates three references x, y and z to the same object,

class Foo[X]
    fun foo(x: this->X) =>
        let y : this->X = x
        let z : this->X = x
        None

Unless X is bounded by #share (or similar), this should not be allowed.

This can be used to create two iso references to the same object, as shown in the snippet below.
The clone method aliases this.a, which results in a this->A!. However this bug allows it to cast it to a this->A.

class Counter
  var i: USize = 0
  fun ref inc() => i = i + 1

class Box[A]
    var a: (A | None)
    new create(x: (A | None)) =>
        this.a = consume x

    fun ref take() : A^ ? =>
        (this.a = None) as A^

    fun clone() : Box[this->A] =>
        Box[this->A](this.a)

actor Main
  new create(env: Env) =>
    try
        let x: Box[Counter iso] = Box[Counter iso](Counter)
        let y: Box[Counter iso] = x.clone()

        let a : Counter iso = x.take()
        let a' : Counter iso = y.take()

        env.out.print(a.i.string())
        a'.inc()
        env.out.print(a.i.string())
    else
        None
    end

Playground link : https://is.gd/6gwQK4

Pony version :

0.12.3 [release]
compiled with: llvm 3.9.1 -- cc (Ubuntu 5.4.0-6ubuntu1~16.04.4) 5.4.0 20160609

[plietar]

Simpler test case, which relies on X! ≤ ref->X.
The method alias duplicates any reference, including an iso or trn.

class Foo
  fun alias[X](x: X!) : X^ =>
    let y : ref->X = consume x
    consume y

[sylvanc]

This looks like a bug in viewpoint.c. In particular, for the first example, in is_arrow_sub_arrow we compare ask if this->X <: this->X!. This calls viewpoint_reifypair, which results in:

(lldb) call ast_print(r_sub)
(tupletype
  (-> ref (typeparamref (id X) #any !))
  (-> val (typeparamref (id X) #any !))
  (-> box (typeparamref (id X) #any !))
)

(lldb) call ast_print(r_super)
(tupletype
  (-> ref (typeparamref (id X) #any x))
  (-> val (typeparamref (id X) #any x))
  (-> box (typeparamref (id X) #any x))
)

Which is good! But then we need to compare those. And when we have:

(lldb) call ast_print(sub)
(-> ref (typeparamref (id X) #any !))

(lldb) call ast_print(super)
(-> ref (typeparamref (id X) #any x))

It reifies as:

(lldb) call ast_print(r_sub)
(tupletype
  (typeparamref (id X) tag x)
  (typeparamref (id X) box x)
  (typeparamref (id X) ref x)
  (typeparamref (id X) val x)
  (typeparamref (id X) box x)
  (typeparamref (id X) tag x)
)

(lldb) call ast_print(r_super)
(tupletype
  (typeparamref (id X) tag x)
  (typeparamref (id X) box x)
  (typeparamref (id X) ref x)
  (typeparamref (id X) val x)
  (typeparamref (id X) box x)
  (typeparamref (id X) tag x)
)

This is bad! r_super is ref->X, not ref->X! so the reification should be:

(tupletype
  (typeparamref (id X) iso x)
  (typeparamref (id X) trn x)
  (typeparamref (id X) ref x)
  (typeparamref (id X) val x)
  (typeparamref (id X) box x)
  (typeparamref (id X) tag x)
)

[SeanTAllen]

This no longer compiles. I believe this has been fixed, but leaving open for discussion at sync.

main.pony:14:22: argument not assignable to parameter
        Box[this->A](this.a)
                     ^
    Info:
    main.pony:14:22: argument type is (this->A #any | None val)
            Box[this->A](this.a)
                         ^
    main.pony:7:16: parameter type requires (this->A #any ^ | None val^)
        new create(x: (A | None)) =>
                   ^
    main.pony:14:22: A iso is not a subtype of A iso ^: the subtype has no constraint
            Box[this->A](this.a)
                         ^
    main.pony:14:22: A trn is not a subtype of A trn ^: the subtype has no constraint
            Box[this->A](this.a)
                         ^
    main.pony:14:22: (ref->A iso, ref->A trn, ref->A ref, ref->A val, ref->A box, ref->A tag) is not a pairwise subtype of (ref->A iso ^, ref->A trn ^, ref->A ref ^, ref->A val ^, ref->A box ^, ref->A tag ^)
            Box[this->A](this.a)
                         ^
    main.pony:14:22: (ref->A #any, val->A #any, box->A #any) is not a pairwise subtype of (ref->A #any ^, val->A #any ^, box->A #any ^)
            Box[this->A](this.a)
                         ^
    main.pony:14:22: A #any is not a subtype of None val^: the subtype has no constraint
            Box[this->A](this.a)
                         ^
    main.pony:14:22: this->A #any is not a subtype of any element of (this->A #any ^ | None val^)
            Box[this->A](this.a)
                         ^
    main.pony:14:22: not every element of (this->A #any | None val) is a subtype of (this->A #any ^ | None val^)
            Box[this->A](this.a)
                         ^

[jasoncarr0]

Note that this example: #1798 (comment) still compiles and is problematic. The main example no longer works because ! isn't used implicitly in those cases anymore, but the issue still exists when it's used expicitly.